From e23e2f9b5aad7b20dbbfa68300823a32853a5632 Mon Sep 17 00:00:00 2001 From: Matthias Meijers Date: Mon, 25 Nov 2024 19:39:47 +0100 Subject: [PATCH 1/3] Additional generic binding proof (lemma 4.11) and postponing INDCCA proof KDF PP due to annoying oracle reasoning. --- proofs/KeyEncapsulationMechanisms.eca | 380 +++++++++++++++++++++++++- tmp/KEM_KDFBinding.eca | 155 +++++++++++ tmp/KEM_KDF_PP_BINDING.eca | 164 +++++++++++ properties.txt => tmp/properties.txt | 0 4 files changed, 697 insertions(+), 2 deletions(-) create mode 100644 tmp/KEM_KDFBinding.eca create mode 100644 tmp/KEM_KDF_PP_BINDING.eca rename properties.txt => tmp/properties.txt (100%) diff --git a/proofs/KeyEncapsulationMechanisms.eca b/proofs/KeyEncapsulationMechanisms.eca index 51b9e33..e6df743 100644 --- a/proofs/KeyEncapsulationMechanisms.eca +++ b/proofs/KeyEncapsulationMechanisms.eca @@ -3753,7 +3753,7 @@ proof. by byequiv => //; sim. qed. Relation between HON-BIND-CT-K (for arbitrary adversary) and HON-BIND-CT-PK (with above reduction adversary). Requires generated public keys to be different. - (Shows HON-BIND-CT-PK + Different PKs --> HON-BIND-K-PK.) + (Shows HON-BIND-CT-PK + Different PKs --> HON-BIND-CT-K.) **) lemma Bnd_HON_CT_K_PK &m : Pr[HON_BIND(S, O0, O1, A).main(CT_Binds_K) @ &m : res] @@ -3816,7 +3816,137 @@ qed. end section. -(** Reduction adversary reducing LEAK-BIND-K-CT and LEAK-BIND-PKK-CT **) +(** + Reduction adversary reducing HON-BIND-K-CT (resp. HON-BIND-K,CT-PK) + to HON-BIND-K-PK in the case of unequal ciphertexts (resp. equal ciphertexts) +**) +module (R_HON_KCT_KCTPK_KPK (A : Adv_HONBIND) : Adv_HONBIND) (O0 : Oracles_CCA, O1 : Oracles_CCA) = { + proc choose(bc : bindconf) : bool = { + return true; + } + + proc find(bc : bindconf, pk0 : pk_t, pk1 : pk_t) : ctxt_t * ctxt_t = { + var b : bool; + var c0, c1 : ctxt_t; + + (c0, c1) <@ A(O0, O1).find(K_Binds_PK, pk0, pk1); + + return (c0, c1); + } +}. + + +section. + +(* Declare arbitrary KEM S *) +declare module S <: Scheme. + +(* Declare arbitrary CCA1 oracles O0 and O1 (with initialization) *) +declare module O0 <: Oracles_CCA1i{-S}. +declare module O1 <: Oracles_CCA1i{-S, -O0}. + +(* Declare arbtirary HON-BIND adversary A *) +declare module A <: Adv_HONBIND{-S, -O0, -O1}. + +(* + Auxiliary module equivalent to HON_BIND, but with certain variables + defined global instead of local (so we can refer to them in proofs). +*) +local module HON_BIND_V = { + var c0, c1 : ctxt_t + + proc main(bc : bindconf) : bool = { + var pk0, pk1 : pk_t; + var sk0, sk1 : sk_t; + var b : bool; + var k0, k1 : key_t option; + var no_fail : bool; + + (pk0, sk0) <@ S.keygen(); + + if (is_pkbsc bc) { (* public key is binding source, equalize key pairs *) + (pk1, sk1) <- (pk0, sk0); + } 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); + + (c0, c1) <@ A(O0(S), O1(S)).find(bc, pk0, pk1); + + k0 <@ S.decaps(sk0, c0); + k1 <@ S.decaps(sk1, c1); + + no_fail <- k0 <> None /\ k1 <> None; + + return no_fail /\ is_bindbreak bc (oget k0) (oget k1) pk0 pk1 c0 c1; + } +}. + +(* + Equivalence (expressed as equality of probabilities) between + original HON_BIND and (auxiliary) HON_BIND_V. +*) +local lemma EqPr_HONBIND_V &m (bc : bindconf) : + Pr[HON_BIND(S, O0, O1, A).main(bc) @ &m : res] + = + Pr[HON_BIND_V.main(bc) @ &m : res]. +proof. by byequiv => //; sim. qed. + +(** + Relation between HON-BIND-K-PK (for arbitrary adversary) + and HON-BIND-K-CT and HON-BIND-K,CT-PK (with above reduction adversary). + Requires generated public keys to be different. + (Shows HON-BIND-K-CT + HON-BIND-K,CT-PK --> HON-BIND-K-PK.) +**) +lemma Bnd_HON_KPK_KCT_KCTPK &m : + Pr[HON_BIND(S, O0, O1, A).main(K_Binds_PK) @ &m : res] + <= + Pr[HON_BIND(S, O0, O1, R_HON_KCT_KCTPK_KPK(A)).main(K_Binds_CT) @ &m : res] + + Pr[HON_BIND(S, O0, O1, R_HON_KCT_KCTPK_KPK(A)).main(KCT_Binds_PK) @ &m : res]. +proof. +rewrite EqPr_HONBIND_V Pr[mu_split HON_BIND_V.c0 <> HON_BIND_V.c1] StdOrder.RealOrder.ler_add. ++ byequiv => //. + proc; inline R_HON_KCT_KCTPK_KPK. + wp; do 2! call (: true). + wp; call (: ={glob S, glob O0, glob O1}); 1..2: by sim. + seq 1 1 : ( ={glob S, glob O0, glob O1, glob A, pk0, sk0} + /\ bc{1} = K_Binds_PK + /\ bc{2} = K_Binds_CT); 1: by call (: true). + wp => /=; do 2! (call (: ={glob S}); 1..3: by sim). + rcondf{1} ^if; 1: by auto. + rcondf{2} ^if; 1: by auto. + rcondt{1} ^if; 1: by auto. + rcondf{2} ^if; 1: by auto. + rcondt{2} ^if; 1: by auto. + by call (: true); wp. +byequiv => //. +proc; inline R_HON_KCT_KCTPK_KPK. +wp; do 2! call (: true). +wp; call (: ={glob S, glob O0, glob O1}); 1..2: by sim. +seq 1 1 : ( ={glob S, glob O0, glob O1, glob A, pk0, sk0} + /\ bc{1} = K_Binds_PK + /\ bc{2} = KCT_Binds_PK); 1: by call (: true). +wp => /=; do 2! (call (: ={glob S}); 1..3: by sim). +rcondf{1} ^if; 1: by auto. +rcondf{2} ^if; 1: by auto. +rcondt{1} ^if; 1: by auto. +rcondt{2} ^if; 1: by auto. +by call (: true). +qed. + +end section. + + +(** Reduction adversary reducing LEAK-BIND-K-CT to LEAK-BIND-PKK-CT **) module (R_LEAK_K_PKK_CT (A : Adv_LEAKBIND) : Adv_LEAKBIND) = { proc choose(bc : bindconf) : bool = { return false; @@ -4039,6 +4169,127 @@ qed. end section. +(** + Reduction adversary reducing LEAK-BIND-K-CT (resp. LEAK-BIND-K,CT-PK) + to LEAK-BIND-K-PK in the case of unequal ciphertexts (resp. equal ciphertexts) +**) +module R_LEAK_KCT_KCTPK_KPK (A : Adv_LEAKBIND) : Adv_LEAKBIND = { + proc choose(bc : bindconf) : bool = { + return true; + } + + 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; + + (c0, c1) <@ A.find(K_Binds_PK, pk0, sk0, pk1, sk1); + + return (c0, c1); + } +}. + + +section. + +(* Declare arbitrary KEM S *) +declare module S <: Scheme. + +(* Declare arbtirary LEAK-BIND adversary A *) +declare module A <: Adv_LEAKBIND{-S}. + +(* + Auxiliary module equivalent to LEAK_BIND, but with certain variables + defined global instead of local (so we can refer to them in proofs). +*) +local module LEAK_BIND_V = { + var c0, c1 : ctxt_t + + proc main(bc : bindconf) : bool = { + var pk0, pk1 : pk_t; + var sk0, sk1 : sk_t; + var b : bool; + var k0, k1 : key_t option; + var no_fail : bool; + + (pk0, sk0) <@ S.keygen(); + + if (is_pkbsc bc) { (* public key is binding source, equalize key pairs *) + (pk1, sk1) <- (pk0, sk0); + } 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); + + k0 <@ S.decaps(sk0, c0); + k1 <@ S.decaps(sk1, c1); + + no_fail <- k0 <> None /\ k1 <> None; + + return no_fail /\ is_bindbreak bc (oget k0) (oget k1) pk0 pk1 c0 c1; + } +}. + +(* + Equivalence (expressed as equality of probabilities) between + original LEAK_BIND and (auxiliary) LEAK_BIND_V. +*) +local lemma EqPr_LEAKBIND_V &m (bc : bindconf) : + Pr[LEAK_BIND(S, A).main(bc) @ &m : res] + = + Pr[LEAK_BIND_V.main(bc) @ &m : res]. +proof. by byequiv => //; sim. qed. + +(** + Relation between LEAK-BIND-K-PK (for arbitrary adversary) + and LEAK-BIND-K-CT and LEAK-BIND-K,CT-PK (with above reduction adversary). + Requires generated public keys to be different. + (Shows LEAK-BIND-K-CT + LEAK-BIND-K,CT-PK --> LEAK-BIND-K-PK.) +**) +lemma Bnd_LEAK_KPK_KCT_KCTPK &m : + Pr[LEAK_BIND(S, A).main(K_Binds_PK) @ &m : res] + <= + Pr[LEAK_BIND(S, R_LEAK_KCT_KCTPK_KPK(A)).main(K_Binds_CT) @ &m : res] + + Pr[LEAK_BIND(S, R_LEAK_KCT_KCTPK_KPK(A)).main(KCT_Binds_PK) @ &m : res]. +proof. +rewrite EqPr_LEAKBIND_V Pr[mu_split LEAK_BIND_V.c0 <> LEAK_BIND_V.c1] StdOrder.RealOrder.ler_add. ++ byequiv => //. + proc; inline R_LEAK_KCT_KCTPK_KPK. + wp; do 2! call (: true). + wp; call (: true); wp => /=. + seq 1 1 : ( ={glob S, glob A, pk0, sk0} + /\ bc{1} = K_Binds_PK + /\ bc{2} = K_Binds_CT); 1: by call (: true). + rcondf{1} ^if; 1: by auto. + rcondf{2} ^if; 1: by auto. + rcondt{1} ^if; 1: by auto. + rcondf{2} ^if; 1: by auto. + rcondt{2} ^if; 1: by auto. + by call (: true); wp. +byequiv => //. +proc; inline R_LEAK_KCT_KCTPK_KPK. +wp; do 2! call (: true). +wp; call (: true); wp => /=. +seq 1 1 : ( ={glob S, glob A, pk0, sk0} + /\ bc{1} = K_Binds_PK + /\ bc{2} = KCT_Binds_PK); 1: by call (: true). +rcondf{1} ^if; 1: by auto. +rcondf{2} ^if; 1: by auto. +rcondt{1} ^if; 1: by auto. +rcondt{2} ^if; 1: by auto. +by call (: true). +qed. + +end section. + + (** Reduction adversary reducing MAL-BIND-K-CT to MAL-BIND-PKK-CT **) module R_MAL_K_PKK_CT (A : Adv_MALBIND) : Adv_MALBIND = { proc choose(bc : bindconf) : malbind_scenario = { @@ -4168,4 +4419,129 @@ by wp; call(: true); skip => /> /#. qed. +(** + Reduction adversary reducing MAL-BIND-K-CT (resp. MAL-BIND-K,CT-PK) + to MAL-BIND-K-PK in the case of unequal ciphertexts (resp. equal ciphertexts) +**) +module R_MAL_KCT_KCTPK_KPK (A : Adv_MALBIND) : Adv_MALBIND = { + proc choose(bc : bindconf) : malbind_scenario = { + var mbs : malbind_scenario; + + mbs <@ A.choose(K_Binds_PK); + + return mbs; + } + + proc find_dd = A.find_dd + proc find_ed = A.find_ed + proc find_ee = A.find_ee +}. + +section. + +(* Declare arbitrary KEM S *) +declare module S <: SchemeDerand. + +(* Declare arbtirary MAL-BIND adversary A *) +declare module A <: Adv_MALBIND{-S}. + + +(* + Auxiliary module equivalent to MAL_BIND, but with certain variables + defined global instead of local (so we can refer to them in proofs). +*) +local module MAL_BIND_V = { + var c0, c1 : ctxt_t + + proc main(bc : bindconf) : bool = { + var mbs : malbind_scenario; + var sk0, sk1 : sk_t; + var r0, r1 : rand_t; + var k0, k1 : key_t; + var k0o, k1o : key_t option; + var pk0, pk1 : pk_t; + var no_fail, is_bb : bool; + + mbs <@ A.choose(bc); + + if (mbs = DECAPS_DECAPS) { + (sk0, sk1, c0, c1) <@ A.find_dd(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + k0o <@ S.decaps(sk0, c0); + k1o <@ S.decaps(sk1, c1); + + no_fail <- k0o <> None /\ k1o <> None; + is_bb <- is_bindbreak bc (oget k0o) (oget k1o) pk0 pk1 c0 c1; + } elif (mbs = ENCAPS_DECAPS) { + (sk0, sk1, r0, c1) <@ A.find_ed(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + k1o <@ S.decaps(sk1, c1); + + no_fail <- k1o <> None; + is_bb <- is_bindbreak bc k0 (oget k1o) pk0 pk1 c0 c1; + } else { (* mbs = ENCAPS_ENCAPS *) + (sk0, sk1, r0, r1) <@ A.find_ee(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + (k1, c1) <@ S.encaps(pk1, r1); + + no_fail <- true; + is_bb <- is_bindbreak bc k0 k1 pk0 pk1 c0 c1; + } + + return no_fail /\ is_bb; + } +}. + +(* + Equivalence (expressed as equality of probabilities) between + original MAL_BIND and (auxiliary) MAL_BIND_V. +*) +local lemma EqPr_MALBIND_V &m (bc : bindconf) : + Pr[MAL_BIND(S, A).main(bc) @ &m : res] + = + Pr[MAL_BIND_V.main(bc) @ &m : res]. +proof. by byequiv => //; sim. qed. + +(** + Relation between MAL-BIND-K-PK (for arbitrary adversary) + and MAL-BIND-K-CT and MAL-BIND-K,CT-PK (with above reduction adversary). + Requires generated public keys to be different. + (Shows MAL-BIND-K-CT + MAL-BIND-K,CT-PK --> MAL-BIND-K-PK.) +**) +lemma Bnd_MAL_KPK_KCT_KCTPK &m : + Pr[MAL_BIND(S, A).main(K_Binds_PK) @ &m : res] + <= + Pr[MAL_BIND(S, R_MAL_KCT_KCTPK_KPK(A)).main(K_Binds_CT) @ &m : res] + + Pr[MAL_BIND(S, R_MAL_KCT_KCTPK_KPK(A)).main(KCT_Binds_PK) @ &m : res]. +proof. +rewrite EqPr_MALBIND_V Pr[mu_split MAL_BIND_V.c0 <> MAL_BIND_V.c1] StdOrder.RealOrder.ler_add. ++ byequiv => //. + proc; inline R_MAL_KCT_KCTPK_KPK(A).choose. + seq 1 3 : ( ={glob S, glob A, mbs} + /\ bc{1} = K_Binds_PK + /\ bc{2} = K_Binds_CT); 1: by wp; call (: true); wp. + if => //; 1: by wp; do 2! call (: true); wp; call (: true). + by if => //; wp; do 2! call (: true); wp; call (: true). +byequiv => //. +proc; inline R_MAL_KCT_KCTPK_KPK(A).choose. +seq 1 3 : ( ={glob S, glob A, mbs} + /\ bc{1} = K_Binds_PK + /\ bc{2} = KCT_Binds_PK); 1: by wp; call (: true); wp. +if => //; 1: by wp; do 2! call (: true); wp; call (: true). +by if => //; wp; do 2! call (: true); wp; call (: true). +qed. + +end section. + end Relations. diff --git a/tmp/KEM_KDFBinding.eca b/tmp/KEM_KDFBinding.eca new file mode 100644 index 0000000..a0c976d --- /dev/null +++ b/tmp/KEM_KDFBinding.eca @@ -0,0 +1,155 @@ +require import AllCore Distr. +require KeyEncapsulationMechanismsROM. +require KeyedHashFunctions. + + +(* 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. + + +(* Operators *) +(** Key derivation function (keyed hash function) **) +op kdf : key_t -> ctxt_t -> key_t. + + +(* Clones and imports *) +(* Definitions and properties for KEMs in ROM *) +clone import KeyEncapsulationMechanismsROM as KEMsROM with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t, + + type in_t <- in_t, + type out_t <- out_t + + proof *. + +(* Also import definitions and properteis for non-ROM KEMs and random oracles *) +import KEMs F_RO. + +op dkeypm : pk_t -> key_t distr. + +(* Indistinguishability properties *) +clone import IND with + op dkeym <- dkeypm + + proof *. + + +(** Definitions and properties for keyed hash functions **) +clone import KeyedHashFunctions as KHFs with + type key_t <- key_t, + type in_t <- ctxt_t, + type out_t <- key_t + + proof *. + + +print PRF. + +op [lossless] dkey : key_t distr. +op dkeycm : { ctxt_t -> key_t distr | forall c, is_lossless (dkeycm c) } as dkeycm_ll. + +clone import PRF as KDFPRF with + op dkey <- dkey, + op doutm <- dkeycm + + proof *. + realize dkey_ll by exact: dkey_ll. + realize doutm_ll by exact: dkeycm_ll. + + +module KEM_KDF_PP (S : Scheme) : Scheme = { + proc keygen = S.keygen + + proc encaps(pk : pk_t) : key_t * ctxt_t = { + var k, kpp : key_t; + var c : ctxt_t; + + (k, c) <@ S.encaps(pk); + kpp <- kdf k c; + + return (kpp, c); + } + + proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + + ko <@ S.decaps(sk, c); + kppo <- if ko = None then None else Some (kdf (oget ko) c); + + return kppo; + } +}. + + +module (R_INDCCA_INDCCA (A : Adv_INDCCA) : Adv_INDCCA) (O : Oracles_CCA) = { + module O_R_CCA : Oracles_CCA = { + proc decaps(c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + + ko <@ O.decaps(c); + kppo <- if ko = None then None else Some (kdf (oget ko) c); + + return kppo; + } + } + + proc distinguish(pk : pk_t, k : key_t, c : ctxt_t) : bool = { + var b : bool; + var kpp : key_t; + + kpp <- kdf k c; + + b <@ A(O_R_CCA).distinguish(pk, kpp, c); + + return b; + } +}. + +module (R_PRF_INDCCA (S : Scheme, A : Adv_INDCCA) : Adv_PRF) (O : Oracle_PRF) = { + module O_R_CCA = { + var sk : sk_t + + proc decaps(c : ctxt_t) : key_t option = { + + } + } + + proc distinguish() : bool = { + var pk : pk_t; + + + (pk, sk) <@ S.keygen(); + k <$ dkey; + + + } +}. + +module + +section. + +declare module S <: Scheme. + + + +end section. diff --git a/tmp/KEM_KDF_PP_BINDING.eca b/tmp/KEM_KDF_PP_BINDING.eca new file mode 100644 index 0000000..e03d7b9 --- /dev/null +++ b/tmp/KEM_KDF_PP_BINDING.eca @@ -0,0 +1,164 @@ +require import AllCore Distr. +require KeyEncapsulationMechanismsROM. +require KeyedHashFunctions. + + +(* 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. + + +(* Operators *) +(** Key derivation function (keyed hash function) **) +op kdf : key_t -> ctxt_t -> key_t. + + +(* Distributions *) +(** **) +op dkeym : pk_t -> key_t distr. + + +(* Clones and imports *) +(* Definitions and properties for KEMs in ROM *) +clone import KeyEncapsulationMechanismsROM as KEMsROM with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t, + + type in_t <- key_t * ctxt_t, + type out_t <- key_t + + proof *. + +import KEMs F_RO. + +(* Indistinguishability properties (in ROM) *) +clone import INDROM with + op dkeym <- dkeym + + proof *. + +import IND. + + +module (KEM_KDF_PP (S : Scheme) : Scheme_ROM) (RO : RandomOracle) = { + proc keygen = S.keygen + + proc encaps(pk : pk_t) : key_t * ctxt_t = { + var k, kpp : key_t; + var c : ctxt_t; + + (k, c) <@ S.encaps(pk); + kpp <@ RO.get((k, c)); + + return (kpp, c); + } + + proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + var kpp : key_t; + + ko <@ S.decaps(sk, c); + + if (ko = None) { + kppo <- None; + } else { + kpp <@ RO.get((oget ko, c)); + kppo <- Some kpp; + } + + return kppo; + } +}. + +(* Class of adversaries againt CR (of a random oracle) *) +module type Adv_CR_ROM (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t) * (key_t * ctxt_t) +}. + +(* CR (of a random oracle) game *) +module CR_ROM (RO : RandomOraclei, A : Adv_CR_ROM) = { + proc main() = { + var kc, kc' : key_t * ctxt_t; + var k, k' : key_t; + + RO.init(); + + (kc, kc') <@ A(RO).find(); + + k <@ RO.get(kc); + k' <@ RO.get(kc'); + + return kc <> kc' /\ k = k'; + } +}. + + +module (R_INDCCA_INDCCAROM (RO : RandomOraclei) (A : Adv_INDCCA_ROM) : Adv_INDCCA) (O : Oracles_CCA) = { + module O_R_CCA : Oracles_CCA = { + proc decaps(c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + var kpp : key_t; + + ko <@ O.decaps(c); + if (ko = None) { + kppo <- None; + } else { + kpp <@ RO.get((oget ko, c)); + kppo <- Some kpp; + } + + return kppo; + } + } + + proc distinguish(pk : pk_t, k : key_t, c : ctxt_t) : bool = { + var b : bool; + var kpp : key_t; + + RO.init(); + + kpp <@ RO.get((k, c)); + + b <@ A(RO, O_R_CCA).distinguish(pk, kpp, c); + + return b; + } +}. + + +section. + +declare module S <: Scheme{-RO, -O_CCA2_Default}. + +declare module A <: Adv_INDCCA_ROM{-S, -RO, -O_CCA2_Default}. + +module O_CCA2_Default_ROM (RO : RandomOracle) (S : Scheme) = O_CCA2_Default(S). + +local lemma test : + equiv[IND_CCA_ROM(RO, KEM_KDF_PP(S), O_CCA2_Default_ROM, A).main ~ IND_CCA(S, O_CCA2_Default, R_INDCCA_INDCCAROM(RO, A)).main : ={glob S, glob A} ==> ={res}]. +proof. +proc. +inline{1} 2; inline{2} 6. +inline{1} 3. +(** Idea: If b = 0, match random oracle gets, if b = 1, match sampling LHS with random oracle get on RHS; might be easier to do provided bit variant **) +admit. +qed. + +end section. diff --git a/properties.txt b/tmp/properties.txt similarity index 100% rename from properties.txt rename to tmp/properties.txt From d0d61310f95692b9014ed0cf19c4332eb380bdbe Mon Sep 17 00:00:00 2001 From: Matthias Meijers Date: Mon, 25 Nov 2024 21:01:50 +0100 Subject: [PATCH 2/3] Setup MALBIND K CT proof in case of post-processing K and CT through KDF. --- proofs/KEM_KDF_PP_Binding.eca | 184 ++++++++++++++++++++++++++++++++++ 1 file changed, 184 insertions(+) create mode 100644 proofs/KEM_KDF_PP_Binding.eca diff --git a/proofs/KEM_KDF_PP_Binding.eca b/proofs/KEM_KDF_PP_Binding.eca new file mode 100644 index 0000000..612df56 --- /dev/null +++ b/proofs/KEM_KDF_PP_Binding.eca @@ -0,0 +1,184 @@ +require import AllCore Distr. +require KeyEncapsulationMechanismsROM. + + +(* 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. + +(** Randomness **) +type rand_t. + +(* Inputs to the random oracle *) +type in_t. + +(* Outputs of the random oracle *) +type out_t. + + +(* Operators *) +(** Key derivation function (keyed hash function) **) +op kdf : key_t -> ctxt_t -> key_t. + + +(* Distributions *) +(** **) +op dkeym : pk_t -> key_t distr. + + +(* Clones and imports *) +(* Definitions and properties for KEMs in ROM *) +clone import KeyEncapsulationMechanismsROM as KEMsROM with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t, + + type in_t <- key_t * ctxt_t, + type out_t <- key_t + + proof *. + +clone import MALBINDROM with + type rand_t <- rand_t. + +import MALBIND KEMs F_RO. + +(* Indistinguishability properties (in ROM) *) +clone import INDROM with + op dkeym <- dkeym + + proof *. + +import IND. + + +module (KEM_KDF_PP_Ct (S : SchemeDerand) : SchemeDerand_ROM) (RO : RandomOracle) = { + proc keygen = S.keygen + + proc encaps(pk : pk_t, r : rand_t) : key_t * ctxt_t = { + var k, kpp : key_t; + var c : ctxt_t; + + (k, c) <@ S.encaps(pk, r); + kpp <@ RO.get((k, c)); + + return (kpp, c); + } + + proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + var kpp : key_t; + + ko <@ S.decaps(sk, c); + + if (ko = None) { + kppo <- None; + } else { + kpp <@ RO.get((oget ko, c)); + kppo <- Some kpp; + } + + return kppo; + } +}. + +(* Class of adversaries againt CR (of a random oracle) *) +module type Adv_CR_ROM (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t) * (key_t * ctxt_t) +}. + +(* CR (of a random oracle) game *) +module CR_ROM (RO : RandomOraclei, A : Adv_CR_ROM) = { + proc main() = { + var kc, kc' : key_t * ctxt_t; + var k, k' : key_t; + + RO.init(); + + (kc, kc') <@ A(RO).find(); + + k <@ RO.get(kc); + k' <@ RO.get(kc'); + + return kc <> kc' /\ k = k'; + } +}. + + +module (R_KCT_CR (S : SchemeDerand) (A : Adv_MALBIND_ROM) : Adv_CR_ROM) (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t) * (key_t * ctxt_t) = { + var mbs : malbind_scenario; + var sk0, sk1 : sk_t; + var r0, r1 : rand_t; + var c0, c1 : ctxt_t; + var k0, k1 : key_t; + var k0o, k1o : key_t option; + var pk0, pk1 : pk_t; + var kc0, kc1 : key_t * ctxt_t; + + mbs <@ A(RO).choose(K_Binds_CT); + + if (mbs = DECAPS_DECAPS) { + (sk0, sk1, c0, c1) <@ A(RO).find_dd(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + k0o <@ S.decaps(sk0, c0); + k1o <@ S.decaps(sk1, c1); + + kc0 <- (oget k0o, c0); + kc1 <- (oget k1o, c1); + } elif (mbs = ENCAPS_DECAPS) { + (sk0, sk1, r0, c1) <@ A(RO).find_ed(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + k1o <@ S.decaps(sk1, c1); + + kc0 <- (k0, c0); + kc1 <- (oget k1o, c1); + } else { (* mbs = ENCAPS_ENCAPS *) + (sk0, sk1, r0, r1) <@ A(RO).find_ee(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + (k1, c1) <@ S.encaps(pk1, r1); + + kc0 <- (k0, c0); + kc1 <- (k1, c1); + } + + return (kc0, kc1); + } +}. + + + +section. + +declare module S <: SchemeDerand{-RO}. + +declare module A <: Adv_MALBIND_ROM{-S, -RO}. + +local lemma test : + equiv[MAL_BIND_ROM(RO, KEM_KDF_PP_Ct(S), A).main ~ CR_ROM(RO, R_KCT_CR(S, A)).main : ={glob S, glob A} /\ arg{1} = K_Binds_CT ==> res{1} => res{2}]. +proof. + +qed. + +end section. From d2072a0d9297ecc0ab37214244ebdccc3dbf4ba1 Mon Sep 17 00:00:00 2001 From: Matthias Meijers Date: Tue, 26 Nov 2024 18:50:32 +0100 Subject: [PATCH 3/3] Finish binding of CT/PK by post-processing KEM encaps and decaps with KDF (modeled as RO) --- proofs/KEM_KDF_PP.eca | 748 ++++++++++++++++++++++++++++++++++ proofs/KEM_KDF_PP_Binding.eca | 184 --------- 2 files changed, 748 insertions(+), 184 deletions(-) create mode 100644 proofs/KEM_KDF_PP.eca delete mode 100644 proofs/KEM_KDF_PP_Binding.eca diff --git a/proofs/KEM_KDF_PP.eca b/proofs/KEM_KDF_PP.eca new file mode 100644 index 0000000..fa2b2c7 --- /dev/null +++ b/proofs/KEM_KDF_PP.eca @@ -0,0 +1,748 @@ +require import AllCore Distr. +require KeyEncapsulationMechanismsROM. + + +(* 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. + +(** Randomness **) +type rand_t. + + +(** + Considers the case where the post-processing is done + by passing the symmetric key and encapsulation (obtained from any other KEM) + to a KDF (modeled as a RO). +**) +theory PPKDFKCT. +(* Clones and imports *) +(* Definitions for KEMs in ROM *) +clone import KeyEncapsulationMechanismsROM as KEMsROM with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t, + + type in_t <- key_t * ctxt_t, + type out_t <- key_t + + proof *. + +(* Definitions for malicious binding in ROM *) +clone import MALBINDROM with + type rand_t <- rand_t. + +import MALBIND KEMs F_RO. + + +(* Properties (other) *) +(** Class of adversaries againt CR in ROM **) +module type Adv_CR_ROM (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t) * (key_t * ctxt_t) +}. + +(** CR game in ROM **) +module CR_ROM (RO : RandomOraclei, A : Adv_CR_ROM) = { + proc main() = { + var kc, kc' : key_t * ctxt_t; + var k, k' : key_t; + + RO.init(); + + (kc, kc') <@ A(RO).find(); + + k <@ RO.get(kc); + k' <@ RO.get(kc'); + + return kc <> kc' /\ k = k'; + } +}. + + +(* Scheme *) +(** + KEM that simply adds a post-processing step to the encapsulation and decapsulation + of the provided KEM (processing the symmetric key and encapsulation/ciphertext). +**) +(** + Note, the KEMs (both provided and constructed) are of the "derandomized KEM" type + because we will mainly be considering malicious binding properties. +**) +module (KEM_KDF_PP_CT (S : SchemeDerand) : SchemeDerand_ROM) (RO : RandomOracle) = { + proc keygen = S.keygen + + proc encaps(pk : pk_t, r : rand_t) : key_t * ctxt_t = { + var k, kpp : key_t; + var c : ctxt_t; + + (k, c) <@ S.encaps(pk, r); + kpp <@ RO.get((k, c)); + + return (kpp, c); + } + + proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + var kpp : key_t; + + ko <@ S.decaps(sk, c); + + if (ko = None) { + kppo <- None; + } else { + kpp <@ RO.get((oget ko, c)); + kppo <- Some kpp; + } + + return kppo; + } +}. + + +(** Reduction adversary reducing from CR (in ROM) to MAL-BIND-K-CT (in ROM) **) +module (R_KCT_CR (S : SchemeDerand) (A : Adv_MALBIND_ROM) : Adv_CR_ROM) (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t) * (key_t * ctxt_t) = { + var mbs : malbind_scenario; + var sk0, sk1 : sk_t; + var r0, r1 : rand_t; + var c0, c1 : ctxt_t; + var k0, k1 : key_t; + var k0o, k1o : key_t option; + var pk0, pk1 : pk_t; + var kc0, kc1 : key_t * ctxt_t; + + mbs <@ A(RO).choose(K_Binds_CT); + + if (mbs = DECAPS_DECAPS) { + (sk0, sk1, c0, c1) <@ A(RO).find_dd(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + k0o <@ S.decaps(sk0, c0); + k1o <@ S.decaps(sk1, c1); + + kc0 <- (oget k0o, c0); + kc1 <- (oget k1o, c1); + } elif (mbs = ENCAPS_DECAPS) { + (sk0, sk1, r0, c1) <@ A(RO).find_ed(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + k1o <@ S.decaps(sk1, c1); + + kc0 <- (k0, c0); + kc1 <- (oget k1o, c1); + } else { (* mbs = ENCAPS_ENCAPS *) + (sk0, sk1, r0, r1) <@ A(RO).find_ee(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + (k1, c1) <@ S.encaps(pk1, r1); + + kc0 <- (k0, c0); + kc1 <- (k1, c1); + } + + return (kc0, kc1); + } +}. + + + +section. +(* Declare arbitrary ("derandomized") KEM *) +declare module S <: SchemeDerand{-RO}. + +(* Declare arbitrary MAL-BIND adversary (in ROM)*) +declare module A <: Adv_MALBIND_ROM{-S, -RO}. + +(* By assumption, the distribution(s) that the random oracle samples from is (are) Lossless *) +declare axiom dout_ll (kc : key_t * ctxt_t) : is_lossless (dout kc). + +(** + Equivalence between MAL-BIND-K-CT of post-processing KEM (for arbitrary adversary) + and CR (for above reduction adversary). (Shows CR --> MAL-BIND-K-CT, in ROM) +**) +equiv Eqv_MALBINDKCT_CR_ROM : + MAL_BIND_ROM(RO, KEM_KDF_PP_CT(S), A).main ~ CR_ROM(RO, R_KCT_CR(S, A)).main : + ={glob S, glob A} /\ arg{1} = K_Binds_CT ==> res{1} => res{2}. +proof. +proc. +inline{1} 2; inline{2} 2. +seq 3 2 : (#pre /\ ={RO.m, mbs} /\ bc0{1} = bc{1}). ++ call (: ={RO.m}); 1: by sim. + by inline *; wp. +inline KEM_KDF_PP_CT(S, RO).decaps KEM_KDF_PP_CT(S, RO).encaps. +wp; if => //. ++ wp. + seq 6 4 : ( ={glob S, glob RO, sk0, sk1, c0, c1, pk0, pk1} + /\ sk{1} = sk0{1} + /\ c{1} = c0{1} + /\ bc0{1} = K_Binds_CT + /\ ko{1} = k0o{2}) => [/> |]. + + by call (: true); wp; call (: ={RO.m}); 1: sim. + case (ko{1} = None). + + rcondt{1} ^if; 1: by auto. + sp; conseq (: _ ==> true) => //. + inline RO.get; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + if{1}; 1: by wp; rnd{2}; wp; rnd{2}; wp; skip => />; smt(dout_ll). + by wp; rnd; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + swap{1} [4..6] -3; sp; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + sp 0 3; seq 1 1 : (#pre /\ kpp{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko0{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +if => //. ++ seq 1 1 : (#pre /\ ={sk0, sk1, r0, c1}); 1: by call (: ={RO.m}); 1: sim. + wp; sp. + seq 1 1 : (#pre /\ k{1} = k0{2} /\ c3{1} = c0{2}); 1: by call (: true). + swap{1} [1..2] 3; sp. + seq 1 1 : (#pre /\ ko1{1} = k1o{2}); 1: by call (: true). + sp; seq 1 1: (#pre /\ kpp1{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko1{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +inline RO.get; wp; rnd; wp. +swap{1} [12..14] -4; wp; rnd. +wp; call (: true); wp; call (: true). +wp; call (: ={RO.m}); 1: by sim. +by skip => />. +qed. + +end section. + +end PPKDFKCT. + + + +(** + Considers the case where the post-processing is done + by passing the symmetric key and public key (obtained from any other KEM) + to a KDF (modeled as a RO). +**) +theory PPKDFKPK. +(* Clones and imports *) +(* Definitions for KEMs in ROM *) +clone import KeyEncapsulationMechanismsROM as KEMsROM with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t, + + type in_t <- key_t * pk_t, + type out_t <- key_t + + proof *. + +(* Definitions for malicious binding in ROM *) +clone import MALBINDROM with + type rand_t <- rand_t. + +import MALBIND KEMs F_RO. + + +(* Properties (other) *) +(** Class of adversaries againt CR in ROM **) +module type Adv_CR_ROM (RO : RandomOracle) = { + proc find() : (key_t * pk_t) * (key_t * pk_t) +}. + +(** CR game in ROM **) +module CR_ROM (RO : RandomOraclei, A : Adv_CR_ROM) = { + proc main() = { + var kpk, kpk' : key_t * pk_t; + var k, k' : key_t; + + RO.init(); + + (kpk, kpk') <@ A(RO).find(); + + k <@ RO.get(kpk); + k' <@ RO.get(kpk'); + + return kpk <> kpk' /\ k = k'; + } +}. + + +(* Scheme *) +(** + KEM that simply adds a post-processing step to the encapsulation and decapsulation + of the provided KEM (processing the symmetric key and public key). +**) +(** + Note, the KEMs (both provided and constructed) are of the "derandomized KEM" type + because we will mainly be considering malicious binding properties. +**) +module (KEM_KDF_PP_PK (S : SchemeDerand) : SchemeDerand_ROM) (RO : RandomOracle) = { + proc keygen = S.keygen + + proc encaps(pk : pk_t, r : rand_t) : key_t * ctxt_t = { + var k, kpp : key_t; + var c : ctxt_t; + + (k, c) <@ S.encaps(pk, r); + kpp <@ RO.get((k, pk)); + + return (kpp, c); + } + + proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + var kpp : key_t; + + ko <@ S.decaps(sk, c); + + if (ko = None) { + kppo <- None; + } else { + kpp <@ RO.get((oget ko, sk2pk sk)); + kppo <- Some kpp; + } + + return kppo; + } +}. + + +(** Reduction adversary reducing from CR (in ROM) to MAL-BIND-K-PK (in ROM) **) +module (R_KPK_CR (S : SchemeDerand) (A : Adv_MALBIND_ROM) : Adv_CR_ROM) (RO : RandomOracle) = { + proc find() : (key_t * pk_t) * (key_t * pk_t) = { + var mbs : malbind_scenario; + var sk0, sk1 : sk_t; + var r0, r1 : rand_t; + var c0, c1 : ctxt_t; + var k0, k1 : key_t; + var k0o, k1o : key_t option; + var pk0, pk1 : pk_t; + var kpk0, kpk1 : key_t * pk_t; + + mbs <@ A(RO).choose(K_Binds_PK); + + if (mbs = DECAPS_DECAPS) { + (sk0, sk1, c0, c1) <@ A(RO).find_dd(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + k0o <@ S.decaps(sk0, c0); + k1o <@ S.decaps(sk1, c1); + + kpk0 <- (oget k0o, pk0); + kpk1 <- (oget k1o, pk1); + } elif (mbs = ENCAPS_DECAPS) { + (sk0, sk1, r0, c1) <@ A(RO).find_ed(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + k1o <@ S.decaps(sk1, c1); + + kpk0 <- (k0, pk0); + kpk1 <- (oget k1o, pk1); + } else { (* mbs = ENCAPS_ENCAPS *) + (sk0, sk1, r0, r1) <@ A(RO).find_ee(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + (k1, c1) <@ S.encaps(pk1, r1); + + kpk0 <- (k0, pk0); + kpk1 <- (k1, pk1); + } + + return (kpk0, kpk1); + } +}. + + + +section. +(* Declare arbitrary ("derandomized") KEM *) +declare module S <: SchemeDerand{-RO}. + +(* Declare arbitrary MAL-BIND adversary (in ROM) *) +declare module A <: Adv_MALBIND_ROM{-S, -RO}. + +(* By assumption, the distribution(s) that the random oracle samples from is (are) lossless *) +declare axiom dout_ll (kpk : key_t * pk_t) : is_lossless (dout kpk). + +(** + Equivalence between MAL-BIND-K-PK of post-processing KEM (for arbitrary adversary) + and CR (for above reduction adversary). (Shows CR --> MAL-BIND-K-PK, in ROM) +**) +equiv Eqv_MALBINDKPK_CR_ROM : + MAL_BIND_ROM(RO, KEM_KDF_PP_PK(S), A).main ~ CR_ROM(RO, R_KPK_CR(S, A)).main : + ={glob S, glob A} /\ arg{1} = K_Binds_PK ==> res{1} => res{2}. +proof. +proc. +inline{1} 2; inline{2} 2. +seq 3 2 : (#pre /\ ={RO.m, mbs} /\ bc0{1} = bc{1}). ++ call (: ={RO.m}); 1: by sim. + by inline *; wp. +inline KEM_KDF_PP_PK(S, RO).decaps KEM_KDF_PP_PK(S, RO).encaps. +wp; if => //. ++ wp. + seq 6 4 : ( ={glob S, glob RO, sk0, sk1, c0, c1, pk0, pk1} + /\ pk0{1} = sk2pk sk0{1} + /\ pk1{1} = sk2pk sk1{1} + /\ sk{1} = sk0{1} + /\ c{1} = c0{1} + /\ bc0{1} = K_Binds_PK + /\ ko{1} = k0o{2}) => [/> |]. + + by call (: true); wp; call (: ={RO.m}); 1: sim. + case (ko{1} = None). + + rcondt{1} ^if; 1: by auto. + sp; conseq (: _ ==> true) => //. + inline RO.get; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + if{1}; 1: by wp; rnd{2}; wp; rnd{2}; wp; skip => />; smt(dout_ll). + by wp; rnd; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + swap{1} [4..6] -3; sp; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + sp 0 3; seq 1 1 : (#pre /\ kpp{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko0{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +if => //. ++ seq 1 1 : (#pre /\ ={sk0, sk1, r0, c1}); 1: by call (: ={RO.m}); 1: sim. + wp; sp. + seq 1 1 : (#pre /\ k{1} = k0{2} /\ c3{1} = c0{2}); 1: by call (: true). + swap{1} [1..2] 3; sp. + seq 1 1 : (#pre /\ ko1{1} = k1o{2}); 1: by call (: true). + sp; seq 1 1: (#pre /\ kpp1{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko1{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +inline RO.get; wp; rnd; wp. +swap{1} [12..14] -4; wp; rnd. +wp; call (: true); wp; call (: true). +wp; call (: ={RO.m}); 1: by sim. +by skip => />. +qed. + +end section. + +end PPKDFKPK. + + +(** + Considers the case where the post-processing is done + by passing the symmetric key, encapsulation, and public key + (obtained from any other KEM) to a KDF (modeled as a RO). +**) +theory PPKDFKCTPK. +(* Clones and imports *) +(* Definitions for KEMs in ROM *) +clone import KeyEncapsulationMechanismsROM as KEMsROM with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t, + + type in_t <- key_t * ctxt_t * pk_t, + type out_t <- key_t + + proof *. + +(* Definitions for malicious binding in ROM *) +clone import MALBINDROM with + type rand_t <- rand_t. + +import MALBIND KEMs F_RO. + + +(* Properties (other) *) +(** Class of adversaries againt CR in ROM **) +module type Adv_CR_ROM (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t * pk_t) * (key_t * ctxt_t * pk_t) +}. + +(** CR game in ROM **) +module CR_ROM (RO : RandomOraclei, A : Adv_CR_ROM) = { + proc main() = { + var kcpk, kcpk' : key_t * ctxt_t * pk_t; + var k, k' : key_t; + + RO.init(); + + (kcpk, kcpk') <@ A(RO).find(); + + k <@ RO.get(kcpk); + k' <@ RO.get(kcpk'); + + return kcpk <> kcpk' /\ k = k'; + } +}. + + +(* Scheme *) +(** + KEM that simply adds a post-processing step to the encapsulation and decapsulation + of the provided KEM (processing the symmetric key, encapsulation, and public key). +**) +(** + Note, the KEMs (both provided and constructed) are of the "derandomized KEM" type + because we will mainly be considering malicious binding properties. +**) +module (KEM_KDF_PP_CTPK (S : SchemeDerand) : SchemeDerand_ROM) (RO : RandomOracle) = { + proc keygen = S.keygen + + proc encaps(pk : pk_t, r : rand_t) : key_t * ctxt_t = { + var k, kpp : key_t; + var c : ctxt_t; + + (k, c) <@ S.encaps(pk, r); + kpp <@ RO.get((k, c, pk)); + + return (kpp, c); + } + + proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { + var ko, kppo : key_t option; + var kpp : key_t; + + ko <@ S.decaps(sk, c); + + if (ko = None) { + kppo <- None; + } else { + kpp <@ RO.get((oget ko, c, sk2pk sk)); + kppo <- Some kpp; + } + + return kppo; + } +}. + + +(** Shared code between reduction adversaries **) +module R_S (S : SchemeDerand) (A : Adv_MALBIND_ROM) (RO : RandomOracle) = { + proc main(bc : bindconf) : (key_t * ctxt_t * pk_t) * (key_t * ctxt_t * pk_t) = { + var mbs : malbind_scenario; + var sk0, sk1 : sk_t; + var r0, r1 : rand_t; + var c0, c1 : ctxt_t; + var k0, k1 : key_t; + var k0o, k1o : key_t option; + var pk0, pk1 : pk_t; + var kcpk0, kcpk1 : key_t * ctxt_t * pk_t; + + mbs <@ A(RO).choose(bc); + + if (mbs = DECAPS_DECAPS) { + (sk0, sk1, c0, c1) <@ A(RO).find_dd(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + k0o <@ S.decaps(sk0, c0); + k1o <@ S.decaps(sk1, c1); + + kcpk0 <- (oget k0o, c0, pk0); + kcpk1 <- (oget k1o, c1, pk1); + } elif (mbs = ENCAPS_DECAPS) { + (sk0, sk1, r0, c1) <@ A(RO).find_ed(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + k1o <@ S.decaps(sk1, c1); + + kcpk0 <- (k0, c0, pk0); + kcpk1 <- (oget k1o, c1, pk1); + } else { (* mbs = ENCAPS_ENCAPS *) + (sk0, sk1, r0, r1) <@ A(RO).find_ee(); + + pk0 <- sk2pk sk0; + pk1 <- sk2pk sk1; + + (k0, c0) <@ S.encaps(pk0, r0); + (k1, c1) <@ S.encaps(pk1, r1); + + kcpk0 <- (k0, c0, pk0); + kcpk1 <- (k1, c1, pk1); + } + + return (kcpk0, kcpk1); + } +}. + +(** Reduction adversary reducing from CR (in ROM) to MAL-BIND-K-CT (in ROM) **) +module (R_KCT_CR (S : SchemeDerand) (A : Adv_MALBIND_ROM) : Adv_CR_ROM) (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t * pk_t) * (key_t * ctxt_t * pk_t) = { + var kcpk0, kcpk1 : key_t * ctxt_t * pk_t; + + (kcpk0, kcpk1) <@ R_S(S, A, RO).main(K_Binds_CT); + + return (kcpk0, kcpk1); + } +}. + +(** Reduction adversary reducing from CR (in ROM) to MAL-BIND-K-PK (in ROM) **) +module (R_KPK_CR (S : SchemeDerand) (A : Adv_MALBIND_ROM) : Adv_CR_ROM) (RO : RandomOracle) = { + proc find() : (key_t * ctxt_t * pk_t) * (key_t * ctxt_t * pk_t) = { + var kcpk0, kcpk1 : key_t * ctxt_t * pk_t; + + (kcpk0, kcpk1) <@ R_S(S, A, RO).main(K_Binds_PK); + + return (kcpk0, kcpk1); + } +}. + + +section. +(* Declare arbitrary ("derandomized") KEM *) +declare module S <: SchemeDerand{-RO}. + +(* Declare arbitrary MAL-BIND adversary (in ROM) *) +declare module A <: Adv_MALBIND_ROM{-S, -RO}. + +(* By assumption, the distribution(s) that the random oracle samples from is (are) Lossless *) +declare axiom dout_ll (kcpk : key_t * ctxt_t * pk_t) : is_lossless (dout kcpk). + + +(** + Equivalence between MAL-BIND-K-CT of post-processing KEM (for arbitrary adversary) + and CR (for above reduction adversary). (Shows CR --> MAL-BIND-K-CT, in ROM) +**) +equiv Eqv_MALBINDKCT_CR_ROM : + MAL_BIND_ROM(RO, KEM_KDF_PP_CTPK(S), A).main ~ CR_ROM(RO, R_KCT_CR(S, A)).main : + ={glob S, glob A} /\ arg{1} = K_Binds_CT ==> res{1} => res{2}. +proof. +proc. +inline{1} 2; inline{2} 2; inline{2} 2. +seq 3 3 : (#pre /\ ={RO.m, mbs} /\ bc0{1} = bc{1}). ++ call (: ={RO.m}); 1: by sim. + by inline *; wp. +inline KEM_KDF_PP_CTPK(S, RO).decaps KEM_KDF_PP_CTPK(S, RO).encaps. +wp; if => //. ++ wp. + seq 6 4 : ( ={glob S, glob RO, sk0, sk1, c0, c1, pk0, pk1} + /\ pk0{1} = sk2pk sk0{1} + /\ pk1{1} = sk2pk sk1{1} + /\ sk{1} = sk0{1} + /\ c{1} = c0{1} + /\ bc0{1} = K_Binds_CT + /\ ko{1} = k0o{2}) => [/> |]. + + by call (: true); wp; call (: ={RO.m}); 1: sim. + case (ko{1} = None). + + rcondt{1} ^if; 1: by auto. + sp; conseq (: _ ==> true) => //. + inline RO.get; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + if{1}; 1: by wp; rnd{2}; wp; rnd{2}; wp; skip => />; smt(dout_ll). + by wp; rnd; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + swap{1} [4..6] -3; sp; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + sp 0 4; seq 1 1 : (#pre /\ kpp{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko0{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +if => //. ++ seq 1 1 : (#pre /\ ={sk0, sk1, r0, c1}); 1: by call (: ={RO.m}); 1: sim. + wp; sp. + seq 1 1 : (#pre /\ k{1} = k0{2} /\ c3{1} = c0{2}); 1: by call (: true). + swap{1} [1..2] 3; sp. + seq 1 1 : (#pre /\ ko1{1} = k1o{2}); 1: by call (: true). + sp; seq 1 1: (#pre /\ kpp1{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko1{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +inline RO.get; wp; rnd; wp. +swap{1} [12..14] -4; wp; rnd. +wp; call (: true); wp; call (: true). +wp; call (: ={RO.m}); 1: by sim. +by skip => />. +qed. + +(** + Equivalence between MAL-BIND-K-PK of post-processing KEM (for arbitrary adversary) + and CR (for above reduction adversary). (Shows CR --> MAL-BIND-K-PK, in ROM) +**) +equiv Eqv_MALBINDKPK_CR_ROM : + MAL_BIND_ROM(RO, KEM_KDF_PP_CTPK(S), A).main ~ CR_ROM(RO, R_KPK_CR(S, A)).main : + ={glob S, glob A} /\ arg{1} = K_Binds_PK ==> res{1} => res{2}. +proof. +proc. +inline{1} 2; inline{2} 2; inline{2} 2. +seq 3 3 : (#pre /\ ={RO.m, mbs} /\ bc0{1} = bc{1}). ++ call (: ={RO.m}); 1: by sim. + by inline *; wp. +inline KEM_KDF_PP_CTPK(S, RO).decaps KEM_KDF_PP_CTPK(S, RO).encaps. +wp; if => //. ++ wp. + seq 6 4 : ( ={glob S, glob RO, sk0, sk1, c0, c1, pk0, pk1} + /\ pk0{1} = sk2pk sk0{1} + /\ pk1{1} = sk2pk sk1{1} + /\ sk{1} = sk0{1} + /\ c{1} = c0{1} + /\ bc0{1} = K_Binds_PK + /\ ko{1} = k0o{2}) => [/> |]. + + by call (: true); wp; call (: ={RO.m}); 1: sim. + case (ko{1} = None). + + rcondt{1} ^if; 1: by auto. + sp; conseq (: _ ==> true) => //. + inline RO.get; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + if{1}; 1: by wp; rnd{2}; wp; rnd{2}; wp; skip => />; smt(dout_ll). + by wp; rnd; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + swap{1} [4..6] -3; sp; seq 1 1 : (#pre /\ ko0{1} = k1o{2}); 1: by call (: true). + sp 0 4; seq 1 1 : (#pre /\ kpp{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko0{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +if => //. ++ seq 1 1 : (#pre /\ ={sk0, sk1, r0, c1}); 1: by call (: ={RO.m}); 1: sim. + wp; sp. + seq 1 1 : (#pre /\ k{1} = k0{2} /\ c3{1} = c0{2}); 1: by call (: true). + swap{1} [1..2] 3; sp. + seq 1 1 : (#pre /\ ko1{1} = k1o{2}); 1: by call (: true). + sp; seq 1 1: (#pre /\ kpp1{1} = k{2}); 1: by inline RO.get; wp; rnd; wp. + sp; case (ko1{1} = None). + + rcondt{1} ^if; 1: by auto. + by inline RO.get; wp; rnd{2}; wp; skip => />; smt(dout_ll). + rcondf{1} ^if; 1: by auto. + by inline RO.get; wp; rnd; wp; skip => />. +inline RO.get; wp; rnd; wp. +swap{1} [12..14] -4; wp; rnd. +wp; call (: true); wp; call (: true). +wp; call (: ={RO.m}); 1: by sim. +by skip => />. +qed. + +end section. + +end PPKDFKCTPK. diff --git a/proofs/KEM_KDF_PP_Binding.eca b/proofs/KEM_KDF_PP_Binding.eca deleted file mode 100644 index 612df56..0000000 --- a/proofs/KEM_KDF_PP_Binding.eca +++ /dev/null @@ -1,184 +0,0 @@ -require import AllCore Distr. -require KeyEncapsulationMechanismsROM. - - -(* 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. - -(** Randomness **) -type rand_t. - -(* Inputs to the random oracle *) -type in_t. - -(* Outputs of the random oracle *) -type out_t. - - -(* Operators *) -(** Key derivation function (keyed hash function) **) -op kdf : key_t -> ctxt_t -> key_t. - - -(* Distributions *) -(** **) -op dkeym : pk_t -> key_t distr. - - -(* Clones and imports *) -(* Definitions and properties for KEMs in ROM *) -clone import KeyEncapsulationMechanismsROM as KEMsROM with - type pk_t <- pk_t, - type sk_t <- sk_t, - type key_t <- key_t, - type ctxt_t <- ctxt_t, - - type in_t <- key_t * ctxt_t, - type out_t <- key_t - - proof *. - -clone import MALBINDROM with - type rand_t <- rand_t. - -import MALBIND KEMs F_RO. - -(* Indistinguishability properties (in ROM) *) -clone import INDROM with - op dkeym <- dkeym - - proof *. - -import IND. - - -module (KEM_KDF_PP_Ct (S : SchemeDerand) : SchemeDerand_ROM) (RO : RandomOracle) = { - proc keygen = S.keygen - - proc encaps(pk : pk_t, r : rand_t) : key_t * ctxt_t = { - var k, kpp : key_t; - var c : ctxt_t; - - (k, c) <@ S.encaps(pk, r); - kpp <@ RO.get((k, c)); - - return (kpp, c); - } - - proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { - var ko, kppo : key_t option; - var kpp : key_t; - - ko <@ S.decaps(sk, c); - - if (ko = None) { - kppo <- None; - } else { - kpp <@ RO.get((oget ko, c)); - kppo <- Some kpp; - } - - return kppo; - } -}. - -(* Class of adversaries againt CR (of a random oracle) *) -module type Adv_CR_ROM (RO : RandomOracle) = { - proc find() : (key_t * ctxt_t) * (key_t * ctxt_t) -}. - -(* CR (of a random oracle) game *) -module CR_ROM (RO : RandomOraclei, A : Adv_CR_ROM) = { - proc main() = { - var kc, kc' : key_t * ctxt_t; - var k, k' : key_t; - - RO.init(); - - (kc, kc') <@ A(RO).find(); - - k <@ RO.get(kc); - k' <@ RO.get(kc'); - - return kc <> kc' /\ k = k'; - } -}. - - -module (R_KCT_CR (S : SchemeDerand) (A : Adv_MALBIND_ROM) : Adv_CR_ROM) (RO : RandomOracle) = { - proc find() : (key_t * ctxt_t) * (key_t * ctxt_t) = { - var mbs : malbind_scenario; - var sk0, sk1 : sk_t; - var r0, r1 : rand_t; - var c0, c1 : ctxt_t; - var k0, k1 : key_t; - var k0o, k1o : key_t option; - var pk0, pk1 : pk_t; - var kc0, kc1 : key_t * ctxt_t; - - mbs <@ A(RO).choose(K_Binds_CT); - - if (mbs = DECAPS_DECAPS) { - (sk0, sk1, c0, c1) <@ A(RO).find_dd(); - - pk0 <- sk2pk sk0; - pk1 <- sk2pk sk1; - - k0o <@ S.decaps(sk0, c0); - k1o <@ S.decaps(sk1, c1); - - kc0 <- (oget k0o, c0); - kc1 <- (oget k1o, c1); - } elif (mbs = ENCAPS_DECAPS) { - (sk0, sk1, r0, c1) <@ A(RO).find_ed(); - - pk0 <- sk2pk sk0; - pk1 <- sk2pk sk1; - - (k0, c0) <@ S.encaps(pk0, r0); - k1o <@ S.decaps(sk1, c1); - - kc0 <- (k0, c0); - kc1 <- (oget k1o, c1); - } else { (* mbs = ENCAPS_ENCAPS *) - (sk0, sk1, r0, r1) <@ A(RO).find_ee(); - - pk0 <- sk2pk sk0; - pk1 <- sk2pk sk1; - - (k0, c0) <@ S.encaps(pk0, r0); - (k1, c1) <@ S.encaps(pk1, r1); - - kc0 <- (k0, c0); - kc1 <- (k1, c1); - } - - return (kc0, kc1); - } -}. - - - -section. - -declare module S <: SchemeDerand{-RO}. - -declare module A <: Adv_MALBIND_ROM{-S, -RO}. - -local lemma test : - equiv[MAL_BIND_ROM(RO, KEM_KDF_PP_Ct(S), A).main ~ CR_ROM(RO, R_KCT_CR(S, A)).main : ={glob S, glob A} /\ arg{1} = K_Binds_CT ==> res{1} => res{2}]. -proof. - -qed. - -end section.