diff --git a/proofs/KeyEncapsulationMechanisms.eca b/proofs/KeyEncapsulationMechanisms.eca index bf3a2e2..d9d7a27 100644 --- a/proofs/KeyEncapsulationMechanisms.eca +++ b/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.