Revision 058022c3be6121e485ecf48e19424d1ed36dc535 authored by François Dupressoir on 19 January 2022, 19:29:05 UTC, committed by François Dupressoir on 19 January 2022, 19:29:05 UTC
closes #127
1 parent 46ba308
SymmetricEncryption.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
require import Bool Core List DBool.
type key.
type plaintext.
type ciphertext.
module type Scheme = {
proc * init(): unit {}
proc kg(): key
proc enc(k:key,p:plaintext): ciphertext
proc dec(k:key,c:ciphertext): plaintext option
}.
module type CPA_Oracles = {
proc enc(p:plaintext): ciphertext
}.
module type CCA_Oracles = {
proc enc(p:plaintext): ciphertext
proc dec(c:ciphertext): plaintext option
}.
module type Adv_INDCPA (O:CPA_Oracles) = {
proc choose(): plaintext * plaintext
proc guess(c:ciphertext): bool
}.
module type Adv_INDCCA (O:CCA_Oracles) = {
proc choose(): plaintext * plaintext
proc guess(c:ciphertext): bool
}.
module Wrap (S:Scheme) = {
var k:key
var qs:ciphertext list
proc init(): unit = {
S.init();
k <@ S.kg();
qs <- [];
}
proc enc(p:plaintext): ciphertext = {
var r:ciphertext;
r <@ S.enc(k,p);
return r;
}
proc dec(c:ciphertext): plaintext option = {
var r:plaintext option;
qs <- c::qs;
r <@ S.dec(k,c);
return r;
}
proc queried_challenge(c:ciphertext): bool = {
return mem qs c;
}
}.
module INDCPA (S:Scheme, A:Adv_INDCPA) = {
module O = Wrap(S)
module A = A(O)
proc main(): bool = {
var b, b':bool;
var p, p0, p1:plaintext;
var c:ciphertext;
O.init();
(p0,p1) <@ A.choose();
b <$ {0,1};
p <- if b then p1 else p0;
c <@ O.enc(p);
b' <@ A.guess(c);
return (b = b');
}
}.
module INDCCA (S:Scheme, A:Adv_INDCCA) = {
module O = Wrap(S)
module A = A(O)
proc main(): bool = {
var b, b', qc:bool;
var p, p0, p1:plaintext;
var c:ciphertext;
O.init();
(p0,p1) <@ A.choose();
b <$ {0,1};
p <- if b then p1 else p0;
c <@ O.enc(p);
b' <@ A.guess(c);
qc <@ O.queried_challenge(c);
return (b = b' /\ !qc);
}
}.
module ToCCA (A:Adv_INDCPA, O:CCA_Oracles) = A(O).
lemma CCA_implies_CPA (S <: Scheme {INDCPA}) (A <: Adv_INDCPA {S, INDCPA}) &m:
Pr[INDCPA(S,A).main() @ &m: res] = Pr[INDCCA(S,ToCCA(A)).main() @ &m: res].
proof strict.
byequiv (_: ={glob A} ==> ={res})=> //; proc.
call{2} (_: Wrap.qs = [] ==> !res); first by proc; skip; smt.
conseq [-frame] (_: _ ==> Wrap.qs{2} = [] /\ (b = b'){1} = (b = b'){2}); first smt.
call (_: ={glob Wrap, glob S} /\ Wrap.qs{2} = []);
first by proc; call (_: true).
call (_: ={glob Wrap, glob S});
first by call (_: true).
wp; rnd.
call (_: ={glob Wrap, glob S} /\ Wrap.qs{2} = []);
first by proc; call (_: true).
by call (_: true ==> ={glob Wrap, glob S} /\ Wrap.qs{2} = []);
first by proc; wp; sim.
qed.
Computing file changes ...