Cleanup previous proof.

proofs/KeyEncapsulationMechanisms.eca

@@ -3401,21 +3401,29 @@ module R_SROBCPA_WROBCPA (S : Scheme) (A : Adv_WROBCPA) : Adv_SROBCPA = {
 
 section.
 
+(* Declare arbitrary KEM S *)
 declare module S <: Scheme.
-declare module A <: Adv_WROBCPA{-S}.
 
+(* Losslessness (i.e., termination) assumptions on S's procedures *)
 declare axiom S_keygen_ll : islossless S.keygen.
 declare axiom S_encaps_ll : islossless S.encaps.
 declare axiom S_decaps_ll : islossless S.decaps.
-declare axiom A_choose_ll : islossless A.choose.
 
+(* Statelessness assumptions on S's procedures *)
 declare axiom S_keygen_sl (GS : glob S) :
   phoare[S.keygen : glob S = GS ==> glob S = GS] = 1%r. 
-
 declare axiom S_decaps_sl (GS : glob S) :
   phoare[S.decaps : glob S = GS ==> glob S = GS] = 1%r. 
+
+(* Declare arbitrary WROB-CPA adversary A *)
+declare module A <: Adv_WROBCPA{-S}.
+
+(* Losslessness (i.e., termination) assumptions on A *)
+declare axiom A_choose_ll : islossless A.choose.
 
-local module DD = {
+
+(* Auxiliary module used to prove equivalence between different orders of decapsulation *)
+local module Decaps_Order = {
   proc main(sk, sk', c, c') : key_t option * key_t option = {
     var k, k' : key_t option;
 
@@ -3426,36 +3434,35 @@ local module DD = {
   }
 }.
 
-local lemma testph skt skt' ct ct' kt kt' &m :
-  Pr[DD.main(skt, skt', ct, ct') @ &m : (res.`1, res.`2) = (kt, kt')]
+(* Equality (of probability) relating Decaps_Order call and individual decapsulation calls *)
+local lemma EqPr_DecapsOrder &m skt skt' ct ct' kt kt' :
+  Pr[Decaps_Order.main(skt, skt', ct, ct') @ &m : (res.`1, res.`2) = (kt, kt')]
   =
-  Pr[S.decaps(skt, ct) @ &m : res = kt] * 
-  Pr[S.decaps(skt', ct') @ &m : res = kt'].
+  Pr[S.decaps(skt, ct) @ &m : res = kt] * Pr[S.decaps(skt', ct') @ &m : res = kt'].
 proof.
 pose pr_dec_skc := Pr[S.decaps(skt, ct) @ &m : res = kt]. 
 pose pr_dec_skcp := Pr[S.decaps(skt', ct') @ &m : res = kt']. 
 byphoare (: glob S = (glob S){m} /\ arg = (skt, skt', ct, ct') ==> _) => //.
 proc.
-seq 1 : (k = kt) pr_dec_skc pr_dec_skcp _ 0%r (#pre). 
-conseq />.
-call (: (glob S) = (glob S){m} ==> (glob S) = (glob S){m}). 
-bypr. move=> /> &m' glS. rewrite Pr[mu_not].
-rewrite (: Pr[S.decaps(sk{m'}, c{m'}) @ &m' : true] = 1%r).
-byphoare S_decaps_ll => //.
-rewrite RField.subr_eq0 eq_sym.
-byphoare (S_decaps_sl (glob S){m}) => //. by skip.
-call (: glob S = (glob S){m} /\ arg = (skt, ct) ==> res = kt).
-rewrite /pr_dec_skc. bypr => /> &m' glS ->.
-byequiv => //. by proc true. by skip.
-call (: glob S = (glob S){m} /\ arg = (skt', ct') ==> res = kt').
-rewrite /pr_dec_skcp. bypr. move=> &m' [glS ->] /=.
-byequiv => //. rewrite glS. by proc true.
-skip => />. hoare.
-call (: true). skip => />. 
-smt().
+seq 1 : (k = kt) pr_dec_skc pr_dec_skcp _ 0%r (#pre) => //.
++ call (: (glob S) = (glob S){m} ==> (glob S) = (glob S){m}); 2: by skip.
+  bypr=> /> &m' glS. 
+  rewrite Pr[mu_not] (: Pr[S.decaps(sk{m'}, c{m'}) @ &m' : true] = 1%r); 1: by byphoare S_decaps_ll => //.
+  by rewrite RField.subr_eq0 eq_sym; byphoare (S_decaps_sl (glob S){m}) => //. 
++ call (: glob S = (glob S){m} /\ arg = (skt, ct) ==> res = kt); 2: by skip.
+  rewrite /pr_dec_skc; bypr => /> &m' glS ->.
+  by byequiv => //; proc true. 
++ call (: glob S = (glob S){m} /\ arg = (skt', ct') ==> res = kt'); 2: by skip => />.
+  rewrite /pr_dec_skcp; bypr=> &m' [glS ->] /=.
+  by byequiv => //; proc true.
+by hoare; call (: true); skip => />. 
 qed.
 
-local lemma testpr skt ct kt &1 &2:
+(* 
+  The output distribution of decapsulation is the same as long as 
+  the (initial) globals and arguments are the same.
+*)
+local lemma EqPr_Decaps &1 &2 skt ct kt:
   (glob S){1} = (glob S){2} =>
   Pr[S.decaps(skt, ct) @ &1 : res = kt]
   =
@@ -3466,18 +3473,25 @@ byequiv (: ={glob S, arg} ==> ={res}) => //.
 by proc true.
 qed.
 
-local equiv testeqv :
-  DD.main ~ DD.main : 
+(* 
+  Equivalence stating relation between input and output order of Decaps_Order.
+  (i.e., if you swap public keys and secret keys in input, output keys will be swapped) 
+*)
+local equiv Eqv_DecapsOrder :
+  Decaps_Order.main ~ Decaps_Order.main : 
     ={glob S} /\ arg{1} = (arg.`2, arg.`1, arg.`4, arg.`3){2} ==> res{1} = (res.`2, res.`1){2}.
 proof.
-bypr (res.`1, res.`2){1} (res.`2, res.`1){2}. smt().
-move=> />. move=> &1 &2 [kt kt'] eqglS -> /=. 
-move:  (testph sk'{2} sk{2} c'{2} c{2} kt kt' &1) => /= ->.
-move:  (testph sk{2} sk'{2} c{2} c'{2} kt' kt &2) => /=. 
-rewrite andbC => ->.
-by rewrite (testpr sk'{2} c'{2} kt &1 &2) 1://  (testpr sk{2} c{2} kt' &1 &2) 1:// RField.mulrC.
+bypr (res.`1, res.`2){1} (res.`2, res.`1){2} => [/#|]. 
+move=> /> &1 &2 [kt kt'] eqglS -> /=. 
+rewrite (EqPr_DecapsOrder &1 _ _ _ _ kt kt') andbC (EqPr_DecapsOrder &2 _ _ _ _ kt' kt). 
+by rewrite 2?(EqPr_Decaps &1 &2) 3:RField.mulrC.
 qed. 
 
+
+(* 
+  Auxiliary module equivalent to WROB_CPA, but with additional variables, and 
+  certain variables defined global instead of local (so we can refer to them in proofs)
+*)
 local module WROB_CPA_V = {
   var b : bool
   var k'' : key_t option
@@ -3502,6 +3516,10 @@ local module WROB_CPA_V = {
   }
 }.
 
+(* 
+  Equivalence (expressed as equality of probabilities) between 
+  original WROB_CPA and (auxiliary) WROB_CPA_V.
+*)
 local lemma EqPr_WROBCPA_V &m :
   Pr[WROB_CPA(S, A).main() @ &m : res]
   =
@@ -3554,127 +3572,20 @@ proc; inline *.
 seq 4 7 : (={glob S, sk0, sk1, c} /\ WROB_CPA_V.b{1} = b{2}). 
 + by wp; call (: true); call (: true); wp; do 2! call (: true).
 case (b{2}); last first.
-+ transitivity{2} {(k0, k1) <@ DD.main(sk1, sk0, c, c);} 
++ transitivity{2} {(k0, k1) <@ Decaps_Order.main(sk1, sk0, c, c);} 
                   (! WROB_CPA_V.b{1} /\ ={glob S, sk0, sk1, c} ==> k'{1} <> None /\ WROB_CPA_V.k''{1} <> None => k0{2} <> None /\ k1{2} <> None)
-                  (={glob S, sk0, sk1, c} /\ b{1} ==> k0{1} <> None /\ k1{1} <> None => k0{2} <> None /\ k1{2} <> None). smt(). smt(). 
-  inline{2} 1.
-  wp. call (: true). conseq />. smt(). call (: true); wp; skip => />.
-  transitivity{1} {(k0, k1) <@ DD.main(sk0, sk1, c, c);} 
+                  (={glob S, sk0, sk1, c} /\ b{1} ==> k0{1} <> None /\ k1{1} <> None => k0{2} <> None /\ k1{2} <> None); 1,2: smt().
+  + inline{2} 1.
+    by wp; call (: true); call (: true); wp; skip => />. 
+  transitivity{1} {(k0, k1) <@ Decaps_Order.main(sk0, sk1, c, c);} 
                   (={glob S, sk0, sk1, c} ==> k0{1} <> None /\ k1{1} <> None => k0{2} <> None /\ k1{2} <> None)
-                  (={glob S, sk0, sk1, c} ==> k0{1} <> None /\ k1{1} <> None => k0{2} <> None /\ k1{2} <> None).
-  progress. smt().  smt().
-  call testeqv. by skip.
+                  (={glob S, sk0, sk1, c} ==> k0{1} <> None /\ k1{1} <> None => k0{2} <> None /\ k1{2} <> None); 1,2: smt().  
+  + by call Eqv_DecapsOrder.
   inline{1} 1.
   by wp; call (: true); call (: true); wp; skip.
-call (: true); call (: true). by skip => />.
-qed.
-
-(*
-(** Reduction adversary reducing SROB-CCA1 to WROB-CCA1 **)
-module (R_SROBCCA1_WROBCCA1 (A : Adv_WROBCCA1) : Adv_SROBCCA1) (O0 : Oracles_CCA, O1 : Oracles_CCA) = {
-  proc scout(pk0 : pk_t, pk1 : pk_t) : unit = {
-    A(O0, O1).scout(pk0, pk1);
-  }
-
-  proc distinguish(kc : key_t * ctxt_t) : bool = {
-    var b : bool;
-
-    b <@ A(O0, O1).distinguish(kc.`2);
-
-    return b;
-  }
-}.
-
-(** 
-  Equivalence between WROB_CCA1 (for arbitrary adversary) and SROB_CCA1
-  (with above reduction adverary). (Shows SROB_CCA1 --> WROB_CCA1.)
-**)
-lemma Eqv_WROBCCA1_SROBCCA1 (S <: Scheme) (O0 <: Oracles_CCA1i{-S}) (O1 <: Oracles_CCA1i{-S, -O0})
-                           (A <: Adv_WROBCCA1{-S, -O0, -O1}) :
-  equiv[O0.init ~ O0.init : ={glob S, glob A} ==> ={glob O0}] =>
-  equiv[O1.init ~ O1.init : ={glob S, glob A} ==> ={glob O1}] =>
-  equiv[WROB_CCA1(S, O0, O1, A).main ~ SROB_CCA1(S, O0, O1, R_SROBCCA1_WROBCCA1(A)).main :
-    ={glob S, glob A} ==> ={res}].
-proof.
-move=> O0_eqv_init O1_eqv_init.
-proc; inline *.
-wp; call (: true); wp; call (: true); rnd.
-call (: ={glob O0, glob O1}); 1,2: by sim.
-wp; call O1_eqv_init; call O0_eqv_init.
-by do 2! call (: true). 
-qed.
-
-
-(** Reduction adversary reducing SROB-CCA2 to WROB-CCA2 **)
-module (R_SROBCCA2_WROBCCA2 (A : Adv_WROBCCA2) : Adv_SROBCCA2) (O0 : Oracles_CCA, O1 : Oracles_CCA) = {
-  proc scout(pk0 : pk_t, pk1 : pk_t) : unit = {
-    A(O0, O1).scout(pk0, pk1);
-  }
-
-  proc distinguish(kc : key_t * ctxt_t) : bool = {
-    var b : bool;
-
-    b <@ A(O0, O1).distinguish(kc.`2);
-
-    return b;
-  }
-}.
-
-(** 
-  Equivalence between WROB_CCA2 (for arbitrary adversary) and SROB_CCA2
-  (with above reduction adverary). (Shows SROB_CCA2 --> WROB_CCA2.)
-**)
-lemma Eqv_WROBCCA2_SROBCCA2 (S <: Scheme)
-                           (O01 <: Oracles_CCA1i{-S}) (O11 <: Oracles_CCA1i{-S, -O01})
-                           (O02 <: Oracles_CCA2i{-S}) (O21 <: Oracles_CCA2i{-S, -O02})
-                           (A <: Adv_WROBCCA2{-S, -O01, -O11, -O02, -O21}) :
-  equiv[O01.init ~ O01.init : ={glob S, glob A} ==> ={glob O01}] =>
-  equiv[O11.init ~ O11.init : ={glob S, glob A} ==> ={glob O11}] =>
-  equiv[O02.init ~ O02.init : ={glob S, glob A} ==> ={glob O02}] =>
-  equiv[O21.init ~ O21.init : ={glob S, glob A} ==> ={glob O21}] =>
-  equiv[WROB_CCA2(S, O01, O11, O02, O21, A).main ~ SROB_CCA2(S, O01, O11, O02, O21, R_SROBCCA2_WROBCCA2(A)).main :
-          ={glob S, glob A} ==> ={res}].
-proof.
-move=> O01_eqv_init O11_eqv_init O02_eqv_init O21_eqv_init.
-proc; inline *.
-wp; call (: ={glob O02, glob O21}); 1,2: by sim.
-wp; call O21_eqv_init; call O02_eqv_init. 
-call (: true); rnd. 
-call (: ={glob O01, glob O11}); 1,2: by sim.
-wp; call O11_eqv_init; call O01_eqv_init. 
-by do 2! call (: true).
+by call (: true); call (: true); skip => />.
 qed.
 
-
-(** Reduction adversary reducing SROB-CCA to WROB-CCA **)
-module (R_SROBCCA_WROBCCA (A : Adv_WROBCCA) : Adv_SROBCCA) (O0 : Oracles_CCA, O1 : Oracles_CCA)  = {
-  proc distinguish(pk0 : pk_t, pk1 : pk_t, kc : key_t * ctxt_t) : bool = {
-    var b : bool;
-
-    b <@ A(O0, O1).distinguish(pk0, pk1, kc.`2);
-
-    return b;
-  }
-}.
-
-(** 
-  Equivalence between WROB_CCA (for arbitrary adversary) and SROB_CCA
-  (with above reduction adverary). (Shows SROB_CCA --> WROB_CCA.)
-**)
-lemma Eqv_WROBCCA_SROBCCA (S <: Scheme) (O0 <: Oracles_CCA2i{-S}) (O1 <: Oracles_CCA2i{-S, -O0})
-                         (A <: Adv_WROBCCA{-S, -O0, -O1}) :
-  equiv[O0.init ~ O0.init : ={glob S, glob A} ==> ={glob O0}] =>
-  equiv[O1.init ~ O1.init : ={glob S, glob A} ==> ={glob O1}] =>
-  equiv[WROB_CCA(S, O0, O1, A).main ~ SROB_CCA(S, O0, O1, R_SROBCCA_WROBCCA(A)).main :
-        ={glob S, glob A} ==> ={res}].
-proof.
-move=> O0_eqv_init O1_eqv_init.
-proc; inline *.
-wp; call (: ={glob O0, glob O1}); 1,2: by sim.
-wp; call O1_eqv_init; call O0_eqv_init.
-call (: true); rnd.
-by do 2! call (: true).
-qed.
-*)
 end section.
+
 end Relations.