diff --git a/proofs/FO_KEM.eca b/proofs/FO_KEM.eca index ef1e7fc..83e5ee3 100644 --- a/proofs/FO_KEM.eca +++ b/proofs/FO_KEM.eca @@ -1,5 +1,7 @@ require import AllCore. require KeyEncapsulationMechanisms PublicKeyEncryption. +require PublicKeyEncryptionROM. + (* Types *) @@ -12,10 +14,26 @@ type sk_t. (** Shared/session keys (symmetric) **) type key_t. +(** Plaintexts **) +type ptxt_t = key_t. + (** Ciphertexts/Encapsulations **) type ctxt_t. +(** Randomness **) +type rand_t. +(* Clones and imports *) (** Import basic PKE and KEM definitions **) -clone import PublicKeyEncryption as PKE. +clone import PublicKeyEncryptionROM as PKEROM with + type pk_t <- pk_t, + type sk_t <- sk_t, + type ptxt_t <- ptxt_t, + type ctxt_t <- ctxt_t, + + type in_t <- ptxt_t, + type out_t <- rand_t. + +import PKE F_RO. +import DeltaCorrectROM. diff --git a/proofs/KeyEncapsulationMechanisms.eca b/proofs/KeyEncapsulationMechanisms.eca index f7670fc..51b9e33 100644 --- a/proofs/KeyEncapsulationMechanisms.eca +++ b/proofs/KeyEncapsulationMechanisms.eca @@ -12,7 +12,7 @@ - [Keeping Up with the KEMs: Stronger Security Notions for KEMs and Automated Analysis of KEM-based Protocols](https://eprint.iacr.org/2023/1933) - [Unbindable Kemmy Schmidt: ML-KEM is neither MAL-BIND-K-CT nor MAL-BIND-K-PK](https://eprint.iacr.org/2024/523) - [On the Complete Non-Malleability of the Fujisaki-Okamoto Transform](https://eprint.iacr.org/2022/1654) - (TODO: Add complete non-malleability) + (Missing properties: complete non-malleability) ^*) (* Require/Import libraries *) @@ -1837,9 +1837,16 @@ type bindconf = [ Checks whether binding configuration considers the public key as a binding source element **) -op is_pkbc (bc : bindconf) = +op is_pkbsc (bc : bindconf) = bc = PKK_Binds_CT \/ bc = PKCT_Binds_K. +(** + Checks whether binding configuration considers + the public key as a binding source element +**) +op is_pkbtc (bc : bindconf) = + bc = K_Binds_PK \/ bc = CT_Binds_PK \/ bc = KCT_Binds_PK. + (** Checks whether the provided values consitute a binding break w.r.t. the given binding configuration. @@ -1871,6 +1878,7 @@ op is_bindbreak (bc : bindconf) (k0 k1 : key_t) (pk0 pk1 : pk_t) (c0 c1 : ctxt_t *) (** Adversary class considered for HON-BIND **) module type Adv_HONBIND (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(bc : bindconf) : bool { } proc find(bc : bindconf, pk0 : pk_t, pk1 : pk_t) : ctxt_t * ctxt_t }. @@ -1879,16 +1887,24 @@ module HON_BIND (S : Scheme, O0 : Oracles_CCA1i, O1 : Oracles_CCA1i, A : Adv_HON proc main(bc : bindconf) = { var pk0, pk1 : pk_t; var sk0, sk1 : sk_t; + var b : bool; var c0, c1 : ctxt_t; var k0, k1 : key_t option; var no_fail: bool; (pk0, sk0) <@ S.keygen(); - if (is_pkbc bc) { + if (is_pkbsc bc) { (* public key is binding source, equalize key pairs *) (pk1, sk1) <- (pk0, sk0); - } else { + } elif (is_pkbtc bc) { (* public key is binding target, independently generate key pairs *) (pk1, sk1) <@ S.keygen(); + } else { (* neither of the above, let adversary choose what to do with key pairs *) + b <@ A(O0(S), O1(S)).choose(bc); + if (b) { + (pk1, sk1) <@ S.keygen(); + } else { + (pk1, sk1) <- (pk0, sk0); + } } O0(S).init(sk0); @@ -1913,6 +1929,7 @@ module HON_BIND (S : Scheme, O0 : Oracles_CCA1i, O1 : Oracles_CCA1i, A : Adv_HON *) (** Adversary class considered for LEAK-BIND **) module type Adv_LEAKBIND = { + proc choose(bc : bindconf) : bool proc find(bc : bindconf, pk0 : pk_t, sk0 : sk_t, pk1 : pk_t, sk1 : sk_t) : ctxt_t * ctxt_t }. @@ -1921,16 +1938,24 @@ module LEAK_BIND (S : Scheme, A : Adv_LEAKBIND) = { proc main(bc : bindconf) = { var pk0, pk1 : pk_t; var sk0, sk1 : sk_t; + var b : bool; var c0, c1 : ctxt_t; var k0, k1 : key_t option; var no_fail : bool; (pk0, sk0) <@ S.keygen(); - if (is_pkbc bc) { + if (is_pkbsc bc) { (* public key is binding source, equalize key pairs *) (pk1, sk1) <- (pk0, sk0); - } else { + } elif (is_pkbtc bc) { (* public key is binding target, independently generate key pairs *) (pk1, sk1) <@ S.keygen(); + } else { (* neither of the above, let adversary choose what to do with key pairs *) + b <@ A.choose(bc); + if (b) { + (pk1, sk1) <@ S.keygen(); + } else { + (pk1, sk1) <- (pk0, sk0); + } } (c0, c1) <@ A.find(bc, pk0, sk0, pk1, sk1); @@ -3450,6 +3475,14 @@ module Keygen_Equal_PK (S : Scheme) = { (** Reduction adversary reducing from LEAK-BIND to HON-BIND **) module R_LEAK_HON (S : Scheme) (O0 : Oracles_CCA1i, O1 : Oracles_CCA1i) (A : Adv_HONBIND) : Adv_LEAKBIND = { + proc choose(bc : bindconf) : bool = { + var b : bool; + + b <@ A(O0(S), O1(S)).choose(bc); + + return b; + } + proc find(bc : bindconf, pk0 : pk_t, sk0 : sk_t, pk1 : pk_t, sk1 : sk_t) : ctxt_t * ctxt_t = { var c0, c1 : ctxt_t; @@ -3476,7 +3509,10 @@ wp; call (: true); call (: true). wp; call (: ={glob O0, glob O1, glob S}); 1,2: by sim. do 2! (call (: ={glob S}); 1..3: by sim). seq 1 1 : (#pre /\ ={pk0, sk0}); 1: by sim. -by wp; if => //; [wp | call (: true)]. +wp; if => //=; 1: by wp. +if => //=; 1: by call (: true). +seq 1 3 : (#pre /\ ={b}); 1: by wp; call (: true); wp. +by if => //; [call (: true) | wp]. qed. (** Reduction adversary reducing from MAL-BIND (Decaps Decaps case) to LEAK-BIND **) @@ -3484,16 +3520,24 @@ module R_MALDD_LEAK (S : Scheme) (A : Adv_LEAKBIND) : Adv_MALBIND_DD = { proc find(bc : bindconf) : sk_t * sk_t * ctxt_t * ctxt_t = { var pk0, pk1 : pk_t; var sk0, sk1 : sk_t; + var b : bool; var c0, c1 : ctxt_t; (pk0, sk0) <@ S.keygen(); - if (is_pkbc bc) { + if (is_pkbsc bc) { (* public key is binding source, equalize key pairs *) (pk1, sk1) <- (pk0, sk0); - } else { + } elif (is_pkbtc bc) { (* public key is binding target, independently generate key pairs *) (pk1, sk1) <@ S.keygen(); - } - + } else { (* neither of the above, let adversary choose what to do with key pairs *) + b <@ A.choose(bc); + if (b) { + (pk1, sk1) <@ S.keygen(); + } else { + (pk1, sk1) <- (pk0, sk0); + } + } + (c0, c1) <@ A.find(bc, pk0, sk0, pk1, sk1); return (sk0, sk1, c0, c1); @@ -3513,44 +3557,65 @@ lemma Eqv_LEAKBIND_MALBINDDD (S <: Scheme) (A <: Adv_LEAKBIND{-S}) : ={glob S, glob A, arg} ==> ={res}]. proof. move=> kg_sem. -proc; inline *. +proc; inline *. wp; call (: true); call (: true). wp; call (: true); sp 0 1. seq 1 1 : (#pre /\ pk0{1} = pk00{2} /\ sk0{1} = sk00{2} /\ sk2pk sk0{1} = pk0{1}). + call (: ={glob S} ==> ={glob S, res} /\ sk2pk res{1}.`2 = res{1}.`1) => //. by conseq (: ={glob S} ==> ={glob S, res}) kg_sem; proc true. if => //; 1: by wp. +if => //=. ++ call (: ={glob S} ==> ={glob S, res} /\ sk2pk res{1}.`2 = res{1}.`1) => //. + + by conseq (: ={glob S} ==> ={glob S, res}) kg_sem; proc true. + by skip => /> /#. +seq 1 1 : (#pre /\ ={b}); 1: by wp; call (: true); wp. +if => //; 2: by wp. call (: ={glob S} ==> ={glob S, res} /\ sk2pk res{1}.`2 = res{1}.`1) => //. + by conseq (: ={glob S} ==> ={glob S, res}) kg_sem; proc true. by skip => /> /#. qed. -(* Impossible? +(** Reduction adversary reducing HON-BIND-K-CT and HON-BIND-PKK-CT **) module (R_HON_K_PKK_CT (S : Scheme) (A : Adv_HONBIND) : Adv_HONBIND) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(bc : bindconf) : bool = { + return false; + } + proc find(bc : bindconf, pk0 : pk_t, pk1 : pk_t) : ctxt_t * ctxt_t = { var c0, c1 : ctxt_t; - var pk1' : pk_t; - var sk1' : sk_t; - - (pk1', sk1') <@ S.keygen(); - (c0, c1) <@ A(O0(S), O1(S)).find(PKK_Binds_CT, pk0, pk1'); + (c0, c1) <@ A(O0, O1).find(PKK_Binds_CT, pk0, pk1); return (c0, c1); } }. +(** + Equivalence between HON-BIND-PKK-CT (for arbitrary adversary) + and HON-BIND-K-CT (with above reduction adversary). + (Shows HON-BIND-K-CT --> HON-BIND-PKK-CT.) +**) lemma Eqv_HON_PKK_K_CT (S <: Scheme) (O0 <: Oracles_CCA1i{-S}) (O1 <: Oracles_CCA1i{-S, -O0}) (A <: Adv_HONBIND{-S, -O0, -O1}): - (forall GS, phoare[S.keygen : glob S = GS ==> glob S = GS] = 1%r) => - equiv[O0(S).init ~ O0(S).init : ={glob S, glob A} ==> ={glob O0}] => - equiv[O1(S).init ~ O1(S).init : ={glob S, glob A} ==> ={glob O1}] => - equiv[HON_BIND(S, O0, O1, A).main ~ HON_BIND(S, O0, O1, R_HON_PKK_K_CT(S, A)).main : - ={glob S, glob A} /\ arg{1} = K_Binds_CT /\ arg{2} = PKK_Binds_CT ==> ={res}]. -proof. admit. qed. -*) + equiv[HON_BIND(S, O0, O1, A).main ~ HON_BIND(S, O0, O1, R_HON_K_PKK_CT(S, A)).main : + ={glob S, glob O0, glob O1, glob A} /\ arg{1} = PKK_Binds_CT /\ arg{2} = K_Binds_CT ==> ={res}]. +proof. +proc; inline *. +wp; call (: true); call (: true) => /=. +wp; call (: ={glob S, glob O0, glob O1}); 1,2: by sim. +wp; do 2! (call(: ={glob S}); 1..3: by sim). +rcondt{1} 2; 1: by move=> &m; call (: true). +do 2! (rcondf{2} 2; 1: by move=> &m; call (: true)). +rcondf{2} 4; 1: by move=> &m; wp; call (: true). +by wp; call (: true). +qed. + (** Reduction adversary reducing HON-BIND-K-PK and HON-BIND-CT-PK to HON-BIND-KCT-PK **) module (R_HON_K_CT_KCT_PK (A : Adv_HONBIND) : Adv_HONBIND) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(bc : bindconf) : bool = { + return witness; + } + proc find(bc : bindconf, pk0 : pk_t, pk1 : pk_t) : ctxt_t * ctxt_t = { var c0, c1 : ctxt_t; @@ -3579,15 +3644,22 @@ wp; do 2! (call (: ={glob S}); 1..3: by sim). seq 1 1 : (#pre /\ ={pk0, sk0}); 1: by call (: true). rcondf{1} 1; 1: by auto. rcondf{2} 1; 1: by auto => /> /#. -by call(: true); skip => /> /#. -qed. +rcondt{1} 1; 2: rcondt{2} 1; 1,2: by auto => /> /#. +by call (: true); skip => /> /#. +qed. (** Reduction adversary reducing HON-BIND-CT-PK to HON-BIND-CT-K **) -module (R_HON_CT_PK_K(A : Adv_HONBIND) : Adv_HONBIND) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { +module (R_HON_CT_PK_K (A : Adv_HONBIND) : Adv_HONBIND) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(bc : bindconf) : bool = { + return witness; + } + proc find(bc : bindconf, pk0 : pk_t, pk1 : pk_t) : ctxt_t * ctxt_t = { + var b : bool; var c0, c1 : ctxt_t; + b <@ A(O0, O1).choose(CT_Binds_K); (c0, c1) <@ A(O0, O1).find(CT_Binds_K, pk0, pk1); return (c0, c1); @@ -3600,8 +3672,14 @@ section. declare module S <: Scheme. (* Losslessness (i.e., termination) assumption on S's decapsulation *) +declare axiom S_keygen_ll : islossless S.keygen. declare axiom S_decaps_ll : islossless S.decaps. +(* Determinism assumption on S's decapsulation *) +declare op s_decaps : sk_t -> ctxt_t -> key_t option. +declare axiom S_decaps_det (sk' : sk_t) (c' : ctxt_t) : + hoare[S.decaps : arg = (sk', c') ==> res = s_decaps sk' c']. + (* Declare arbitrary CCA1 oracles O0 and O1 (with initialization) *) declare module O0 <: Oracles_CCA1i{-S}. declare module O1 <: Oracles_CCA1i{-S, -O0}. @@ -3614,6 +3692,7 @@ declare axiom O1_init_ll : islossless O1(S).init. declare module A <: Adv_HONBIND{-S, -O0, -O1}. (* Losslessness (i.e., termination) assumption on A's finding *) +declare axiom A_choose_ll : islossless A(O0(S), O1(S)).choose. declare axiom A_find_ll : islossless A(O0(S), O1(S)).find. (* @@ -3621,25 +3700,29 @@ declare axiom A_find_ll : islossless A(O0(S), O1(S)).find. defined global instead of local (so we can refer to them in proofs). *) local module HON_BIND_V = { - var pk0 : pk_t - var pk1 : pk_t + var pk0, pk1 : pk_t + var b : bool proc main(bc : bindconf) : bool = { - - var sk0 : sk_t; - var sk1 : sk_t; - var c0 : ctxt_t; - var c1 : ctxt_t; - var k0 : key_t option; - var k1 : key_t option; + var sk0, sk1 : sk_t; + var c0, c1 : ctxt_t; + var k0, k1 : key_t option; var no_fail : bool; (pk0, sk0) <@ S.keygen(); - if (is_pkbc bc) { + + if (is_pkbsc bc) { (* public key is binding source, equalize key pairs *) (pk1, sk1) <- (pk0, sk0); - } else { + } elif (is_pkbtc bc) { (* public key is binding target, independently generate key pairs *) (pk1, sk1) <@ S.keygen(); - } + } else { (* neither of the above, let adversary choose what to do with key pairs *) + b <@ A(O0(S), O1(S)).choose(bc); + if (b) { + (pk1, sk1) <@ S.keygen(); + } else { + (pk1, sk1) <- (pk0, sk0); + } + } O0(S).init(sk0); O1(S).init(sk1); @@ -3679,29 +3762,100 @@ lemma Bnd_HON_CT_K_PK &m : + Pr[Keygen_Equal_PK(S).main() @ &m : res]. proof. -rewrite EqPr_HONBIND_V Pr[mu_split HON_BIND_V.pk0 <> HON_BIND_V.pk1] StdOrder.RealOrder.ler_add. +rewrite EqPr_HONBIND_V Pr[mu_split HON_BIND_V.b]. +have -> /=: + Pr[HON_BIND_V.main(CT_Binds_K) @ &m : res /\ !HON_BIND_V.b] = 0%r. ++ byphoare (: arg = CT_Binds_K ==> _) => //=. + hoare; proc. + do 2! (rcondf 2; 1: by call (: true)). + seq 2 : #pre; 1: by call (: true); call (: true). + case HON_BIND_V.b; 1: by conseq (: _ ==> true) => />. + rcondf 1 => //. + seq 4 : (#pre /\ sk0 = sk1 /\ HON_BIND_V.pk0 = HON_BIND_V.pk1). + + by sp 1; conseq (: _ ==> true) => />. + case (c0 = c1); 2: by conseq (: _ ==> true) => />. + exlim sk0, c0 => skt ct. + by wp; do 2! (call (S_decaps_det skt ct)). +rewrite Pr[mu_split HON_BIND_V.pk0 <> HON_BIND_V.pk1] StdOrder.RealOrder.ler_add. + byequiv (: ={glob S, glob O0, glob O1, glob A} /\ bc{1} = CT_Binds_K /\ bc{2} = CT_Binds_PK ==> _) => //. proc; inline *. seq 1 1 : (#pre /\ ={sk0} /\ HON_BIND_V.pk0{1} = pk0{2}); 1: by call (: true). + do 2! (rcondf{1} 1; 1: by auto). + rcondf{2} 1; 1: by auto. + rcondt{2} 1; 1: by auto. + swap{2} 7 -6. + seq 1 1 : (#pre /\ HON_BIND_V.b{1} = b0{2}); 1: by call (: true). + case (!HON_BIND_V.b{1}). + + conseq (: _ ==> true) => //. + rcondf{1} 1; 1: by auto. + wp; do 2! (call{1} S_decaps_ll; call{2} S_decaps_ll). + wp; call{1} A_find_ll; call{2} A_find_ll. + wp; call{1} O1_init_ll; call{2} O1_init_ll. + call{1} O0_init_ll; call{2} O0_init_ll. + by wp; call{2} S_keygen_ll. wp; call (: true); call (: true); wp. call (: ={glob O0, glob O1, glob S}); 1,2: by sim. wp; do 2! (call (: ={glob S}); 1..3: by sim). - rcondf{1} 1; 1: by auto. - rcondf{2} 1; 1: by auto. - by call (: true). -byequiv => //. + rcondt{1} 1; 1: by auto. + by call (: true); skip => />. +byequiv (: ={glob S} /\ bc{1} = CT_Binds_K ==> _) => //. proc; inline *. -rcondf{1} 2; 1: by move=> ?; call(: true). +do 2! (rcondf{1} 2; 1: by move=> ?; call(: true)). +swap{1} 2 -1; seq 1 0 : #pre; 1: by call{1} A_choose_ll. wp; call{1} S_decaps_ll; call{1} S_decaps_ll; call{1} A_find_ll. call{1} O1_init_ll; call{1} O0_init_ll. -by do 2! call (: true). +seq 1 1 : (#pre /\ HON_BIND_V.pk0{1} = pk0{2}); 1: by call (: true). +case (!HON_BIND_V.b{1}). ++ conseq (: _ ==> true) => //. + rcondf{1} 1; 1: by auto. + by wp; call{2} S_keygen_ll. +rcondt{1} 1; 1: by auto. +by call (: true). qed. end section. +(** Reduction adversary reducing LEAK-BIND-K-CT and LEAK-BIND-PKK-CT **) +module (R_LEAK_K_PKK_CT (A : Adv_LEAKBIND) : Adv_LEAKBIND) = { + proc choose(bc : bindconf) : bool = { + return false; + } + + proc find(bc : bindconf, pk0 : pk_t, sk0 : sk_t, pk1 : pk_t, sk1 : sk_t) : ctxt_t * ctxt_t = { + var c0, c1 : ctxt_t; + + (c0, c1) <@ A.find(PKK_Binds_CT, pk0, sk0, pk1, sk1); + + return (c0, c1); + } +}. + +(** + Equivalence between LEAK-BIND-PKK-CT (for arbitrary adversary) + and LEAK-BIND-K-CT (with above reduction adversary). + (Shows LEAK-BIND-K-CT --> LEAK-BIND-PKK-CT.) +**) +lemma Eqv_LEAK_PKK_K_CT (S <: Scheme) (A <: Adv_LEAKBIND{-S}): + equiv[LEAK_BIND(S, A).main ~ LEAK_BIND(S, R_LEAK_K_PKK_CT(A)).main : + ={glob S, glob A} /\ arg{1} = PKK_Binds_CT /\ arg{2} = K_Binds_CT ==> ={res}]. +proof. +proc; inline *. +wp; call (: true); call (: true) => /=. +wp; call (: true); wp. +rcondt{1} 2; 1: by move=> &m; call (: true). +do 2! (rcondf{2} 2; 1: by move=> &m; call (: true)). +rcondf{2} 4; 1: by move=> &m; wp; call (: true). +by wp; call (: true). +qed. + + (** Reduction adversary reducing LEAK-BIND-K-PK and LEAK-BIND-CT-PK to LEAK-BIND-KCT-PK **) module R_LEAK_K_CT_KCT_PK (A : Adv_LEAKBIND) : Adv_LEAKBIND = { + proc choose(bc : bindconf) : bool = { + return witness; + } + proc find(bc : bindconf, pk0 : pk_t, sk0 : sk_t, pk1 : pk_t, sk1 : sk_t) : ctxt_t * ctxt_t = { var c0, c1 : ctxt_t; @@ -3721,22 +3875,29 @@ lemma Eqv_LEAK_KCT_K_CT_PK (S <: Scheme) (A <: Adv_LEAKBIND{-S}): ={glob S, glob A} /\ arg{1} = KCT_Binds_PK /\ (arg{2} = K_Binds_PK \/ arg{2} = CT_Binds_PK) ==> res{1} => res{2}]. -proof. +proof. proc; inline *. wp; call (: true); call (: true). wp; call (: true); wp. seq 1 1 : (#pre /\ ={pk0, sk0}); 1: by call (: true). rcondf{1} 1; 1: by auto. rcondf{2} 1; 1: by auto => /> /#. -by call(: true); skip => /> /#. +rcondt{1} 1; 2: rcondt{2} 1; 1,2: by auto => /> /#. +by call (: true); skip => /> /#. qed. (** Reduction adversary reducing LEAK-BIND-CT-PK to LEAK-BIND-CT-K **) module R_LEAK_CT_PK_K (A : Adv_LEAKBIND) : Adv_LEAKBIND = { + proc choose(bc : bindconf) : bool = { + return witness; + } + proc find(bc : bindconf, pk0 : pk_t, sk0 : sk_t, pk1 : pk_t, sk1 : sk_t) : ctxt_t * ctxt_t = { + var b : bool; var c0, c1 : ctxt_t; + b <@ A.choose(CT_Binds_K); (c0, c1) <@ A.find(CT_Binds_K, pk0, sk0, pk1, sk1); return (c0, c1); @@ -3749,12 +3910,19 @@ section. declare module S <: Scheme. (* Losslessness (i.e., termination) assumption on S's decapsulation *) +declare axiom S_keygen_ll : islossless S.keygen. declare axiom S_decaps_ll : islossless S.decaps. +(* Determinism assumption on S's decapsulation *) +declare op s_decaps : sk_t -> ctxt_t -> key_t option. +declare axiom S_decaps_det (sk' : sk_t) (c' : ctxt_t) : + hoare[S.decaps : arg = (sk', c') ==> res = s_decaps sk' c']. + (* Declare arbtirary LEAK-BIND adversary A *) declare module A <: Adv_LEAKBIND{-S}. -(* Losslessness (i.e., termination) assumption on A's finding *) +(* Losslessness (i.e., termination) assumption on A's choosing and finding *) +declare axiom A_choose_ll : islossless A.choose. declare axiom A_find_ll : islossless A.find. (* @@ -3762,25 +3930,29 @@ declare axiom A_find_ll : islossless A.find. defined global instead of local (so we can refer to them in proofs). *) local module LEAK_BIND_V = { - var pk0 : pk_t - var pk1 : pk_t + var pk0, pk1 : pk_t + var b : bool proc main(bc : bindconf) : bool = { - - var sk0 : sk_t; - var sk1 : sk_t; - var c0 : ctxt_t; - var c1 : ctxt_t; - var k0 : key_t option; - var k1 : key_t option; + var sk0, sk1 : sk_t; + var c0, c1 : ctxt_t; + var k0, k1 : key_t option; var no_fail : bool; (pk0, sk0) <@ S.keygen(); - if (is_pkbc bc) { + + if (is_pkbsc bc) { (* public key is binding source, equalize key pairs *) (pk1, sk1) <- (pk0, sk0); - } else { + } elif (is_pkbtc bc) { (* public key is binding target, independently generate key pairs *) (pk1, sk1) <@ S.keygen(); - } + } else { (* neither of the above, let adversary choose what to do with key pairs *) + b <@ A.choose(bc); + if (b) { + (pk1, sk1) <@ S.keygen(); + } else { + (pk1, sk1) <- (pk0, sk0); + } + } (c0, c1) <@ A.find(bc, pk0, sk0, pk1, sk1); @@ -3817,20 +3989,51 @@ lemma Bnd_LEAK_CT_K_PK &m : + Pr[Keygen_Equal_PK(S).main() @ &m : res]. proof. -rewrite EqPr_LEAKBIND_V Pr[mu_split LEAK_BIND_V.pk0 <> LEAK_BIND_V.pk1] StdOrder.RealOrder.ler_add. +rewrite EqPr_LEAKBIND_V Pr[mu_split LEAK_BIND_V.b]. +have -> /=: + Pr[LEAK_BIND_V.main(CT_Binds_K) @ &m : res /\ !LEAK_BIND_V.b] = 0%r. ++ byphoare (: arg = CT_Binds_K ==> _) => //=. + hoare; proc. + do 2! (rcondf 2; 1: by call (: true)). + seq 2 : #pre; 1: by call (: true); call (: true). + case LEAK_BIND_V.b; 1: by conseq (: _ ==> true) => />. + rcondf 1 => //. + seq 2 : (#pre /\ sk0 = sk1 /\ LEAK_BIND_V.pk0 = LEAK_BIND_V.pk1). + + by sp 1; conseq (: _ ==> true) => />. + case (c0 = c1); 2: by conseq (: _ ==> true) => />. + exlim sk0, c0 => skt ct. + by wp; do 2! (call (S_decaps_det skt ct)). +rewrite Pr[mu_split LEAK_BIND_V.pk0 <> LEAK_BIND_V.pk1] StdOrder.RealOrder.ler_add. + byequiv (: ={glob S, glob A} /\ bc{1} = CT_Binds_K /\ bc{2} = CT_Binds_PK ==> _) => //. proc; inline *. seq 1 1 : (#pre /\ ={sk0} /\ LEAK_BIND_V.pk0{1} = pk0{2}); 1: by call (: true). - wp; call (: true); call (: true); wp. - call (: true); wp. - rcondf{1} 1; 1: by auto. + do 2! (rcondf{1} 1; 1: by auto). rcondf{2} 1; 1: by auto. - by call (: true). -byequiv => //. + rcondt{2} 1; 1: by auto. + swap{2} 7 -6. + seq 1 1 : (#pre /\ LEAK_BIND_V.b{1} = b0{2}); 1: by call (: true). + case (!LEAK_BIND_V.b{1}). + + conseq (: _ ==> true) => //. + rcondf{1} 1; 1: by auto. + wp; do 2! (call{1} S_decaps_ll; call{2} S_decaps_ll). + wp; call{1} A_find_ll; call{2} A_find_ll. + by wp; call{2} S_keygen_ll. + wp; call (: true); call (: true). + wp; call (: true). + rcondt{1} 1; 1: by auto. + by wp; call (: true); skip => />. +byequiv (: ={glob S} /\ bc{1} = CT_Binds_K ==> _) => //. proc; inline *. -rcondf{1} 2; 1: by move=> ?; call(: true). +do 2! (rcondf{1} 2; 1: by move=> ?; call(: true)). +swap{1} 2 -1; seq 1 0 : #pre; 1: by call{1} A_choose_ll. wp; call{1} S_decaps_ll; call{1} S_decaps_ll; call{1} A_find_ll. -by do 2! call (: true). +seq 1 1 : (#pre /\ LEAK_BIND_V.pk0{1} = pk0{2}); 1: by call (: true). +case (!LEAK_BIND_V.b{1}). ++ conseq (: _ ==> true) => //. + rcondf{1} 1; 1: by auto. + by wp; call{2} S_keygen_ll. +rcondt{1} 1; 1: by auto. +by call (: true). qed. end section. @@ -3964,5 +4167,5 @@ wp; call (: true); call (: true). by wp; call(: true); skip => /> /#. qed. - + end Relations. diff --git a/proofs/KeyEncapsulationMechanismsROM.eca b/proofs/KeyEncapsulationMechanismsROM.eca new file mode 100644 index 0000000..b4bee9d --- /dev/null +++ b/proofs/KeyEncapsulationMechanismsROM.eca @@ -0,0 +1,1476 @@ +(*^ + This library generically defines Key-Encapsulation Mechanisms (KEM) schemes + and their properties (both correctness and security) for proofs + in the Random Oracle Model (ROM). In essence, these are the + regular definitions (defined in KeyEncapsulationMechanisms.eca) extended + with a (single) random oracle compatible with the ones in PROM.ec. + For further details about the definitions for KEMs and/or + random oracles, refer to the respective theories. +^*) +(* Require/Import libraries *) +require import AllCore List PROM. +require (*--*) KeyEncapsulationMechanisms. + +(* Types *) +(** Public keys (asymmetric) **) +type pk_t. + +(** Secret keys (asymmetric) **) +type sk_t. + +(** Shared/session keys (symmetric) **) +type key_t. + +(** Ciphertexts/Encapsulations **) +type ctxt_t. + +(* Inputs to the random oracle *) +type in_t. + +(* Outputs of the random oracle *) +type out_t. + + +(* Clones and imports *) +(** Definitions and properties for KEMs (non-ROM) **) +clone import KeyEncapsulationMechanisms as KEMs with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t + + proof *. + +(** Definitions for random oracles **) +clone import FullRO as F_RO with + type in_t <- in_t, + type out_t <- out_t + + proof *. + + +(* + (Random) Oracles. + The definitions in this file only require "regular" random oracles that provide + an initialization functionality and a query functionality, i.e., no (re-)programmability. + Nevertheless, we do want the definitions to be compatible with the definitions used in + the main random oracle file of EC's standard library (PROM.ec). So, we simply take and + restrict the definitions from this file, limiting functionality but guaranteeing + compatability (importantly, any fundamental changes in PROM.ec will prevent this + file from being processed, which serves as an automatic compatibility check). +*) +(* + Type for (random) oracles used in security games, + exposing both the initialization functionality and the query functionality +*) +module type RandomOraclei = { + include RO [init, get] +}. + +(* + Type for (random) oracles used in schemes and given to adversaries, + exposing only the query functionality +*) +module type RandomOracle = { + include RandomOraclei [get] +}. + + +(* Schemes in ROM *) +(** KEM in ROM **) +module type Scheme_ROM (RO : RandomOracle) = { + include Scheme +}. + + +(* Correctness in ROM *) +(** Correctness program/game in ROM **) +module Correctness_ROM (RO : RandomOraclei) (S : Scheme_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ Correctness(S(RO)).main(); + + return r; + } +}. + + +(* Security in ROM *) +(* Attacker capabilities/models in ROM *) +(* + Chosen-Plaintext Attacks (CPA) in ROM. + The adversary is given the considered public key and, hence, + is able to produce encapsulations, i.e., (symmetric) key/ciphertext pairs. + (Typically, this means the adversary can construct ciphertexts + corresponding to chosen (symmetric) keys.) +*) + +(* + non-adaptive Chosen-Ciphertext Attacks (CCA1) in ROM. + The adversary is given the considered public key and access to a decryption oracle + *before* the stage in which it is expected to distinguish/return a break. + Hence, the adversary is able to produce encapsulations + *and* query for decryptions of chosen ciphertexts. +*) +(** Interface for oracles employed in CCA1 security games in ROM **) +module type Oracles_CCA1i_ROM (RO : RandomOracle) (S : Scheme) = { + proc init(sk_init : sk_t) : unit + proc decaps(c : ctxt_t) : key_t option +}. + + +(* + adaptive Chosen-Ciphertext Attacks (Traditional: CCA2, Modern : CCA) in ROM. + The adversary is given the considered public key and access to a decryption oracle throughout. + Hence, the adversary is able to produce encapsulations + *and* query for decryptions of chosen ciphertexts (potentially barring ciphertexts + that are part of the challenge). + Traditionally, this was analogous to CCA2 security for PKE schemes, meaning there were + two adversary stages: one before receiving the challenge (given a public key and access to a + non-restricted decapsulation oracle), and one after receiving the challenge (given access to a + restricted decapsulation oracle, i.e., one that prohibited querying the challenge). + Over time, the formalization shifted toward only considering the second adversary stage + (provding the public key(s) to this stage as well). + Here, we denote the traditional one by CCA2 (as we do for PKE schemes), and the modern one by CCA. +*) +(** Interface for oracles employed in CCA2 (CCA) security games in ROM **) +module type Oracles_CCA2i_ROM (RO : RandomOracle) (S : Scheme) = { + proc init(sk_init : sk_t, c'_init : ctxt_t) : unit + proc decaps(c : ctxt_t) : key_t option +}. + + +(* + One-Wayness (OW) in ROM. + The adversary is asked to produce the (symmetric) key + encapsulated by a given ciphertext. +*) +(* + One-Wayness under Chosen-Plaintext Attacks (OW-CPA) in ROM. + In a CPA setting, the adversary is asked to produce the (symmetric) key + encapsulated by a given ciphertext. +*) +(** Adversary class considered for OW-CPA in ROM **) +module type Adv_OWCPA_ROM (RO : RandomOracle) = { + include Adv_OWCPA +}. + +(** OW-CPA security game in ROM **) +module OW_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_OWCPA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ OW_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + + +(* + One-Wayness under non-adaptive Chosen-Ciphertext Attacks (OW-CCA1) in ROM. + In a CCA1 setting, the adversary is asked to produce the (symmetric) key + encapsulated by a given ciphertext. +*) +(** Adversary class considered for OW-CCA1 in ROM **) +module type Adv_OWCCA1_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit { O.decaps } + proc find(c : ctxt_t) : key_t { } +}. + +(** OW-CCA1 security game in ROM **) +module OW_CCA1_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA1i_ROM, A : Adv_OWCCA1_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ OW_CCA1(S(RO), O(RO), A(RO)).main(); + + return r; + } +}. + + +(* + One-Wayness under (traditional) adaptive Chosen-Ciphertext Attacks (OW-CCA2) in ROM. + In a (traditional) CCA2 setting, the adversary is asked to produce the (symmetric) key + encapsulated by a given ciphertext. +*) +(** Adversary class considered for OW-CCA2 in ROM **) +module type Adv_OWCCA2_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit + proc find(c : ctxt_t) : key_t +}. + +(** OW-CCA2 security game in ROM **) +module OW_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_OWCCA2_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ OW_CCA2(S(RO), O1(RO), O2(RO), A(RO)).main(); + + return r; + } +}. + + +(* + One-Wayness under (modern) adaptive Chosen-Ciphertext Attacks (OW-CCA) in ROM. + In a (modern) CCA2 setting, the adversary is asked to produce the (symmetric) key + encapsulated by a given ciphertext. +*) +(** Adversary class considered for OW-CCA (i.e., modern OW-CCA2) in ROM **) +module type Adv_OWCCA_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc find(pk : pk_t, c : ctxt_t) : key_t +}. + +(** OW-CCA (i.e., modern OW-CCA2) security game in ROM **) +module OW_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA2i_ROM, A : Adv_OWCCA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ OW_CCA(S(RO), O(RO), A(RO)).main(); + + return r; + } +}. + + +(** + (ciphertext) INDistinguishability (IND) in ROM. + The adversary is asked to determine whether a given + (symmetric) key is (1) encapsulated by a given ciphertext or (2) independently + sampled at random. +**) +abstract theory INDROM. +(* Distributions *) +(** (Sub-)Distribution over (symmetric) keys (may depend on public key) **) +(** + Dependence on public key may be used to, e.g., model cases where the key space + depends on the public key (like in the case of RSA). Instead of having the actual type + change depending on the public key (which, at the time of writing, is not possible in EC). +**) +op dkeym : pk_t -> key_t distr. + + +(* Clone and import definitions from IND theory (in non-ROM KEM theory) *) +clone import IND with + op dkeym <- dkeym + + proof *. + + +(* + (ciphertext) INDistinguishability under Chosen-Plaintext Attacks (IND-CPA) in ROM. + In a CPA setting, the adversary is asked to determine whether a given + (symmetric) key is (1) encapsulated by a given ciphertext or (2) independently + sampled at random (from dkeym). +*) +(** Adversary class considered for IND-CPA in ROM **) +module type Adv_INDCPA_ROM (RO : RandomOracle) = { + include Adv_INDCPA +}. + +(** IND-CPA security game (sampled bit) in ROM **) +module IND_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_INDCPA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + +(** IND-CPA security game (provided bit) in ROM **) +module IND_CPA_P_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_INDCPA_ROM) = { + proc main(b : bool) : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CPA_P(S(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + (ciphertext) INDistinguishability under non-adaptive Chosen-Ciphertext Attacks (IND-CCA1) in ROM. + In a CCA1 setting, the adversary is asked to determine whether a given + (symmetric) key is (1) encapsulated by a given ciphertext or (2) independently + sampled at random (from dkeym). +*) +(** Adversary class considered for IND-CCA1 in ROM **) +module type Adv_INDCCA1_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit { O.decaps } + proc distinguish(k : key_t, c : ctxt_t) : bool { } +}. + +(** IND-CCA1 security game (sampled bit) in ROM **) +module IND_CCA1_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA1i_ROM, A : Adv_INDCCA1_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CCA1(S(RO), O(RO), A(RO)).main(); + + return r; + } +}. + +(** IND-CCA1 security game (provided bit) in ROM **) +module IND_CCA1_P_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA1i_ROM, A : Adv_INDCCA1_ROM) = { + proc main(b : bool) : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CCA1_P(S(RO), O(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + (ciphertext) INDistinguishability under (traditional) adaptive Chosen-Ciphertext Attacks (IND-CCA2) in ROM. + In a (traditional) CCA2 setting, the adversary is asked to determine whether a given + (symmetric) key is (1) encapsulated by a given ciphertext or (2) independently + sampled at random (from dkeym). +*) +(** Adversary class considered for IND-CCA2 in ROM **) +module type Adv_INDCCA2_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit + proc distinguish(k : key_t, c : ctxt_t) : bool +}. + +(** IND-CCA2 security game (sampled bit) in ROM **) +module IND_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_INDCCA2_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CCA2(S(RO), O1(RO), O2(RO), A(RO)).main(); + + return r; + } +}. + +(** IND-CCA2 security game (provided bit) in ROM **) +module IND_CCA2_P_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_INDCCA2_ROM) = { + proc main(b : bool) : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CCA2_P(S(RO), O1(RO), O2(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + (ciphertext) INDistinguishability under (modern) adaptive Chosen-Ciphertext Attacks (IND-CCA2) in ROM. + In a (modern) CCA2 setting, the adversary is asked to determine whether a given + (symmetric) key is (1) encapsulated by a given ciphertext or (2) independently + sampled at random (from dkeym). +*) +(** Adversary class considered for IND-CCA (i.e., modern IND-CCA2) in ROM **) +module type Adv_INDCCA_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc distinguish(pk : pk_t, k : key_t, c : ctxt_t) : bool +}. + +(** IND-CCA (i.e., modern IND-CCA2) security game (sampled bit) in ROM **) +module IND_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA2i_ROM, A : Adv_INDCCA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CCA(S(RO), O(RO), A(RO)).main(); + + return r; + } +}. + +(** IND-CCA (i.e., modern IND-CCA2) security game (provided bit) in ROM **) +module IND_CCA_P_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA2i_ROM, A : Adv_INDCCA_ROM) = { + proc main(b : bool) : bool = { + var r : bool; + + RO.init(); + + r <@ IND_CCA_P(S(RO), O(RO), A(RO)).main(b); + + return r; + } +}. + +end INDROM. + + +(** + (ciphertext) Non-Malleability (NM) in ROM. + Given a ciphertext (encapsulating some key K), the adversary is + asked to provide a relation R and a list of ciphertexts such that the (symmetric) keys + resulting from decapsulating the ciphertexts (in the list) are related (through R) with + K (significantly) more often than with a (symmetric) key that is independently sampled + at random. + + (ciphertext) Strong Non-Malleability (SNM) + As NM-CPA, but the adversary is additionally given a pair of (symmetric) keys of + which one is independently sampled at random, and the other is the one + encapsulated by the given ciphertext. (The order in which they appear in the pair + is (uniformly) random). + + Note that these notions only have a sensible definition with a provided bit, so + no "sampled bit" variants are defined. +**) +abstract theory NMROM. +(* Distributions *) +(** (Sub-)Distribution over (symmetric) keys (may depend on public key) **) +(** + Dependence on public key may be used to, e.g., model cases where the key space + depends on the public key (like in the case of RSA). Instead of having the actual type + change depending on the public key (which, at the time of writing, is not possible in EC). +**) +op dkeym : pk_t -> key_t distr. + + +(* Clone and import definitions from NM theory (in non-ROM KEM theory) *) +clone import NM with + op dkeym <- dkeym + + proof *. + + +(* + (ciphertext) Non-Malleability under Chosen-Plaintext Attacks (NM-CPA) in ROM. + In a CPA setting, given a ciphertext (encapsulating some key K), the adversary is + asked to provide a relation R and a list of ciphertexts such that the (symmetric) keys + resulting from decapsulating the ciphertexts (in the list) are related (through R) with + K (significantly) more often than with a (symmetric) key that is independently sampled + at random. +*) +(** Adversary class considered for NM-CPA in ROM **) +module type Adv_NMCPA_ROM (RO : RandomOracle) = { + include Adv_NMCPA +}. + +(** NM-CPA security game in ROM **) +module NM_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_NMCPA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ NM_CPA(S(RO), A(RO)).main(b); + + return r; + } +}. + +(* + (ciphertext) Strong Non-Malleability under Chosen-Plaintext Attacks (SNM-CPA) in ROM. + As NM-CPA, but the adversary is additionally given a pair of (symmetric) keys of + which one is independently sampled at random, and the other is the one + encapsulated by the given ciphertext. (The order in which they appear in the pair + is (uniformly) random). +*) +(** Adversary class considered for SNM-CPA in ROM **) +module type Adv_SNMCPA_ROM (RO : RandomOracle) = { + include Adv_SNMCPA +}. + +(** SNM-CPA security game in ROM **) +module SNM_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_SNMCPA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ SNM_CPA(S(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + (ciphertext) Non-Malleability under non-adaptive Chosen-Ciphertext Attacks (NM-CCA1) in ROM. + In a CCA1 setting, given a ciphertext (encapsulating some key K), the adversary is + asked to provide a relation R and a list of ciphertexts such that the (symmetric) keys + resulting from decapsulating the ciphertexts (in the list) are related (through R) with + K (significantly) more often than with a (symmetric) key that is independently sampled + at random. +*) +(** Adversary class considered for NM-CCA1 in ROM **) +module type Adv_NMCCA1_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit { O.decaps } + proc find(c : ctxt_t) : (key_t -> key_t option list -> bool) * ctxt_t list { } +}. + +(** NM-CCA1 security game in ROM **) +module NM_CCA1_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA1i_ROM, A : Adv_NMCCA1_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ NM_CCA1(S(RO), O(RO), A(RO)).main(b); + + return r; + } +}. + +(* + (ciphertext) Strong Non-Malleability under non-adaptive Chosen-Ciphertext Attacks (SNM-CCA1) in ROM. + As NM-CCA1, but the adversary is additionally given a pair of (symmetric) keys of + which one is independently sampled at random, and the other is the one + encapsulated by the given ciphertext. (The order in which they appear in the pair + is (uniformly) random). +*) +(** Adversary class considered for SNM-CCA1 in ROM **) +module type Adv_SNMCCA1_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit { O.decaps } + proc find(c : ctxt_t, kk : key_t * key_t) : (key_t -> key_t option list -> bool) * ctxt_t list { } +}. + +(** SNM-CCA1 security game in ROM **) +module SNM_CCA1_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA1i_ROM, A : Adv_SNMCCA1_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ SNM_CCA1(S(RO), O(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + (ciphertext) Non-Malleability under (traditional) adaptive Chosen-Ciphertext Attacks (NM-CCA2) in ROM. + In a (traditional) CCA2 setting, given a ciphertext (encapsulating some key K), the adversary is + asked to provide a relation R and a list of ciphertexts such that the (symmetric) keys + resulting from decapsulating the ciphertexts (in the list) are related (through R) with + K (significantly) more often than with a (symmetric) key that is independently sampled + at random. +*) +(** Adversary class considered for NM-CCA2 in ROM **) +module type Adv_NMCCA2_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit + proc find(c : ctxt_t) : (key_t -> key_t option list -> bool) * ctxt_t list +}. + +(** NM-CCA2 security game in ROM **) +module NM_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_NMCCA2_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ NM_CCA2(S(RO), O1(RO), O2(RO), A(RO)).main(b); + + return r; + } +}. + +(* + (ciphertext) Strong Non-Malleability under (traditional) adaptive Chosen-Ciphertext Attacks (SNM-CCA2) in ROM. + As NM-CCA2, but the adversary is additionally given a pair of (symmetric) keys of + which one is independently sampled at random, and the other is the one + encapsulated by the given ciphertext. (The order in which they appear in the pair + is (uniformly) random). +*) +(** Adversary class considered for SNM-CCA2 in ROM **) +module type Adv_SNMCCA2_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc scout(pk : pk_t) : unit + proc find(c : ctxt_t, kk : key_t * key_t) : (key_t -> key_t option list -> bool) * ctxt_t list +}. + +(** SNM-CCA2 security game in ROM **) +module SNM_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_SNMCCA2_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ SNM_CCA2(S(RO), O1(RO), O2(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + (ciphertext) Non-Malleability under (modern) adaptive Chosen-Ciphertext Attacks (NM-CCA) in ROM. + In a (modern) CCA2 setting, given a ciphertext (encapsulating some key K), the adversary is + asked to provide a relation R and a list of ciphertexts such that the (symmetric) keys + resulting from decapsulating the ciphertexts (in the list) are related (through R) with + K (significantly) more often than with a (symmetric) key that is independently sampled + at random. +*) +(** Adversary class considered for NM-CCA (i.e., modern NM-CCA2) in ROM **) +module type Adv_NMCCA_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc find(pk : pk_t, c : ctxt_t) : (key_t -> key_t option list -> bool) * ctxt_t list +}. + +(** NM-CCA (i.e., modern NM-CCA2) security game in ROM **) +module NM_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA2i_ROM, A : Adv_NMCCA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ NM_CCA(S(RO), O(RO), A(RO)).main(b); + + return r; + } +}. + +(* + (ciphertext) Strong Non-Malleability under (modern) adaptive Chosen-Ciphertext Attacks (SNM-CCA) in ROM. + As NM-CCA, but the adversary is additionally given a pair of (symmetric) keys of + which one is independently sampled at random, and the other is the one + encapsulated by the given ciphertext. (The order in which they appear in the pair + is (uniformly) random). +*) +(** Adversary class considered for SNM-CCA (i.e., modern SNM-CCA2) in ROM **) +module type Adv_SNMCCA_ROM (RO : RandomOracle) (O : Oracles_CCA) = { + proc find(pk : pk_t, c : ctxt_t, kk : key_t * key_t) : (key_t -> key_t option list -> bool) * ctxt_t list +}. + +(** SNM-CCA (i.e., modern SNM-CCA2) security game in ROM **) +module SNM_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM, O : Oracles_CCA2i_ROM, A : Adv_SNMCCA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ SNM_CCA(S(RO), O(RO), A(RO)).main(b); + + return r; + } +}. + +end NMROM. + + +(* + ANOnymity (ANO) in ROM. + The adversary is given two (honestly generated) public keys and an encapsulation + (i.e., ciphertext/key pair), and asked to determine which public key was used to + create the encapsulation. + + Weak ANOnymity (WANO) in ROM. + As ANO, but the adversary is only given the ciphertext of the encapsulation + (i.e., not the key). +*) +(* + ANOnymity under Chosen-Plaintext attack (ANO-CPA) in ROM. + In a CPA setting, The adversary is given two (honestly generated) public keys + and an encapsulation (i.e., key/ciphertext pair), and asked to determine which + public key was used to create the encapsulation. +*) +(** Adversary class considerd for ANO-CPA in ROM **) +module type Adv_ANOCPA_ROM (RO : RandomOracle) = { + include Adv_ANOCPA +}. + +(** ANO-CPA security game (sampled bit) in ROM **) +module ANO_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_ANOCPA_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ ANO_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + +(** ANO-CPA security game (provided bit) in ROM **) +module ANO_CPA_P_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_ANOCPA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ ANO_CPA_P(S(RO), A(RO)).main(b); + + return r; + } +}. + +(* + Weak ANOnymity under Chosen-Plaintext attack (WANO-CPA) in ROM. + As ANO-CPA, but the adversary is only given the ciphertext of the encapsulation + (i.e., not the key). +*) +(** Adversary class considerd for WANO-CPA in ROM **) +module type Adv_WANOCPA_ROM (RO : RandomOracle) = { + include Adv_WANOCPA +}. + +(** WANO-CPA security game (sampled bit) in ROM **) +module WANO_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_WANOCPA_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ WANO_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + +(** WANO-CPA security game (provided bit) in ROM **) +module WANO_CPA_P_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_WANOCPA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ WANO_CPA_P(S(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + ANOnymity under non-adaptive Chosen-Plaintext attack (ANO-CCA1) in ROM. + In a CCA1 setting, the adversary is given (in the first stage) two (honestly generated) public keys + and (in the second stage) an encapsulation (i.e., key/ciphertext pair), and is + asked to determine which public key was used to create the encapsulation. +*) +(** Adversary class considerd for ANO-CCA1 in ROM **) +module type Adv_ANOCCA1_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc scout(pk0 : pk_t, pk1 : pk_t) : unit{ O0.decaps, O1.decaps } + proc distinguish(kc : key_t * ctxt_t) : bool { } +}. + +(** ANO-CCA1 security game (sampled bit) in ROM **) +module ANO_CCA1_ROM (RO : RandomOraclei) (S : Scheme_ROM, O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, A : Adv_ANOCCA1_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ ANO_CCA1(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + +(** ANO-CCA1 security game (provided bit) in ROM **) +module ANO_CCA1_P_ROM (RO : RandomOraclei) (S : Scheme_ROM, O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, A : Adv_ANOCCA1_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ ANO_CCA1_P(S(RO), O0(RO), O1(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + Weak ANOnymity under non-adaptive Chosen-Plaintext attack (WANO-CCA1) in ROM. + As ANO-CCA1, but the adversary is only given the ciphertext of the encapsulation + (i.e., not the key). +*) +(** Adversary class considerd for WANO-CCA1 in ROM **) +module type Adv_WANOCCA1_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc scout(pk0 : pk_t, pk1 : pk_t) : unit{ O0.decaps, O1.decaps } + proc distinguish(c : ctxt_t) : bool { } +}. + +(** WANO-CCA1 security game (sampled bit) in ROM **) +module WANO_CCA1_ROM (RO : RandomOraclei) (S : Scheme_ROM, O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, A : Adv_WANOCCA1_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ WANO_CCA1(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + +(** WANO-CCA1 security game (provided bit) in ROM **) +module WANO_CCA1_P_ROM (RO : RandomOraclei) (S : Scheme_ROM, O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, A : Adv_WANOCCA1_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ WANO_CCA1_P(S(RO), O0(RO), O1(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + ANOnymity under (traditional) adaptive Chosen-Plaintext attack (ANO-CCA2) in ROM. + In a (traditional) CCA2 setting, the adversary is given (in the first stage) two + (honestly generated) public keys and (in the second stage) an encapsulation + (i.e., key/ciphertext pair), and is + asked to determine which public key was used to create the encapsulation. +*) +(** Adversary class considerd for ANO-CCA2 in ROM **) +module type Adv_ANOCCA2_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc scout(pk0 : pk_t, pk1 : pk_t) : unit + proc distinguish(kc : key_t * ctxt_t) : bool +}. + +(** ANO-CCA2 security game (sampled bit) in ROM **) +module ANO_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O01 : Oracles_CCA1i_ROM, O11 : Oracles_CCA1i_ROM) + (O02 : Oracles_CCA2i_ROM, O12 : Oracles_CCA2i_ROM) + (A : Adv_ANOCCA2_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ ANO_CCA2(S(RO), O01(RO), O11(RO), O02(RO), O12(RO), A(RO)).main(); + + return r; + } +}. + +(** ANO-CCA2 security game (provided bit) in ROM **) +module ANO_CCA2_P_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O01 : Oracles_CCA1i_ROM, O11 : Oracles_CCA1i_ROM) + (O02 : Oracles_CCA2i_ROM, O12 : Oracles_CCA2i_ROM) + (A : Adv_ANOCCA2_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ ANO_CCA2_P(S(RO), O01(RO), O11(RO), O02(RO), O12(RO), A(RO)).main(b); + + return r; + } +}. + +(* + Weak ANOnymity under (traditional) adaptive Chosen-Plaintext attack (WANO-CCA2) in ROM. + As ANO-CCA2, but the adversary is only given the ciphertext of the encapsulation + (i.e., not the key). +*) +(** Adversary class considerd for WANO-CCA2 in ROM **) +module type Adv_WANOCCA2_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc scout(pk0 : pk_t, pk1 : pk_t) : unit + proc distinguish(c : ctxt_t) : bool +}. + +(** WANO-CCA2 security game (sampled bit) in ROM **) +module WANO_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O01 : Oracles_CCA1i_ROM, O11 : Oracles_CCA1i_ROM) + (O02 : Oracles_CCA2i_ROM, O12 : Oracles_CCA2i_ROM) + (A : Adv_WANOCCA2_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ WANO_CCA2(S(RO), O01(RO), O11(RO), O02(RO), O12(RO), A(RO)).main(); + + return r; + } +}. + +(** WANO-CCA2 security game (provided bit) in ROM **) +module WANO_CCA2_P_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O01 : Oracles_CCA1i_ROM, O11 : Oracles_CCA1i_ROM) + (O02 : Oracles_CCA2i_ROM, O12 : Oracles_CCA2i_ROM) + (A : Adv_WANOCCA2_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ WANO_CCA2_P(S(RO), O01(RO), O11(RO), O02(RO), O12(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + ANOnymity under (modern) adaptive Chosen-Plaintext attack (ANO-CCA) in ROM. + In a (modern) CCA setting, the adversary is given (in the first stage) two + (honestly generated) public keys and (in the second stage) an encapsulation + (i.e., key/ciphertext pair), and is + asked to determine which public key was used to create the encapsulation. +*) +(** Adversary class considerd for ANO-CCA (i.e., modern ANO-CCA2) in ROM **) +module type Adv_ANOCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc distinguish(pk0 : pk_t, pk1 : pk_t, kc : key_t * ctxt_t) : bool +}. + +(** ANO-CCA (i.e., modern ANO-CCA2) security game (sampled bit) in ROM **) +module ANO_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA2i_ROM, O1 : Oracles_CCA2i_ROM) + (A : Adv_ANOCCA_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ ANO_CCA(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + +(** ANO-CCA (i.e., modern ANO-CCA2) security game (provided bit) in ROM **) +module ANO_CCA_P_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA2i_ROM, O1 : Oracles_CCA2i_ROM) + (A : Adv_ANOCCA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ ANO_CCA_P(S(RO), O0(RO), O1(RO), A(RO)).main(b); + + return r; + } +}. + +(* + Weak ANOnymity under (modern) adaptive Chosen-Plaintext attack (WANO-CCA) in ROM. + As ANO-CCA2, but the adversary is only given the ciphertext of the encapsulation + (i.e., not the key). +*) +(** Adversary class considerd for ANO-CCA (i.e., modern ANO-CCA2) in ROM **) +module type Adv_WANOCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc distinguish(pk0 : pk_t, pk1 : pk_t, c : ctxt_t) : bool +}. + +(** WANO-CCA (i.e., modern WANO-CCA2) security game (sampled bit) in ROM **) +module WANO_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA2i_ROM, O1 : Oracles_CCA2i_ROM) + (A : Adv_WANOCCA_ROM) = { + proc main() = { + var r : bool; + + RO.init(); + + r <@ WANO_CCA(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + +(** WANO-CCA (i.e., modern WANO-CCA2) security game (provided bit) in ROM **) +module WANO_CCA_P_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA2i_ROM, O1 : Oracles_CCA2i_ROM) + (A : Adv_WANOCCA_ROM) = { + proc main(b : bool) = { + var r : bool; + + RO.init(); + + r <@ WANO_CCA_P(S(RO), O0(RO), O1(RO), A(RO)).main(b); + + return r; + } +}. + + +(* + Strong ROBustness (SROB) in ROM. + The adversary is given two (honestly generated) public keys and is asked to + provide a (single) ciphertext that decapsulates to valid symmetric keys under both + of the secret keys (corresponding to the provided public keys). + + Weak ROBustness (WROB) in ROM. + The adversary is given two (honestly generated) public keys and is asked to choose + which one to use for encapsulation and which one to use (the corresponding secret key of) + for decapsulation. Here, the goal is that the decapsulation (with the key appointed for + decapsulation) of the encapsulation (created with the key appointed for encapsulation) succeeds + (i.e., returns a valid symmetric key). + + Note, as there is no stage in which the adversary is given a distinct challenge artifact, it does + not make sense to have different CCA1/CCA2 settings for these properties. Instead, + we only consider a CPA setting (no decapsulation oracle) and a CCA setting (a decapsulation + oracle like in CCA1, i.e., no considered challenge). +*) +(* + Strong ROBustness under Chosen-Plaintext Attacks (SROB-CPA) in ROM. + In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to + provide a (single) ciphertext that decapsulates to valid symmetric keys under both + of the secret keys (corresponding to the provided public keys). +*) +(** Adversary class considered for SROB-CPA in ROM **) +module type Adv_SROBCPA_ROM (RO : RandomOracle) = { + include Adv_SROBCPA +}. + +(** SROB-CPA security game in ROM **) +module SROB_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_SROBCPA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ SROB_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + +(* + Weak ROBustness under Chosen-Plaintext Attacks (WROB-CPA) in ROM. + In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to choose + which one to use for encapsulation and which one to use (the corresponding secret key of) + for decapsulation. Here, the goal is that the decapsulation (with the key appointed for + decapsulation) of the encapsulation (created with the key appointed for encapsulation) succeeds + (i.e., returns a valid symmetric key). +*) +(** Adversary class considered for WROB-CPA in ROM **) +module type Adv_WROBCPA_ROM (RO : RandomOracle) = { + include Adv_WROBCPA +}. + +(** WROB-CPA security game in ROM **) +module WROB_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_WROBCPA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ WROB_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + + +(* + Strong ROBustness under Chosen-Ciphertext Attacks (SROB-CCA) in ROM. + In a CCA setting, the adversary is given two (honestly generated) public keys and is asked to + provide a (single) ciphertext that decapsulates to valid symmetric keys under both + of the secret keys (corresponding to the provided public keys). +*) +(** Adversary class considered for SROB-CCA in ROM **) +module type Adv_SROBCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc find(pk0 : pk_t, pk1 : pk_t) : ctxt_t +}. + +(** SROB-CCA security game in ROM **) +module SROB_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_SROBCCA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ SROB_CCA(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + +(* + Weak ROBustness under Chosen-Ciphertext Attacks (WROB-CCA) in ROM. + In a CCA setting, the adversary is given two (honestly generated) public keys and is asked to choose + which one to use for encapsulation and which one to use (the corresponding secret key of) + for decapsulation. Here, the goal is that the decapsulation (with the key appointed for + decapsulation) of the encapsulation (created with the key appointed for encapsulation) succeeds + (i.e., returns a valid symmetric key). +*) +(** Adversary class considered for WROB-CCA in ROM **) +module type Adv_WROBCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(pk0 : pk_t, pk1 : pk_t) : bool +}. + +(** WROB-CCA security game in ROM **) +module WROB_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_WROBCCA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ WROB_CCA(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + + +(* + Strong Collision-FReeness (SCFR) in ROM. + As SROB, but additionally requires the resulting symmetric keys to be + equal to eachother (instead of only requiring these keys to be valid). + + Weak Collision-FReeness (WCFR) in ROM. + As WROB, but additionally requires the resulting symmetric keys to be + equal to eachother (instead of only requiring the final decapsulated key to be valid). +*) +(* + Strong Collision-FReeness under Chosen-Plaintext Attacks (SCFR-CPA) in ROM. + In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to + provide a (single) ciphertext that decapsulates to the same valid symmetric key under both + of the secret keys (corresponding to the provided public keys). +*) +(** Adversary class considered for SCFR-CPA in ROM **) +module type Adv_SCFRCPA_ROM (RO : RandomOracle) = { + include Adv_SCFRCPA +}. + +(** SCFR-CPA security game in ROM **) +module SCFR_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_SCFRCPA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ SCFR_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + +(* + Weak Collision-FReeness under Chosen-Plaintext Attacks (WCFR-CPA) in ROM. + In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to choose + which one to use for encapsulation and which one to use (the corresponding secret key of) + for decapsulation. Here, the goal is that the decapsulation (with the key appointed for + decapsulation) of the encapsulation (created with the key appointed for encapsulation) returns + a valid symmetric key that is equal to the encapsulated one. +*) +(** Adversary class considered for WCFR-CPA in ROM **) +module type Adv_WCFRCPA_ROM (RO : RandomOracle) = { + include Adv_WCFRCPA +}. + +(** WCFR-CPA security game in ROM **) +module WCFR_CPA_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_WCFRCPA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ WCFR_CPA(S(RO), A(RO)).main(); + + return r; + } +}. + + +(* + Strong Collision-FReeness under Chosen-Ciphertext Attacks (SCFR-CCA) in ROM. + In a CCA setting, the adversary is given two (honestly generated) public keys and is asked to + provide a (single) ciphertext that decapsulates to the same valid symmetric key under both + of the secret keys (corresponding to the provided public keys). +*) +(** Adversary class considered for SCFR-CCA in ROM **) +module type Adv_SCFRCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc find(pk0 : pk_t, pk1 : pk_t) : ctxt_t +}. + +(** SCFR-CCA security game in ROM **) +module SCFR_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_SCFRCCA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ SCFR_CCA(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + +(* + Weak ROBustness under Chosen-Ciphertext Attacks (WCFR-CCA) in ROM. + In a CCA setting, the adversary is given two (honestly generated) public keys and is asked to choose + which one to use for encapsulation and which one to use (the corresponding secret key of) + for decapsulation. Here, the goal is that the decapsulation (with the key appointed for + decapsulation) of the encapsulation (created with the key appointed for encapsulation) returns + a valid symmetric key that is equal to the encapsulated one. +*) +(** Adversary class considered for WCFR-CCA in ROM **) +module type Adv_WCFRCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(pk0 : pk_t, pk1 : pk_t) : bool +}. + +(** WCFR-CCA security game **) +module WCFR_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_WCFRCCA_ROM) = { + proc main() : bool = { + var r : bool; + + RO.init(); + + r <@ WCFR_CCA(S(RO), O0(RO), O1(RO), A(RO)).main(); + + return r; + } +}. + + +(* + BINDing (BIND) in ROM. + Intuitively, binding properties capture to which extent certain artifacts (in a + a non-failing KEM execution) determine other artifacts (in that same execution). + That is, informally, an artifact (e.g., symmetric key) binds another artifact (e.g., a ciphertext) + if seeing a certain value for the symmetric key (without failing) implies that the ciphertext is actually + the one corresponding to this symmetric key (because it is hard to find another one that decapsulates to the + same symmetric key without failing). + Depending on the adversarial model, the artifacts used as input to the KEM's procedures + are either honestly or maliciously generated. +*) +(* + HONestly BINDing (HON-BIND) in ROM. + Binding properties where the adversary is given two honestly generated public keys, + as well as a decapsulation oracle with which it can decapsulate + w.r.t. the corresponding secret keys. +*) +(** Adversary class considered for HON-BIND **) +module type Adv_HONBIND_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(bc : bindconf) : bool { RO.get } + proc find(bc : bindconf, pk0 : pk_t, pk1 : pk_t) : ctxt_t * ctxt_t +}. + +(** HON-BIND security game (specific configuration is passed to the procedure) **) +module HON_BIND_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_HONBIND_ROM) = { + proc main(bc : bindconf) = { + var r : bool; + + RO.init(); + + r <@ HON_BIND(S(RO), O0(RO), O1(RO), A(RO)).main(bc); + + return r; + } +}. + + +(* + LEAKingly BINDing (LEAK-BIND) in ROM. + Binding properties where the adversary is given two + honestly generated (asymmetric) key pairs. +*) +(** Adversary class considered for LEAK-BIND **) +module type Adv_LEAKBIND_ROM (RO : RandomOracle) = { + include Adv_LEAKBIND +}. + +(** LEAK-BIND security game (specific configuration is passed to the procedure) **) +module LEAK_BIND_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_LEAKBIND_ROM) = { + proc main(bc : bindconf) = { + var r : bool; + + RO.init(); + + r <@ LEAK_BIND(S(RO), A(RO)).main(bc); + + return r; + } +}. + + +(** + MALiciously BINDing (MAL-BIND) in ROM. + Binding properties where the adversary provides the + considered (asymmetric) key material itself. +**) +abstract theory MALBINDROM. +(* Operators *) +(** Derives (honestly) the public key corresponding to a secret key **) +(** + Using this, we can let the adversary (in the MAL-BIND properties) only provide + the to-be-considered (asymmetric) secret keys, and then honestly compute + the corresponding public key ourselves. This allows + us to meaningfully include binding properties involving the public key. +**) +(** + Note: for the properties to make sense, this operator + should be instantiated to something that actually derives + public keys from (honestly generated) secret keys for the considered KEM. +**) +op sk2pk : sk_t -> pk_t. + + +(* Clone and import definitions from MALBIND theory (in non-ROM KEM theory) *) +clone import MALBIND with + op sk2pk <- sk2pk + + proof *. + + +(* + MALiciously BINDing w.r.t. Decapsulation/Decapsulation (MAL-BIND-DD) in ROM. + In a MAL-BIND setting, the adversary is asked to provide two ciphertext + (to be decapsulated) as to induce a binding break (w.r.t. the considered configuration). +*) +(** Adversary class considered for MAL-BIND-DD in ROM **) +module type Adv_MALBIND_DD_ROM (RO : RandomOracle) = { + include Adv_MALBIND_DD +}. + +(** MAL-BIND-DD security game (specific configuration is passed to the procedure) in ROM **) +module MAL_BIND_DD_ROM (RO : RandomOraclei) (S : Scheme_ROM, A : Adv_MALBIND_DD_ROM) = { + proc main(bc : bindconf) : bool = { + var r : bool; + + RO.init(); + + r <@ MAL_BIND_DD(S(RO), A(RO)).main(bc); + + return r; + } +}. + + +(* + In the remaining MAL-BIND properties, the adversary is asked to provide + the randomness used in encapsulation(s). That is, these properties need + to consider "derandomized" encapsulation procedures, taking the randomness + as additional input (instead of generating it on the fly). + To this end, we specify a module type for KEMs that is identical to the + original one with an appropriately adjusted encapsulation procedure. + Be aware that the following properties only make sense for KEMs of which + the encapsulation procedure actually employs the provided randomness. + (This is not actually enforced by the module type.) +*) +(* Types *) +(** Randomness (for encapsulation procedure) **) +type rand_t. + + +(* Module types *) +(** "Derandomized" KEM (interface) in ROM **) +module type SchemeDerand_ROM (RO : RandomOracle) = { + include SchemeDerand +}. + + +(* + MALiciously BINDing w.r.t. Encapsulation/Decapsulation (MAL-BIND-ED) in ROM. + In a MAL-BIND setting, the adversary is asked to provide + randomness and a ciphertext (to be used in encapsulation and + decapsulation, respectively) as to induce a binding break + (w.r.t. the considered configuration). +*) +(** Adversary class considered for MAL-BIND-ED in ROM **) +module type Adv_MALBIND_ED_ROM (RO : RandomOracle) = { + include Adv_MALBIND_ED +}. + +(** MAL-BIND-ED security game (specific configuration is passed to the procedure) in ROM **) +module MAL_BIND_ED_ROM (RO : RandomOraclei) (S : SchemeDerand_ROM, A : Adv_MALBIND_ED_ROM) = { + proc main(bc : bindconf) : bool = { + var r : bool; + + RO.init(); + + r <@ MAL_BIND_ED(S(RO), A(RO)).main(bc); + + return r; + } +}. + + +(* + MALiciously BINDing w.r.t. Encapsulation/Encapsulation (MAL-BIND-EE) in ROM. + In a MAL-BIND setting, the adversary is asked to provide + randomness (to be used in encapsulations) as to induce a binding break + (w.r.t. the considered configuration). +*) +(** Adversary class considered for MAL-BIND-EE in ROM **) +module type Adv_MALBIND_EE_ROM (RO : RandomOracle) = { + include Adv_MALBIND_EE +}. + +(** MAL-BIND-EE security game (specific configuration is passed to the procedure) **) +module MAL_BIND_EE_ROM (RO : RandomOraclei) (S : SchemeDerand_ROM, A : Adv_MALBIND_EE_ROM) = { + proc main(bc : bindconf) : bool = { + var r : bool; + + RO.init(); + + r <@ MAL_BIND_EE(S(RO), A(RO)).main(bc); + + return r; + } +}. + + +(* + MALiciously BINDing w.r.t. any of DD, ED, or EE (MAL-BIND) in ROM. + The adversary is asked to choose any of the MAL-BIND scenarios (DD, DE, or EE) + and provide values that induce a binding break + (w.r.t. the considered configuration) for that scenario. +*) +(* Can potentially reuse things specific to MALBIND scenarios in general MALBIND game by tweaking interfaces, but may hurt readability quite a bit *) +(** Adversary class considered for MAL-BIND in ROM **) +module type Adv_MALBIND_ROM (RO : RandomOracle) = { + include Adv_MALBIND +}. + +(** MAL-BIND security game (specific configuration is passed to the procedure) in ROM**) +module MAL_BIND_ROM (RO : RandomOraclei) (S : SchemeDerand_ROM, A : Adv_MALBIND_ROM) = { + proc main(bc : bindconf) : bool = { + var r : bool; + + RO.init(); + + r <@ MAL_BIND(S(RO), A(RO)).main(bc); + + return r; + } +}. + +end MALBINDROM. + diff --git a/proofs/PublicKeyEncryption.eca b/proofs/PublicKeyEncryption.eca index 2ff12bc..f40b545 100644 --- a/proofs/PublicKeyEncryption.eca +++ b/proofs/PublicKeyEncryption.eca @@ -11,7 +11,7 @@ - [Anonymous, Robust Post-Quantum Public Key Encryption](https://eprint.iacr.org/2021/708) - [A Modular Analysis of the Fujisaki-Okamoto Transformation](https://eprint.iacr.org/2017/604) - [Completely Non-Malleable Encryption Revisited](https://iacr.org/archive/pkc2008/49390068/49390068.pdf) - (TODO: Add more niche properties (complete non-malleability, plaintext awareness))) + (Missing properties: complete non-malleability, plaintext awareness) ^*) (* Require/Import libraries *) diff --git a/proofs/PublicKeyEncryptionROM.eca b/proofs/PublicKeyEncryptionROM.eca index 30a39f9..83ac572 100644 --- a/proofs/PublicKeyEncryptionROM.eca +++ b/proofs/PublicKeyEncryptionROM.eca @@ -5,7 +5,7 @@ regular definitions (defined in PublicKeyEncryption.eca) extended with a (single) random oracle compatible with the ones in PROM.ec. For further details about the definitions for PKE schemes and/or - random oracles, refer to the respective, aforementioned theories. + random oracles, refer to the respective theories. ^*) (* Require/Import libraries *) require import AllCore List PROM. @@ -33,7 +33,7 @@ type out_t. (* Clones and imports *) -(** Definitions and properties for public key encryption schemes (non-ROM) **) +(* Definitions and properties for public key encryption schemes (non-ROM) *) clone import PublicKeyEncryption as PKE with type pk_t <- pk_t, type sk_t <- sk_t, @@ -42,7 +42,7 @@ clone import PublicKeyEncryption as PKE with proof *. -(** Definitions for random oracles **) +(* Definitions for random oracles *) clone import FullRO as F_RO with type in_t <- in_t, type out_t <- out_t @@ -77,15 +77,15 @@ module type RandomOracle = { }. -(* Schemes *) -(** PKE Schemes (interface with RO) **) +(* Schemes in ROM *) +(** PKE in ROM **) module type Scheme_ROM (RO : RandomOracle) = { include Scheme }. -(* Correctness *) -(** Correctness (probabilistic) program/game in the ROM **) +(* Correctness in ROM *) +(** Correctness (probabilistic) program/game in ROM **) module Correctness_ROM (RO : RandomOraclei, S : Scheme_ROM) = { proc main(p : ptxt_t) : bool = { var r : bool; @@ -99,44 +99,43 @@ module Correctness_ROM (RO : RandomOraclei, S : Scheme_ROM) = { }. -(* Attacker capabilities/models *) +(* Attacker capabilities/models in ROM *) (* - Chosen-Plaintext Attacks (CPA). + Chosen-Plaintext Attacks (CPA) in ROM. The adversary is given the considered public key and, hence, is able to produce ciphertexts corresponding to chosen plaintexts. *) (* - non-adaptive Chosen-Ciphertext Attacks (CCA1) + non-adaptive Chosen-Ciphertext Attacks (CCA1) in ROM. The adversary is given the considered public key and access to a decryption oracle *before* the stage in which it is expected to distinguish/return a break. Hence, the adversary is able to produce ciphertext corresponding to chosen plaintexts *and* query for decryptions of chosen ciphertexts. *) -(* Oracles *) -(** Interface for oracles employed in CCA1 security games, w.r.t. random oracle **) +(** Interface for oracles employed in CCA1 security games in ROM **) module type Oracles_CCA1i_ROM (RO : RandomOracle) (S : Scheme) = { proc init(sk_init : sk_t) : unit proc dec(c : ctxt_t) : ptxt_t option }. (* - adaptive Chosen-Ciphertext Attacks (CCA2) + adaptive Chosen-Ciphertext Attacks (CCA2) in ROM. The adversary is given the considered public key and access to a decryption oracle throughout. Hence, the adversary is able to produce ciphertext corresponding to chosen plaintexts *and* query for decryptions of chosen ciphertexts (potentially barring ciphertexts that are part of the challenge). *) -(** Interface for oracles employed in (the second stage of) CCA2 security games, w.r.t. random oracle **) +(** Interface for oracles employed in (the second stage of) CCA2 security games in ROM **) module type Oracles_CCA2i_ROM (RO : RandomOracle) (S : Scheme) = { proc init(sk_init : sk_t, c'_init : ctxt_t) : unit proc dec(c : ctxt_t) : ptxt_t option }. -(* Properties (regular) *) +(* Security (regular) in ROM *) (** - One-Wayness (OW). + One-Wayness (OW) in ROM. The adversary is asked to produce the message/plaintext encrypted by a given ciphertext. **) @@ -150,14 +149,16 @@ abstract theory OWROM. **) op dptxtm : pk_t -> ptxt_t distr. + (* Clone and import definitions from OW theory (in non-ROM PKE scheme theory) *) clone import OW with op dptxtm <- dptxtm proof *. + (* - One-Wayness under Chosen-Plaintext Attacks (OW-CPA). + One-Wayness under Chosen-Plaintext Attacks (OW-CPA) in ROM. In a CPA setting, the adversary is asked to produce the message/plaintext encrypted by a given ciphertext. *) @@ -180,7 +181,7 @@ module OW_CPA_ROM (RO : RandomOraclei, S : Scheme_ROM, A : Adv_OWCPA_ROM) = { }. (* - One-Wayness under non-adaptive Chosen-Ciphertext Attacks (OW-CCA1). + One-Wayness under non-adaptive Chosen-Ciphertext Attacks (OW-CCA1) in ROM. In a CCA1 setting, the adversary is asked to produce the message/plaintext encrypted by a given ciphertext. *) @@ -205,7 +206,7 @@ module OW_CCA1_ROM (RO : RandomOraclei, S : Scheme_ROM, O : Oracles_CCA1i_ROM, A (* - One-Wayness under adaptive Chosen-Ciphertext Attacks (OW-CCA2). + One-Wayness under adaptive Chosen-Ciphertext Attacks (OW-CCA2) in ROM. In a CCA2 setting, the adversary is asked to produce the message/plaintext encrypted by a given ciphertext. *) @@ -216,9 +217,9 @@ module type Adv_OWCCA2_ROM (RO : RandomOracle) (O : Oracles_CCA) = { }. (** OW-CCA2 security game in ROM **) -module OW_CCA2_ROM (RO : RandomOraclei, S : Scheme_ROM, - O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM, - A : Adv_OWCCA2_ROM) = { +module OW_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_OWCCA2_ROM) = { proc main() : bool = { var r : bool; @@ -234,12 +235,12 @@ end OWROM. (* - (ciphertext) INDistinguishability (IND). + (ciphertext) INDistinguishability (IND) in ROM. The adversary is asked to provide two plaintexts and, subsequently, determine which of these plaintexts is encrypted by a given ciphertext. *) (* - (ciphertext) INDistinguishability under Chosen-Plaintext Attacks (IND-CPA). + (ciphertext) INDistinguishability under Chosen-Plaintext Attacks (IND-CPA) in ROM. In a CPA setting, the adversary is asked to provide two plaintexts and, subsequently, determine which of these plaintexts is encrypted by a given ciphertext. *) @@ -276,7 +277,7 @@ module IND_CPA_P_ROM (RO: RandomOraclei, S : Scheme_ROM, A : Adv_INDCPA_ROM) = { (* - (ciphertext) INDistinguishability under non-adaptive Chosen-Ciphertext Attacks (IND-CCA1). + (ciphertext) INDistinguishability under non-adaptive Chosen-Ciphertext Attacks (IND-CCA1) in ROM. In a CCA1 setting, the adversary is asked to provide two plaintexts and, subsequently, determine which of these plaintexts is encrypted by a given ciphertext. *) @@ -314,7 +315,7 @@ module IND_CCA1_P_ROM (RO : RandomOraclei, S : Scheme_ROM, O : Oracles_CCA1i_ROM (* - (ciphertext) INDistinguishability under adaptive Chosen-Ciphertext Attacks (IND-CCA2). + (ciphertext) INDistinguishability under adaptive Chosen-Ciphertext Attacks (IND-CCA2) in ROM. In a CCA2 setting, the adversary is asked to provide two plaintexts and, subsequently, determine which of these plaintexts is encrypted by a given ciphertext. *) @@ -324,10 +325,10 @@ module type Adv_INDCCA2_ROM (RO : RandomOracle) (O : Oracles_CCA) = { proc distinguish(c : ctxt_t) : bool }. -(** IND-CCA2 security game (sampled bit) **) -module IND_CCA2_ROM (RO : RandomOraclei, S : Scheme_ROM, - O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM, - A : Adv_INDCCA2_ROM) = { +(** IND-CCA2 security game (sampled bit) in ROM **) +module IND_CCA2_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_INDCCA2_ROM) = { proc main() : bool = { var r : bool; @@ -339,10 +340,10 @@ module IND_CCA2_ROM (RO : RandomOraclei, S : Scheme_ROM, } }. -(** IND-CCA2 security game (provided bit) **) -module IND_CCA2_P_ROM (RO : RandomOraclei, S : Scheme_ROM, - O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM, - A : Adv_INDCCA2_ROM) = { +(** IND-CCA2 security game (provided bit) in ROM **) +module IND_CCA2_P_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O1 : Oracles_CCA1i_ROM, O2 : Oracles_CCA2i_ROM) + (A : Adv_INDCCA2_ROM) = { proc main(b : bool) : bool = { var r : bool; @@ -356,7 +357,7 @@ module IND_CCA2_P_ROM (RO : RandomOraclei, S : Scheme_ROM, (** - Non-Malleability (NM). + Non-Malleability (NM) in ROM. The adversary is asked to provide a relation (say R) and a list of ciphertexts such that the plaintexts obtained from decrypting these ciphertexts are related (under R) to the plaintext corresponding to a given ciphertext. @@ -385,9 +386,9 @@ clone import NM with proof *. -(* Properties *) +(* Properties in ROM *) (* - Non-Malleability under Chosen-Plaintext Attacks (NM-CPA) + Non-Malleability under Chosen-Plaintext Attacks (NM-CPA) in ROM. In a CPA setting, the adversary is asked to provide a relation (say R) and a list of ciphertexts such that the plaintexts obtained from decrypting these ciphertexts are related (under R) to the plaintext corresponding to a given ciphertext. @@ -412,7 +413,7 @@ module NM_CPA_ROM (RO : RandomOraclei, S : Scheme_ROM, A : Adv_NMCPA_ROM) = { (* - Non-Malleability under non-adaptive Chosen-Plaintext Attacks (NM-CCA1) + Non-Malleability under non-adaptive Chosen-Plaintext Attacks (NM-CCA1) in ROM. In a CCA1 setting, the adversary is asked to provide a relation (say R) and a list of ciphertexts such that the plaintexts obtained from decrypting these ciphertexts are related (under R) to the plaintext corresponding to a given ciphertext. @@ -438,7 +439,7 @@ module NM_CCA1_ROM (RO : RandomOraclei, S : Scheme_ROM, O : Oracles_CCA1i_ROM, A (* - Non-Malleability under adaptive Chosen-Plaintext Attacks (NM-CCA2) + Non-Malleability under adaptive Chosen-Plaintext Attacks (NM-CCA2) in ROM. In a CCA2 setting, the adversary is asked to provide a relation (say R) and a list of ciphertexts such that the plaintexts obtained from decrypting these ciphertexts are related (under R) to the plaintext corresponding to a given ciphertext. @@ -468,16 +469,16 @@ end NMROM. (* - ANOnymity (ANO). - (Alternatively: Indistinguishability of (public) Keys (IK).) + ANOnymity (ANO) in ROM. + (Alternatively: Indistinguishability of (public) Keys (IK) in ROM.) First, the adversary is given two (honestly generated) public keys and asked to provide a plaintext. Subsequently, the adversary is given the encryption (under one of the aforementioned public keys) of the plaintext it provided and asked to determine which public key was used for the encryption. *) (* - ANOnymity under Chosen-Plaintext attack (ANO-CPA). - (Alternatively: Indistinguishability of (public) Keys under Chosen-Plaintext Attack (IK-CPA).) + ANOnymity under Chosen-Plaintext attack (ANO-CPA) in ROM. + (Alternatively: Indistinguishability of (public) Keys under Chosen-Plaintext Attack (IK-CPA) in ROM.) In a CPA setting, first, the adversary is given two (honestly generated) public keys and asked to provide a plaintext. Subsequently, the adversary is given the encryption (under one of the aforementioned public keys) of the plaintext it provided and asked to determine which @@ -516,9 +517,9 @@ module ANO_CPA_P_ROM (RO : RandomOraclei, S : Scheme_ROM, A : Adv_ANOCPA_ROM) = (* - ANOnymity under non-adaptive Chosen-Plaintext attack (ANO-CCA1). + ANOnymity under non-adaptive Chosen-Plaintext attack (ANO-CCA1) in ROM. (Alternatively: Indistinguishability of (public) Keys under - non-adaptive Chosen-Ciphertext Attack (IK-CCA1).) + non-adaptive Chosen-Ciphertext Attack (IK-CCA1) in ROM.) In a CCA1 setting, first, the adversary is given two (honestly generated) public keys and asked to provide a plaintext. Subsequently, the adversary is given the encryption (under one of the aforementioned public keys) of the plaintext it provided and asked to determine which @@ -531,9 +532,9 @@ module type Adv_ANOCCA1_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_ }. (** ANO-CCA1 security game (sampled bit) in ROM **) -module ANO_CCA1_ROM (RO : RandomOraclei, S : Scheme_ROM, - O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, - A : Adv_ANOCCA1_ROM) = { +module ANO_CCA1_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_ANOCCA1_ROM) = { proc main() : bool = { var r : bool; @@ -546,9 +547,9 @@ module ANO_CCA1_ROM (RO : RandomOraclei, S : Scheme_ROM, }. (** ANO-CCA1 security game (provided bit) in ROM **) -module ANO_CCA1_P_ROM (RO : RandomOraclei, S : Scheme_ROM, - O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, - A : Adv_ANOCCA1_ROM) = { +module ANO_CCA1_P_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_ANOCCA1_ROM) = { proc main(b : bool) : bool = { var r : bool; @@ -562,9 +563,9 @@ module ANO_CCA1_P_ROM (RO : RandomOraclei, S : Scheme_ROM, (* - ANOnymity under adaptive Chosen-Plaintext attack (ANO-CCA2). + ANOnymity under adaptive Chosen-Plaintext attack (ANO-CCA2) in ROM. (Alternatively: Indistinguishability of (public) Keys under - adaptive Chosen-Ciphertext Attack (IK-CCA2).) + adaptive Chosen-Ciphertext Attack (IK-CCA2) in ROM.) In a CCA2 setting, first, the adversary is given two (honestly generated) public keys and asked to provide a plaintext. Subsequently, the adversary is given the encryption (under one of the aforementioned public keys) of the plaintext it provided and asked to determine which @@ -610,12 +611,12 @@ module ANO_CCA2_P_ROM (RO : RandomOraclei, S : Scheme_ROM) (* - Strong ROBustness (SROB). + Strong ROBustness (SROB) in ROM. The adversary is given two (honestly generated) public keys and is asked to provide a (single) ciphertext that decrypts to valid plaintexts under both of the secret keys (corresponding to the provided public keys). - Weak ROBustness (WROB). + Weak ROBustness (WROB) in ROM. The adversary is given two (honestly generated) public keys and is asked to choose which one to use for encryption and which one to use (the corresponding secret key of) for decryption. Here, the goal is that the decryption (with the key appointed for @@ -628,7 +629,7 @@ module ANO_CCA2_P_ROM (RO : RandomOraclei, S : Scheme_ROM) oracle like in CCA1, i.e., no considered challenge). *) (* - Strong ROBustness under Chosen-Plaintext Attacks (SROB-CPA). + Strong ROBustness under Chosen-Plaintext Attacks (SROB-CPA) in ROM. In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to provide a (single) ciphertext that decrypts to valid plaintexts under both of the secret keys (corresponding to the provided public keys). @@ -652,7 +653,7 @@ module SROB_CPA_ROM (RO : RandomOraclei, S : Scheme_ROM, A : Adv_SROBCPA_ROM) = }. (* - Weak ROBustness under Chosen-Plaintext Attacks (WROB-CPA). + Weak ROBustness under Chosen-Plaintext Attacks (WROB-CPA) in ROM. In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to choose which one to use for encryption and which one to use (the corresponding secret key of) for decryption. Here, the goal is that the decryption (with the key appointed for @@ -679,7 +680,7 @@ module WROB_CPA_ROM (RO : RandomOraclei, S : Scheme_ROM, A : Adv_WROBCPA_ROM) = (* - Strong ROBustness under Chosen-Ciphertext Attacks (SROB-CCA). + Strong ROBustness under Chosen-Ciphertext Attacks (SROB-CCA) in ROM. In a CCA setting, the adversary is given two (honestly generated) public keys and is asked to provide a (single) ciphertext that decrypts to valid plaintexts under both of the secret keys (corresponding to the provided public keys). @@ -705,7 +706,7 @@ module SROB_CCA_ROM (RO : RandomOraclei, S : Scheme_ROM, }. (* - Weak ROBustness under Chosen-Ciphertext Attacks (WROB-CCA). + Weak ROBustness under Chosen-Ciphertext Attacks (WROB-CCA) in ROM. In a CCA setting, the adversary is given two (honestly generated) public keys and is asked to choose which one to use for encryption and which one to use (the corresponding secret key of) for decryption. Here, the goal is that the decryption (with the key appointed for @@ -718,9 +719,9 @@ module type Adv_WROBCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_ }. (** WROB-CCA security game in ROM **) -module WROB_CCA_ROM (RO : RandomOraclei, S : Scheme_ROM, - O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, - A : Adv_WROBCCA_ROM) = { +module WROB_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_WROBCCA_ROM) = { proc main() : bool = { var r : bool; @@ -734,16 +735,16 @@ module WROB_CCA_ROM (RO : RandomOraclei, S : Scheme_ROM, (* - Strong Collision-FReeness (SCFR). + Strong Collision-FReeness (SCFR) in ROM. As SROB, but additionally requires the resulting plaintexts to be equal to eachother (instead of only requiring them to be valid). - Weak Collision-FReeness (WCFR). + Weak Collision-FReeness (WCFR) in ROM. As WROB, but additionally requires the resulting plaintexts to be equal to eachother (instead of only requiring the final plaintext to be valid). *) (* - Strong Collision-FReeness under Chosen-Plaintext Attacks (SCFR-CPA). + Strong Collision-FReeness under Chosen-Plaintext Attacks (SCFR-CPA) in ROM. In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to provide a (single) ciphertext that decrypts to the same valid plaintext under both of the secret keys (corresponding to the provided public keys). @@ -767,7 +768,7 @@ module SCFR_CPA_ROM (RO : RandomOraclei, S : Scheme_ROM, A : Adv_SCFRCPA_ROM) = }. (* - Weak Collision-FReeness under Chosen-Plaintext Attacks (WCFR-CPA). + Weak Collision-FReeness under Chosen-Plaintext Attacks (WCFR-CPA) in ROM. In a CPA setting, the adversary is given two (honestly generated) public keys and is asked to choose which one to use for encryption and which one to use (the corresponding secret key of) for decryption. Here, the goal is that the decryption (with the key appointed for @@ -805,9 +806,9 @@ module type Adv_SCFRCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_ }. (** SCFR-CCA security game in ROM **) -module SCFR_CCA_ROM (RO : RandomOraclei, S : Scheme_ROM, - O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, - A : Adv_SCFRCCA_ROM) = { +module SCFR_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_SCFRCCA_ROM) = { proc main() : bool = { var r : bool; @@ -820,7 +821,7 @@ module SCFR_CCA_ROM (RO : RandomOraclei, S : Scheme_ROM, }. (* - Weak ROBustness under Chosen-Ciphertext Attacks (WCFR-CCA). + Weak ROBustness under Chosen-Ciphertext Attacks (WCFR-CCA) in ROM. In a CCA setting, the adversary is given two (honestly generated) public keys and is asked to choose which one to use for encryption and which one to use (the corresponding secret key of) for decryption. Here, the goal is that the decryption (with the key appointed for @@ -833,9 +834,9 @@ module type Adv_WCFRCCA_ROM (RO : RandomOracle) (O0 : Oracles_CCA, O1 : Oracles_ }. (** WCFR-CCA security game in ROM **) -module WCFR_CCA_ROM (RO : RandomOraclei, S : Scheme_ROM, - O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM, - A : Adv_WCFRCCA_ROM) = { +module WCFR_CCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (O0 : Oracles_CCA1i_ROM, O1 : Oracles_CCA1i_ROM) + (A : Adv_WCFRCCA_ROM) = { proc main() : bool = { var r : bool; @@ -848,12 +849,13 @@ module WCFR_CCA_ROM (RO : RandomOraclei, S : Scheme_ROM, }. -(** Delta-correct (i.e., partially-correct) PKE schemes. **) +(** Delta-correct (i.e., partially-correct) PKE schemes in ROM. **) theory DeltaCorrectROM. (* Import definitions from delta-correctness theory (in non-ROM PKE theory) *) import DeltaCorrect. -(* Correctness *) + +(* Correctness in ROM *) (** Adversary class considered for (partial/delta) correctness in ROM **) module type Adv_Cor_ROM (RO : RandomOracle) = { include Adv_Cor @@ -873,8 +875,7 @@ module Correctness_Delta_ROM (RO : RandomOraclei, S : Scheme_ROM, A : Adv_Cor_RO }. -(* Attacker capabilities/models (additional) *) -(* Oracles *) +(* Attacker capabilities/models (additional) in ROM *) (** Interface for Plaintext-Checking (PC) oracles used by games in ROM **) module type Oracles_PCi_ROM (RO : RandomOracle) (S : Scheme) = { proc init(sk_init : sk_t) : unit @@ -888,9 +889,9 @@ module type Oracles_CVi_ROM (RO : RandomOracle) (S : Scheme) = { }. -(* Properties (regular) *) +(* Security (delta-correct) in ROM *) (** - One-Wayness (OW). + One-Wayness (OW) in ROM. The adversary is asked to produce the message/plaintext encrypted by a given ciphertext. **) @@ -912,7 +913,7 @@ clone import OW with proof *. -(* One-Wayness under Chosen-Plaintext Attack (OW-CPA) *) +(* One-Wayness under Chosen-Plaintext Attack (OW-CPA) in ROM *) (** Adversary type considered for OW-CPA in ROM **) module type Adv_OWCPA_ROM (RO : RandomOracle) = { include Adv_OWCPA @@ -932,7 +933,7 @@ module OW_CPA_ROM (RO : RandomOraclei, S : Scheme_ROM, O : Oracles_PCi_ROM, A : }. -(* One-Wayness under Plaintext-Checking Attacks (OW-PCA) *) +(* One-Wayness under Plaintext-Checking Attacks (OW-PCA) in ROM *) (** Adversary type considered for OW-PCA in ROM **) module type Adv_OWPCA_ROM (RO : RandomOracle) (O : Oracles_PC) = { proc find(pk : pk_t, c : ctxt_t) : ptxt_t @@ -952,16 +953,16 @@ module OW_PCA_ROM (RO : RandomOraclei, S : Scheme_ROM, O : Oracles_PCi_ROM, A : }. -(* One-Wayness under Validity-Checking Attacks (OW-VCA) *) +(* One-Wayness under Validity-Checking Attacks (OW-VCA) in ROM *) (** Adversary type considered for OW-VCA in ROM **) module type Adv_OWVCA_ROM (RO : RandomOracle) (O : Oracles_CV) = { proc find(pk : pk_t, c : ctxt_t) : ptxt_t }. (** OW-VCA security game in ROM **) -module OW_VCA_ROM (RO : RandomOraclei, S : Scheme_ROM, - OPC : Oracles_PCi_ROM, OCV : Oracles_CVi_ROM, - A : Adv_OWVCA_ROM) = { +module OW_VCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (OPC : Oracles_PCi_ROM, OCV : Oracles_CVi_ROM) + (A : Adv_OWVCA_ROM) = { proc main() : bool = { var r : bool; @@ -974,16 +975,16 @@ module OW_VCA_ROM (RO : RandomOraclei, S : Scheme_ROM, }. -(* One-Wayness under Validity-Checking Attacks (OW-PVCA) *) +(* One-Wayness under Validity-Checking Attacks (OW-PVCA) in ROM *) (** Adversary type considered for OW-PVCA in ROM **) module type Adv_OWPVCA_ROM (RO : RandomOracle) (OPC : Oracles_PC, OCV : Oracles_CV) = { proc find(pk : pk_t, c : ctxt_t) : ptxt_t }. (** OW-PVCA security game in ROM **) -module OW_PVCA_ROM (RO : RandomOraclei, S : Scheme_ROM, - OPC : Oracles_PCi_ROM, OCV : Oracles_CVi_ROM, - A : Adv_OWPVCA_ROM) = { +module OW_PVCA_ROM (RO : RandomOraclei) (S : Scheme_ROM) + (OPC : Oracles_PCi_ROM, OCV : Oracles_CVi_ROM) + (A : Adv_OWPVCA_ROM) = { proc main() = { var r : bool; @@ -998,4 +999,3 @@ module OW_PVCA_ROM (RO : RandomOraclei, S : Scheme_ROM, end OWROM. end DeltaCorrectROM. - diff --git a/tmp/KEM_Binding.eca b/tmp/KEM_Binding.eca new file mode 100644 index 0000000..ac2e3b8 --- /dev/null +++ b/tmp/KEM_Binding.eca @@ -0,0 +1,70 @@ +(* Require/Import libraries *) +require import AllCore. +require (*--*) KeyedHashFunctions KeyEncapsulationMechanisms. + + +(* Types *) +(* Keyed hash functions *) +(** (Indexing) Keys **) +type ik_t. + +(** Inputs **) +type in_t. + +(** Outputs **) +type out_t. + +(* Key encapsulation mechanisms *) +(** Public keys (asymmetric) **) +type pk_t. + +(** Secret keys (asymmetric) **) +type sk_t. + +(** Shared/session keys (symmetric) **) +type key_t. + +(** Ciphertexts/Encapsulations **) +type ctxt_t. + + +(* Operators *) +(** Keyed hash function **) +op kdf : ik_t -> in_t -> out_t. + + +(* Distributions *) +(** (Proper) distribution over (indexing) keys **) +op [lossless] dik : ik_t distr. + + +(* Clones and imports *) +(* Import basic definitions and properties for KHFs *) +clone import KeyedHashFunctions as KHFs with + type key_t <- ik_t, + type in_t <- in_t, + type out_t <- out_t, + + op f <- kdf + + proof *. + +(* Import basic definitions and properties for KEMs *) +clone import KeyEncapsulationMechanisms as KEMs with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t + + proof *. + +(* Import basic definitions and properties for KEMs with post-processing *) +clone import KeyEncapsulationMechanisms as KEMPPs with + type pk_t <- pk_t * ik_t, + type sk_t <- sk_t * ik_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t + + proof *. + + (* *) diff --git a/tmp/KeyedHashFunctions.eca b/tmp/KeyedHashFunctions.eca new file mode 100644 index 0000000..6a91da0 --- /dev/null +++ b/tmp/KeyedHashFunctions.eca @@ -0,0 +1,1663 @@ +(**************************************************************************) +(* File containing everything related to keyed hash functions. *) +(* This file is based on the material from several papers. *) +(* More precisely, this concerns the following references: *) +(* - "Cryptographic Hash-Function Basics: Definitions, Implications, and *) +(* Separations for Preimage Resistance, Second-Preimage Resistance, *) +(* and Collision Resistance" *) +(* DOI: 10.1007/978-3-540-25937-4_24 *) +(* - "Mitigating Multi-Target Attacks in Hash-based Signatures" *) +(* DOI: 10.1007/978-3-662-49384-7_15 *) +(* - "Decisional second-preimage resistance: When does SPR imply PRE?" *) +(* DOI: 10.1007/978-3-030-34618-8_2 *) +(* - "The SPHINCS+ Signature Framework." *) +(* DOI: 10.1145/3319535.3363229 *) +(* - "Recovering the Tight Security Proof of SPHINCS+" *) +(* DOI: 10.1007/978-3-031-22972-5_1 *) +(**************************************************************************) + +(* --- Require/Import --- *) +(* -- Built-in (i.e, standard library) -- *) +require import AllCore List Distr FMap. + + + +(* +--- + Preliminary Note: + The ensuing formalizes the concept of keyed hash functions and several + properties of such functions. For most of these properties, there are + several variants based on the number of considered functions and/or the number of + considered targets. Independent of the property, these variants always deviate from the + basic property in the same manner. Below, we describe how each of these variants differs + from the basic property. + + - single-function, single-target: + In most cases, this is the default 'variant' of the property (i.e., the standard/basic property). + This considers only a single function (or, equivalently, single index key) and a single target + (e.g., a single input or single output) with/for which the adversary can try to break the + considered property. + + - Single-function, Multi-target (SM): + This variant considers a single function (or, equivalently, single index key) and multiple + targets with/for which the adversary can try to break the considered property. + + - Multi-function, Multi-target (MM): + This variant considers multiple functions (or, equivalently, multiple index keys) and multiple + targets with/for which the adversary can try to break the considered property. + + - Distinct-function, Multi-target (DM): + This variant considers multiple functions (or, equivalently, multiple index keys) and multiple + targets with/for which the adversary can try to break the considered property. Here, in contrast + to the MM variant, the functions are required to be distinct from each other. +--- +*) + + + +(* --- General --- *) +(* -- Types -- *) +(* Types for inputs ('messages') and, respectively, outputs ('message digests') of hash function *) +type in_t. +type out_t. + +(* Type for (indexing) keys *) +type key_t. + + +(* -- Operators -- *) +(* Keyed hash function *) +op f : key_t -> in_t -> out_t. + + + +(* --- Properties --- *) +(* +-- + PREimage resistance (PRE) / One-Wayness (OW). + Given a key k and an output y, it is hard to find an input x such that f k x = y +-- +*) +(* - single-function, single-target PREimage resistance (PRE) - *) +abstract theory PRE. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against PRE *) + module type Adv_PRE = { + proc find(k : key_t, y : out_t) : in_t + }. + + (* PRE game *) + module PRE(A : Adv_PRE) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + var y : out_t; + + (* Sample key k and input x *) + k <$ dkey; + x <$ din; + + (* Compute output y of hash function when given key k and input x *) + y <- f k x; + + (* Ask adversary to find a preimage x' of y *) + x' <@ A.find(k, y); + + (* Success iff x' is a preimage of y, i.e., if f k maps x' to y *) + return f k x' = y; + } + }. +end PRE. + + +(* - Single-function, Multi-target PREimage resistance (SM_PRE) - *) +abstract theory SMPRE. + (* Number of targets in SM_PRE *) + const t_smpre : { int | 1 <= t_smpre } as ge1_tsmpre. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against SM_PRE *) + module type Adv_SMPRE = { + proc find(k : key_t, yl : out_t list) : int * in_t + }. + + (* SM_PRE game *) + module SM_PRE(A : Adv_SMPRE) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + var y : out_t; + var yl : out_t list; + var i : int; + + (* Sample key k *) + k <$ dkey; + + (* + Construct list yl of size t_smpre containing outputs obtained + by applying f k to randomly sampled inputs + *) + yl <- []; + while (size yl < t_smpre) { + x <$ din; + y <- f k x; + yl <- rcons yl y; + } + + (* Ask adversary to find a preimage x' of any output in yl *) + (i, x') <@ A.find(k, yl); + + (* Get key k and output y from yl at index i, as specified by the adversary *) + y <- nth witness yl i; + + (* + Success iff + (1) "0 <= i < size yl": index i provided by adversary is within the bounds of yl + (i.e., between 0 (including) and the size yl = t_smpre (excluding)), and + (2) "f k x' = y": x' is a preimage of y under f k + *) + return 0 <= i < size yl /\ f k x' = y; + } + }. +end SMPRE. + + +(* - Multi-function, Multi-target PREimage resistance (MM_PRE) - *) +abstract theory MMPRE. + (* Number of functions/targets in MM_PRE *) + const t_mmpre : { int | 1 <= t_mmpre } as ge1_tmmpre. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against MM_PRE *) + module type Adv_MMPRE = { + proc find(kyl : (key_t * out_t) list) : int * in_t + }. + + (* MM_PRE game *) + module MM_PRE(A : Adv_MMPRE) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + var y : out_t; + var ky : key_t * out_t; + var kyl : (key_t * out_t) list; + var i : int; + + (* + Construct list kyl of t_mmpre (key, output) pairs (k, y). + For each pair, key k is randomly sampled, + after which output y is obtained by applying f k + to a randomly sampled input + *) + kyl <- []; + while (size kyl < t_mmpre) { + k <$ dkey; + x <$ din; + y <- f k x; + ky <- (k, y); + kyl <- rcons kyl ky; + } + + (* + Ask adversary to find a preimage of an output in any + (key, output) pair in kyl w.r.t. the key in the (same) pair + *) + (i, x') <@ A.find(kyl); + + (* Get (key, output) pair ky from kyl at index i, as specified by adversary *) + ky <- nth witness kyl i; + + (* Extract key k and, respecively, output y from ky *) + k <- ky.`1; + y <- ky.`2; + + (* + Success iff + (1) "0 <= i < size kyl": index provided by adversary is within the bounds of kyl + (i.e., between 0 (including) and size kyl = t_mmpre (excluding)), and + (2) "f k x' = y": f k maps x' to y + *) + return 0 <= i < size kyl /\ f k x' = y; + } + }. +end MMPRE. + + +(* - Distinct-function, Multi-target PREimage resistance (DM_PRE) - *) +abstract theory DMPRE. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Class of adversaries against DM_PRE *) + module type Adv_DMPRE = { + proc pick() : key_t list + proc find(yl : out_t list) : int * in_t + }. + + (* DM_PRE game *) + module DM_PRE(A : Adv_DMPRE) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + var y : out_t; + var kl : key_t list; + var yl : out_t list; + var i : int; + + (* + Ask adversary to provide a list kl of keys that will be used to index f. + As indicated in the return statement, this list must not contain duplicate + elements (so that indexing f with each element gives a distinct function) + *) + kl <@ A.pick(); + + (* + Construct list yl of a size equal to the size of kl. + In yl, the element at index i is the mapping of a randomly sampled input + under the function obtained fromindexing f with the element of kl at index i. + That is, if the i-th element of kl is k, then the i-th element of + yl is obtained by applying f k to a randomly sampled input + *) + yl <- []; + while (size yl < size kl) { + k <- nth witness kl (size yl); + x <$ din; + y <- f k x; + yl <- rcons yl y; + } + + (* + Ask adversary to find a preimage for any output + in yl w.r.t. the corresponding (i.e., at the same index) key in kl + *) + (i, x') <@ A.find(yl); + + (* + Get key k and output y from kl and, respectively, yl at index i, + as specified by the adversary + *) + k <- nth witness kl i; + y <- nth witness yl i; + + (* + Success iff + (1) "0 <= i < size kl": index provided by adversary is within the bounds of kl, and + (2) "uniq kl": kl contains no duplicate elements, and + (3) "f k x' = y": f k maps x' to y + *) + return 0 <= i < size kl /\ uniq kl /\ f k x' = y; + } + }. +end DMPRE. + + +(* +-- + Second Preimage Resistance (SPR). + Given a key k and input x, it is hard to find an input x' that is different from x + such that f k x = f k x' +-- +*) +(* - single-function, single-target Second Preimage Resistance (SPR) - *) +abstract theory SPR. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against SPR *) + module type Adv_SPR = { + proc find(k : key_t, x : in_t) : in_t + }. + + (* SPR game *) + module SPR(A : Adv_SPR) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + + (* Sample key k and input x *) + k <$ dkey; + x <$ din; + + (* Ask adversary to find a second preimage x' of x w.r.t. k (i.e., under f k) *) + x' <@ A.find(k, x); + + (* + Success iff + (1) "x' <> x": x' does not equal x, and + (2) "f k x' = f k x": f k maps x' to the same element as it maps x + *) + return x' <> x /\ f k x' = f k x; + } + }. +end SPR. + + +(* - Single-function, Multi-target Second Preimage Resistance (SM_SPR) - *) +abstract theory SMSPR. + (* Number of targets in SM_SPR *) + const t_smspr : { int | 1 <= t_smspr } as ge1_tsmspr. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against SM_SPR *) + module type Adv_SMSPR = { + proc find(k : key_t, xl : in_t list) : int * in_t + }. + + (* SM_SPR game *) + module SM_SPR(A : Adv_SMSPR) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + var xl : in_t list; + var i : int; + + (* Sample key k *) + k <$ dkey; + + (* Construct list xl of t_smspr randomly sampled inputs *) + xl <- []; + while (size xl < t_smspr) { + x <$ din; + xl <- rcons xl x; + } + + (* Ask adversary to find second preimage for any input in xl *) + (i, x') <@ A.find(k, xl); + + (* Get input from xl at index i, as specified by the adversary *) + x <- nth witness xl i; + + (* + Success iff + (1) "0 <= i < size xl": index i provided by adversary is within the bounds of xl + (i.e., between 0 (including) and the size xl = t_smspr (excluding)), and + (2) "x' <> x": x' does not equal x, and + (3) "f k x' = f k x": f k maps x' to the same element as it maps x + *) + return 0 <= i < size xl /\ x' <> x /\ f k x' = f k x; + } + }. +end SMSPR. + + +(* - Multi-function, Multi-target Second Preimage Resistance (MM_SPR) - *) +abstract theory MMSPR. + (* Number of functions/targets in MM_SPR *) + const t_mmspr : { int | 1 <= t_mmspr } as ge1_tmmspr. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against MM_SPR *) + module type Adv_MMSPR = { + proc find(kxl : (key_t * in_t) list) : int * in_t + }. + + (* MM_SPR game *) + module MM_SPR(A : Adv_MMSPR) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + var kx : key_t * in_t; + var kxl : (key_t * in_t) list; + var i : int; + + (* + Construct list kxl of size t_mmspr containing (key, input) pairs (k, x). + For each pair, key k and input x are both randomly sampled from + their respective distributions + *) + kxl <- []; + while (size kxl < t_mmspr) { + k <$ dkey; + x <$ din; + kx <- (k, x); + kxl <- rcons kxl kx; + } + + (* + Ask adversary to find a second preimage for an input in any + (key, input) pair in kxl w.r.t. the key in the (same) pair + *) + (i, x') <@ A.find(kxl); + + (* Get (key, input) pair kx from kxl at index i, as specified by the adversary *) + kx <- nth witness kxl i; + + (* Extract key k and, respectively, input x from kx *) + k <- kx.`1; + x <- kx.`2; + + (* + Success iff + (1) "0 <= i < size kxl": index provided by adversary is within the bounds of kyl + (i.e., between 0 (including) and size kxl = t_mmspr (excluding)), and + (2) "x' <> x": x' does not equal x, and + (3) "f k x' = f k x": f k maps x' to the same element as it maps x + *) + return 0 <= i < size kxl /\ x' <> x /\ f k x' = f k x; + } + }. +end MMSPR. + + +(* - Distinct-function, Multi-target Second Preimage Resistance (DM_SPR) - *) +abstract theory DMSPR. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Class of adversaries against DM_SPR *) + module type Adv_DMSPR = { + proc pick() : key_t list + proc find(xl : in_t list) : int * in_t + }. + + (* DM_SPR game *) + module DM_SPR(A : Adv_DMSPR) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + var kl : key_t list; + var xl : in_t list; + var i : int; + + (* + Ask adversary to provide a list kl of keys that will be used to index f. + As indicated in the return statement, this list must not contain duplicate + elements (so that indexing f with each element gives a distinct function) + *) + kl <@ A.pick(); + + (* + Construct list xl of a size equal to the size of kl; + each element of xl is a randomly sampled input. + *) + xl <- []; + while (size xl < size kl) { + x <$ din; + xl <- rcons xl x; + } + + (* + Ask adversary to find a second preimage for any input + in xl w.r.t. the corresponding (i.e., at the same index) key in kl + *) + (i, x') <@ A.find(xl); + + (* + Get key k and input x from kl and, respectively, xl at index i, + as specified by the adversary + *) + k <- nth witness kl i; + x <- nth witness xl i; + + (* + Success iff + (1) "0 <= i < size kl": index provided by adversary is within the bounds of kl, and + (2) "uniq kl": kl contains no duplicate elements, and + (3) "x' <> x": x' does not equal x, and + (4) "f k x' = f k x": f k maps x' to the same element as it maps x + *) + return 0 <= i < size kl /\ uniq kl /\ x' <> x /\ f k x' = f k x; + } + }. +end DMSPR. + + +(* +-- + Collision Resistance (CR). + Given a key k, it is hard to find two different inputs x and x' such that f k x = f k x' +-- +*) +(* - regular Collision Resistance (CR) - *) +abstract theory CR. + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against CR *) + module type Adv_CR = { + proc find(k : key_t) : in_t * in_t + }. + + (* CR game *) + module CR(A : Adv_CR) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + + (* Sample key k *) + k <$ dkey; + + (* Ask adversary to find two values x and x' that collide w.r.t. to k (i.e., under f k) *) + (x, x') <@ A.find(k); + + (* + Success iff + (1) "x' <> x": x' does not equal x, and + (2) "f k x' = f k x": f k maps x' to the same element as it maps x + *) + return x' <> x /\ f k x' = f k x; + } + }. +end CR. + + +(* - Target Collision Resistance (TCR) - *) +abstract theory TCR. + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against TCR *) + module type Adv_TCR = { + proc pick() : in_t + proc find(k : key_t) : in_t + }. + + (* TCR game *) + module TCR(A : Adv_TCR) = { + proc main() : bool = { + var k : key_t; + var x, x' : in_t; + + (* Ask adversary to pick an input (the 'target') *) + x <@ A.pick(); + + (* Sample key k *) + k <$ dkey; + + (* Ask adversary to find a value x' that collides with x w.r.t k (i.e., under f k) *) + x' <@ A.find(k); + + (* + Success iff + (1) "x' <> x": x' does not equal x, and + (2) "f k x' = f k x": f k maps x' to the same element as it maps x + *) + return x' <> x /\ f k x' = f k x; + } + }. +end TCR. + + +(* - Extended Target Collision Resistance (ETCR) - *) +abstract theory ETCR. + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against ETCR *) + module type Adv_ETCR = { + proc pick() : in_t + proc find(k : key_t) : key_t * in_t + }. + + (* ETCR game *) + module ETCR (A : Adv_ETCR) = { + proc main() : bool = { + var k, k' : key_t; + var x, x' : in_t; + + (* Ask adversary to pick an input (the 'target') *) + x <@ A.pick(); + + (* Sample key k *) + k <$ dkey; + + (* + Ask adversary to find any pair (k', x') such that x under f k collides with + x' under f k'. + Note that k' may be any element from the domain of keys, including k + *) + (k', x') <@ A.find(k); + + (* + Success iff + (1) "x' <> x": x' does not equal x, and + (2) "f k' x' = f k x": f k' maps x' to the same element as f k maps x + *) + return x' <> x /\ f k x' = f k' x; + } + }. +end ETCR. + + +(* - Multi-target Extended Target Collision Resistance (M_ETCR) - *) +abstract theory METCR. + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Type for oracles used in M_ETCR game *) + module type Oracle_METCRi_t = { + proc init() : unit + proc query(x : in_t) : key_t + proc get(i : int) : key_t * in_t + proc nr_targets() : int + }. + + (* Type for oracles given to adversary in M_ETCR game *) + module type Oracle_METCR_t = { + proc query(x : in_t) : key_t + }. + + (* Default implementation of an oracle for M_ETCR *) + module O_METCR_Default : Oracle_METCRi_t = { + var ts : (key_t * in_t) list + + (* Initialize list of targets (i.e., (key, input) pairs) to the empty list *) + proc init() : unit = { + ts <- []; + } + + (* Samples key k, adds pair (k, x) to list of targets, and returns k *) + proc query(x : in_t) : key_t = { + var k : key_t; + var kx : key_t * in_t; + + k <$ dkey; + + kx <- (k, x); + ts <- rcons ts kx; + + return k; + } + + (* Gets i-th element in list of targets; returns witness if index is out of bounds *) + proc get(i : int) : key_t * in_t = { + return nth witness ts i; + } + + (* Returns the number of elements in the list of targets *) + proc nr_targets() : int = { + return size ts; + } + }. + + (* Class of adversaries against M_ETCR *) + module type Adv_METCR(O : Oracle_METCR_t) = { + proc find() : int * key_t * in_t { O.query } + }. + + (* M_ETCR game *) + module M_ETCR (A : Adv_METCR, O : Oracle_METCRi_t) = { + proc main() : bool = { + var k, k' : key_t; + var x, x' : in_t; + var i : int; + var nrts : int; + + (* Initialize oracle O *) + O.init(); + + (* + Ask adversary to + (1) Generate (key, input) pairs (the 'targets') by querying oracle O + (2) Find a pair (k', x') such that, for any (key, input) pair (k, x) in + the list of targets, x' under f k' collides with x under f k. + Note that k' may be any element from the domain of keys, including k + *) + (i, k', x') <@ A(O).find(); + + (* + Get (key, input) pair (i.e., target) (k, x) from list of targets at index i, + as specified by the adversary + *) + (k, x) <@ O.get(i); + + (* Get number of elements in the list of targets specified by the adversary *) + nrts <@ O.nr_targets(); + + (* + Success iff + (1) "0 <= i < size nrts": index provided by adversary is within the bounds + of nrts (i.e., between 0 (including) and nrts (excluding)), and + (2) "x' <> x": x' does not equal x, and + (3) "f k' x' = f k x": f k' maps x' to the same element as f k maps x + *) + return 0 <= i < nrts /\ x' <> x /\ f k' x' = f k x; + } + }. +end METCR. + + +(* +-- + Decisional Second Preimage Resistance (DSPR). + Given a key k and input x, it is hard to determine whether there exists an input x' + that is different from x such that f k x = f k x' +-- +*) +(* - General - *) +(* Predicate that checks whether there exists a second preimage for a given x under f k *) +abbrev spexists (k : key_t, x : in_t) = exists (x' : in_t), x' <> x /\ f k x' = f k x. + + +(* - single-function, single-target Decisional Second Preimage Resistance (DSPR) - *) +abstract theory DSPR. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against DSPR *) + module type Adv_DSPR = { + proc guess(k : key_t, x : in_t) : bool + }. + + (* + Module used to denote the probability that a randomly sampled input + has a second preimage under a randomly sampled function from the + hash function family f. + Denotes the probability that could trivially be obtained in the + DSPR game by invariably returning 1 + *) + module SPprob(A : Adv_DSPR) = { + proc main() = { + var k : key_t; + var x : in_t; + var b : bool; + + (* Sample key k and input x *) + k <$ dkey; + x <$ din; + + (* Ask adversary to determine whether x has a preimage under f k *) + b <@ A.guess(k, x); + + (* Success iff x has a second preimage under f k *) + return spexists k x; + } + }. + + (* DSPR game *) + module DSPR(A : Adv_DSPR) = { + proc main() : bool = { + var k : key_t; + var x : in_t; + var b : bool; + + (* Sample key k and input x *) + k <$ dkey; + x <$ din; + + (* Ask adversary to determine whether x has a preimage under f k *) + b <@ A.guess(k, x); + + (* Success iff adversary correctly determined whether x has a second preimage under f k *) + return spexists k x = b; + } + }. +end DSPR. + + +(* - Single-Function, Multi-Target Decisional Second Preimage Resistance (SM_DSPR) - *) +abstract theory SMDSPR. + (* Number of targets in SM_DSPR *) + const t_smdspr : { int | 1 <= t_smdspr } as ge1_tsmdspr. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against SM_DSPR *) + module type Adv_SMDSPR = { + proc guess(k : key_t, xl : in_t list) : int * bool + }. + + (* + Module used to denote the probability that could trivially be obtained in the + SM_DSPR game by invariably returning 1 + *) + module SM_SPprob(A : Adv_SMDSPR) = { + proc main() = { + var k : key_t; + var x : in_t; + var xl : in_t list; + var i : int; + var b : bool; + + + (* Sample key k *) + k <$ dkey; + + (* Construct list xl of t_smdspr randomly sampled inputs *) + xl <- []; + while (size xl < t_smdspr) { + x <$ din; + xl <- rcons xl x; + } + + (* + Ask the adversary to determine, for any input in xl, + whether the input has a second preimage w.r.t. key k + *) + (i, b) <@ A.guess(k, xl); + + (* Get input from xl at index i, as specified by the adversary *) + x <- nth witness xl i; + + (* + Success iff + (1) "0 <= i < size xl": index i provided by adversary is within the bounds of xl + (i.e., between 0 (including) and the size xl = t_smdspr (excluding)), and + (2) "spexists k x": adversary correctly determined whether x has a + second preimage under f k + *) + return 0 <= i < size xl /\ spexists k x; + } + }. + + (* SM_DSPR game *) + module SM_DSPR(A : Adv_SMDSPR) = { + proc main() = { + var k : key_t; + var x : in_t; + var xl : in_t list; + var i : int; + var b : bool; + + (* Sample key k *) + k <$ dkey; + + (* Construct list xl of t_smdspr randomly sampled inputs *) + xl <- []; + while (size xl < t_smdspr) { + x <$ din; + xl <- rcons xl x; + } + + (* + Ask the adversary to determine, for any input in xl, + whether the input has a second preimage w.r.t. key k + *) + (i, b) <@ A.guess(k, xl); + + (* Get input from xl at index i, as specified by the adversary *) + x <- nth witness xl i; + + (* + Success iff + (1) "0 <= i < size xl": index i provided by adversary is within the bounds of xl + (i.e., between 0 (including) and the size xl = t_smdspr (excluding)), and + (2) "spexists k x": adversary correctly determined whether x has a + second preimage under f k + *) + return 0 <= i < size xl /\ spexists k x = b; + } + }. + + (* + In the above: + Adv_SMDSPR(A) = max 0 (Pr[SM_DSPR(A).main() @ &m : res] - Pr[SM_SPprob.main() @ &m : res]). + *) +end SMDSPR. + + +(* - Multi-Function, Multi-Target Decisional Second Preimage Resistance (MM_DSPR) - *) +abstract theory MMDSPR. + (* Number of functions/targets in MM_DSPR *) + const t_mmdspr : { int | 1 <= t_mmdspr } as ge1_tmmdspr. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against MM_DSPR *) + module type Adv_MMDSPR = { + proc guess(kxl : (key_t * in_t) list) : int * bool + }. + + (* + Module used to denote the probability that could trivially be obtained in the + MM_DSPR game by invariably returning 1 + *) + module MM_SPprob(A : Adv_MMDSPR) = { + proc main() = { + var k : key_t; + var x : in_t; + var kx : key_t * in_t; + var kxl : (key_t * in_t) list; + var i : int; + var b : bool; + + (* + Construct list kxl of size t_mmdspr containing (key, input) pairs (k, x). + For each pair, key k and input x are both randomly sampled from + their respective distributions + *) + kxl <- []; + while (size kxl < t_mmdspr) { + k <$ dkey; + x <$ din; + kx <- (k, x); + kxl <- rcons kxl kx; + } + + (* + Ask the adversary to determine, for any (key, input) pair in kxl, + whether the input has a second preimage w.r.t. the key in the (same) pair + *) + (i, b) <@ A.guess(kxl); + + (* Get (key, input) pair kx from kxl at index i, as specified by the adversary *) + kx <- nth witness kxl i; + + (* Extract key k and, respectively, input x from kx *) + k <- kx.`1; + x <- kx.`2; + + (* + Success iff + (1) "0 <= i < size kxl": index i provided by adversary is within the bounds of kxl + (i.e., between 0 (including) and the size kxl = t_mmdspr (excluding)), and + (2) "spexists k x": x has a second preimage under f k + *) + return 0 <= i < size kxl /\ spexists k x; + } + }. + + (* MM_DSPR game *) + module MM_DSPR(A : Adv_MMDSPR) = { + proc main() : bool = { + var k : key_t; + var x : in_t; + var kx : key_t * in_t; + var kxl : (key_t * in_t) list; + var i : int; + var b : bool; + + (* + Construct list kxl of size t_mmdspr containing (key, input) pairs (k, x). + For each pair, key k and input x are both randomly sampled from + their respective distributions + *) + kxl <- []; + while (size kxl < t_mmdspr) { + k <$ dkey; + x <$ din; + kx <- (k, x); + kxl <- rcons kxl kx; + } + + (* + Ask the adversary to determine, for any (key, input) pair in kxl, + whether the input has a second preimage w.r.t. the key in the (same) pair + *) + (i, b) <@ A.guess(kxl); + + (* Get (key, input) pair kx from kxl at index i, as specified by the adversary *) + kx <- nth witness kxl i; + + (* Extract key k and, respectively, input x from kx *) + k <- kx.`1; + x <- kx.`2; + + (* + Success iff + (1) "0 <= i < size kxl": index i provided by adversary is within the bounds of kxl + (i.e., between 0 (including) and size kxl = t_mmdspr (excluding)), and + (2) "spexists k x = b": adversary correctly determined whether + x has a second preimage under f k + *) + return 0 <= i < size kxl /\ spexists k x = b; + } + }. + + (* + In the above: + Adv_MMDSPR(A) = max 0 (Pr[MM_DSPR(A).main(t) @ &m : res] - Pr[MM_SPprob(A).main(t) @ &m : res]) + *) +end MMDSPR. + + +(* - Distinct-function, Multi-target Decisional Second Preimage Resistance (DM_DSPR) - *) +abstract theory DMDSPR. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Class of adversaries against DM_DSPR *) + module type Adv_DMDSPR = { + proc pick() : key_t list + proc guess(xl : in_t list) : int * bool + }. + + (* + Module used to denote the probability that could trivially be obtained in the + DM_DSPR game by invariably returning 1 + *) + module DM_SPprob(A : Adv_DMDSPR) = { + proc main() = { + var k : key_t; + var x : in_t; + var kl : key_t list; + var xl : in_t list; + var kx : key_t * in_t; + var i : int; + var b : bool; + + (* + Ask adversary to provide a list kl of keys that will be used to index f. + As indicated in the return statement, this list must not contain duplicate + elements (so that indexing f with each element gives a distinct function) + *) + kl <@ A.pick(); + + (* + Construct list xl of a size equal to the size of kl; + each element of xl is a randomly sampled input + *) + xl <- []; + while (size xl < size kl) { + x <$ din; + xl <- rcons xl x; + } + + (* + Ask adversary to determine, for any input x in xl, whether x has a + second preimage w.r.t. the corresponding (i.e., at the same index) key in kl + *) + (i, b) <@ A.guess(xl); + + (* + Get key k and input x from kl and, respectively, xl at index i, + as specified by the adversary + *) + k <- nth witness kl i; + x <- nth witness xl i; + + (* + Success iff + (1) "0 <= i < size kl": index provided by adversary is within the bounds of kl, and + (2) "uniq kl": kl contains no duplicate elements, and + (3) "spexists k x": x has a second preimage under f k + *) + return 0 <= i < size kl /\ uniq kl /\ spexists k x; + } + }. + + (* DM_DSPR game *) + module DM_DSPR(A : Adv_DMDSPR) = { + proc main() = { + var k : key_t; + var x : in_t; + var kl : key_t list; + var xl : in_t list; + var kx : key_t * in_t; + var i : int; + var b : bool; + + (* + Ask adversary to provide a list kl of keys that will be used to index f. + As indicated in the return statement, this list must not contain duplicate + elements (so that indexing f with each element gives a distinct function) + *) + kl <@ A.pick(); + + (* + Construct list xl of a size equal to the size of kl; + each element of xl is a randomly sampled input + *) + xl <- []; + while (size xl < size kl) { + x <$ din; + xl <- rcons xl x; + } + + (* + Ask adversary to determine, for any input x in xl, whether x has a + second preimage w.r.t. the corresponding (i.e., at the same index) key in kl + *) + (i, b) <@ A.guess(xl); + + (* + Get key k and input x from kl and, respectively, xl at index i, + as specified by the adversary + *) + k <- nth witness kl i; + x <- nth witness xl i; + + (* + Success iff + (1) "0 <= i < size kl": index provided by adversary is within the bounds of kl, and + (2) "uniq kl": kl contains no duplicate elements, and + (3) "spexists k x = b": adversary correctly determined whether + x has a second preimage under f k + *) + return 0 <= i < size kl /\ uniq kl /\ spexists k x = b; + } + }. + + (* + In the above: + Adv_DMDSPR(A) = max 0 (Pr[DM_DSPR(A).main(t) @ &m : res] - Pr[DM_SPprob(A).main(t) @ &m : res]) + *) +end DMDSPR. + + +(* +-- + UnDetectability (UD). + Given a key k and output y, it is hard to determine whether y was obtained by + randomly sampling from the domain of outputs or by computing f k x where x is + randomly sampled from the domain of inputs +-- +*) +(* - single-function, single-target UnDetectability (UD) - *) +abstract theory UD. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over output type *) + op [lossless] dout : out_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against UD *) + module type Adv_UD = { + proc distinguish(k : key_t, y : out_t) : bool + }. + + (* UD game *) + module UD(A : Adv_UD) = { + proc main(b : bool) : bool = { + var k : key_t; + var x : in_t; + var y : out_t; + var b' : bool; + + (* Sample key k *) + k <$ dkey; + + (* + If b + then randomly sample input x and compute output y by applying f k to x + else randomly sample output y + *) + if (b) { + x <$ din; + y <- f k x; + } else { + y <$ dout; + } + + (* + Ask adversary to determine whether y is + (1) computed as f k x for a randomly sampled input x, or + (2) randomly sampled + *) + b' <@ A.distinguish(k, y); + + (* Directly return output of adversary *) + return b'; + } + }. +end UD. + + +(* - Single-function, Multi-target UnDetectability (SM_UD) - *) +abstract theory SMUD. + (* Number of targets in SM_UD *) + const t_smud : { int | 1 <= t_smud } as ge1_tsmud. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over output type *) + op [lossless] dout : out_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against SM_UD *) + module type Adv_SMUD = { + proc distinguish(k : key_t, yl : out_t list) : bool + }. + + (* SM_UD game *) + module SM_UD(A : Adv_SMUD) = { + proc main(b : bool) : bool = { + var k : key_t; + var x : in_t; + var y : out_t; + var yl : out_t list; + var b' : bool; + + (* Sample key k *) + k <$ dkey; + + (* + Construct list of t_smud outputs yl, where each element y is obtained as + If b + then randomly sample input x and compute y by applying f k to x + else randomly sample y + *) + yl <- []; + while (size yl < t_smud) { + if (b) { + x <$ din; + y <- f k x; + } else { + y <$ dout; + } + + yl <- rcons yl y; + } + + (* + Ask adversary to determine whether the outputs in yl are + (1) computed as f k x for a randomly sampled input x, or + (2) randomly sampled + *) + b' <@ A.distinguish(k, yl); + + (* Directly return output of adversary *) + return b'; + } + }. +end SMUD. + + +(* - Multi-function, Multi-target UnDetectability (MM_UD) - *) +abstract theory MMUD. + (* Number of functions/targets in MM_UD *) + const t_mmud : { int | 1 <= t_mmud } as ge1_tmmud. + + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over output type *) + op [lossless] dout : out_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against MM_UD *) + module type Adv_MMUD = { + proc distinguish(kyl : (key_t * out_t) list) : bool + }. + + (* MM_UD game *) + module MM_UD(A : Adv_MMUD) = { + proc main(b : bool) : bool = { + var k : key_t; + var x : in_t; + var y : out_t; + var ky : key_t * out_t; + var kyl : (key_t * out_t) list; + var b' : bool; + + (* + Construct list kyl of size t_mmud containing (key, output) pairs (k, y). + For each pair, key k is randomly sampled and output y is obtained as + If b + then randomly sample input x and compute y by applying f k to x + else randomly sample y + *) + kyl <- []; + while (size kyl < t_mmud) { + k <$ dkey; + + if (b) { + x <$ din; + y <- f k x; + } else { + y <$ dout; + } + + ky <- (k, y); + kyl <- rcons kyl ky; + } + + (* + Ask adversary to determine whether each (key, output) pair (k, y) in + in kyl is + (1) computed as f k x for a randomly sampled input x, or + (2) randomly sampled + *) + b' <@ A.distinguish(kyl); + + (* Directly return output of adversary *) + return b'; + } + }. +end MMUD. + + +(* - Distinct-function, Multi-target UnDetectability (DM_UD) - *) +abstract theory DMUD. + (* Proper distribution over input type *) + op [lossless] din : in_t distr. + + (* Proper distribution over output type *) + op [lossless] dout : out_t distr. + + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Class of adversaries against DM_UD *) + module type Adv_DMUD = { + proc pick() : key_t list + proc distinguish(yl : out_t list) : bool + }. + + (* DM_UD game *) + module DM_UD(A : Adv_DMUD) = { + proc main(b : bool) = { + var k : key_t; + var x : in_t; + var y : out_t; + var kl : key_t list; + var yl : out_t list; + var i : int; + var b' : bool; + + (* + Ask adversary to provide a list kl of keys that will be used to index f. + As indicated in the return statement, this list must not contain duplicate + elements (so that indexing f with each element gives a distinct function) + *) + kl <@ A.pick(); + + (* + Construct list yl of a size equal to the size of kl; + each element y of yl is obtained as + If b + then get key k at corresponding position from kl, randomly sample input x, + and compute y by applying f k to x + else randomly sample y + *) + yl <- []; + while (size yl < size kl) { + k <- nth witness kl (size yl); + + if (b) { + x <$ din; + y <- f k x; + } else { + y <$ dout; + } + + yl <- rcons yl y; + } + + (* + Ask adversary to determine whether each output y in yl is + (1) computed as f k x for a randomly sampled input x + (where k is the corresponding (i.e., at the same index) key in kl), or + (2) randomly sampled + *) + b' <@ A.distinguish(yl); + + (* + Return 1 iff + (1) "uniq kl": kl contains no duplicate elements, and + (2) "b'": adversary returned 1 + *) + return uniq kl /\ b'; + } + }. +end DMUD. + + +(* +-- + Interleaved Target Subset Resilience (ITSR). +-- +*) +abstract theory ITSR. +(* + (* Number of key sets *) + const ks : { int | 1 <= ks } as ge1_ks. + + (* Number of secret value sets in each key set *) + const svsks : { int | 1 <= svsks } as ge1_svsks. + + (* Number of secret values in each secret value set *) + const svsvs : { int | 1 <= svsvs } as ge1_svsvs. +*) + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* + Map from outputs of hash function to a list of tuples of the form + (key set index, secret value set index, secret value index). + *) + op g : out_t -> (int * int * int) list. + +(* + For the lists output by g, the following holds. + - Its size is equal to the number of secret value sets (i.e., svsks). + - Each tuple it contains has the same key set index. + - Each tuple it contains has a different secret value set index. + axiom size_g (y : out_t) : + size (g y) = svsks. + axiom rng_iks (x : int * int * int) (y : out_t) : + x \in g y => 0 <= x.`1 < ks. + axiom rng_sv (x : int * int * int) (y : out_t) : + x \in g y => 0 <= x.`3 < svsvs. + axiom eqiks_g (x x' : int * int * int) (y : out_t) : + x \in g y => x' \in g y => x.`1 = x'.`1. + axiom neqisvs_g (x x' : int * int * int) (y : out_t) : + x \in g y => x' \in g y => x <> x' => x.`2 <> x'.`2. +*) + + (* Composition of g with f *) + op h (k : key_t) (x : in_t) : (int * int * int) list = g (f k x). + + (* Type for oracles used in ITSR game *) + module type Oracle_ITSR = { + proc init() : unit + proc query(x : in_t) : key_t + proc get_targets() : (key_t * in_t) list + }. + + (* Default implementation of an oracle for ITSR *) + module O_ITSR_Default : Oracle_ITSR = { + var ts : (key_t * in_t) list + + (* Initialize list of targets (i.e., (key, input) pairs) to the empty list *) + proc init() : unit = { + ts <- []; + } + + (* Samples key k, adds pair (k, x) to list of targets, and returns k *) + proc query(x : in_t) : key_t = { + var k : key_t; + var kx : key_t * in_t; + + k <$ dkey; + + kx <- (k, x); + ts <- rcons ts kx; + + return k; + } + + (* Gets and returns list of targets ts *) + proc get_targets() : (key_t * in_t) list = { + return ts; + } + }. + + (* Class of adversaries against ITSR *) + module type Adv_ITSR(O : Oracle_ITSR) = { + proc find() : key_t * in_t { O.query } + }. + + (* ITSR game *) + module ITSR(A : Adv_ITSR, O : Oracle_ITSR) = { + proc main() : bool = { + var k : key_t; + var x : in_t; + var kxl : (key_t * in_t) list; + var ikssl_f, ikssl_q : (int * int * int) list; + + (* Initialize oracle O *) + O.init(); + + (* + Ask adversary to + (1) Specify (key, input) pairs (the 'targets') by querying oracle O + (2) Find a pair (k, x) that is not in the list of specified targets and for which + h k x returns a list of which each element is contained within the (combined) + list of tuples that is obtained by mapping all of the specified targets under h. + *) + (k, x) <@ A(O).find(); + + (* + Compute list of (key set index, secret value set index, secret value index) tuples + by applying h to key k and message x provided by the adversary + *) + ikssl_f <- h k x; + + (* Get the list of targets specified by the adversary *) + kxl <@ O.get_targets(); + + (* + First, construct a list for which the i-th element equals h ki xi, where + (ki, xi) denotes the i-th element (i.e., (key, input) tuple) in list kxl. + Note that this results in a list of lists of + (key set index, secret value set index, secret value index) tuples. + Then, flatten the resulting list; that is, take the tuples from all of the + lists (in the list of lists) and put them (orderly) in a single list. + *) + ikssl_q <- flatten (map (fun (kx : key_t * in_t) => h kx.`1 kx.`2) kxl); + + + (* + Success iff + (1) "(forall x, x \in ikssl_f => x \in ikssl_q)": the tuples in the list obtained + from mapping the key and input provided by the adversary under h are all + contained within the (combined) list of tuples obtained from mapping all of + the specified targets under h, and + (2) "! (k, x) \in kxl": the key and input provided by the adversary is not one + of the specified targets. + *) + return (forall x, x \in ikssl_f => x \in ikssl_q) /\ ! (k, x) \in kxl; + } + }. +end ITSR. + + +(* +-- + Pseudo-Random Function family (PRF). + By observing a function's outputs on chosen inputs, it is hard to + distinguish whether the function is a randomly sampled function from the domain + of functions with the considered domain and co-domain, or a randomly selected + function from the hash function family f (i.e., a f k where k is randomly sampled + from the domain of (indexing) keys). + Note that, in contrast to other keyed hash function properties, the PRF property + requires the indexing key to be secret +-- +*) +abstract theory PRF. + (* Proper distribution over (indexing) key type *) + op [lossless] dkey : key_t distr. + + (* Function that maps inputs of type in_t to (proper) distributions over type out_t *) + op doutm : { in_t -> out_t distr | forall x, is_lossless (doutm x) } as doutm_ll. + + (* Type for oracles used in PRF game *) + module type Oracle_PRF = { + proc init(b_init : bool) : unit + proc query(x : in_t) : out_t + }. + + (* Class of adversaries against PRF *) + module type Adv_PRF(O : Oracle_PRF) = { + proc distinguish() : bool { O.query } + }. + + (* Default implementation of an oracle for PRF *) + module O_PRF_Default : Oracle_PRF = { + var b : bool + var k : key_t + var m : (in_t, out_t) fmap + + (* + Initializes b to given b_init, k to randomly sampled value from dkey, + and m to the empty map + *) + proc init(b_init : bool) : unit = { + b <- b_init; + k <$ dkey; + m <- empty; + } + + (* + Query the oracle on input x, returning + if b + then if x is not yet in map m + then value randomly sampled from distribution doutm x + else value at m.[x] + else f k x + *) + proc query(x : in_t) : out_t = { + var y : out_t; + + if (b) { + if (x \notin m) { + y <$ doutm x; + m.[x] <- y; + } + y <- (oget m.[x]); + } else { + y <- f k x; + } + + return y; + } + }. + + (* PRF game *) + module PRF(A : Adv_PRF, O : Oracle_PRF) = { + proc main(b : bool) : bool = { + var b' : bool; + + (* Initialize function used by oracle *) + O.init(b); + + (* + Ask adversary to determine whether the function used by the oracle is + (1) a random function with domain in_t and co-domain out_t, or + (2) of the form f k for a randomly sampled k + *) + b' <@ A(O).distinguish(); + + (* Directly return output of adversary *) + return b'; + } + }. +end PRF.