From f678848ab77980574f4303208381604b552bad61 Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Mon, 30 Oct 2023 19:20:57 +0000 Subject: [PATCH] Counts and lossless to go --- proof/security/FO_TT.ec | 104 ++++------ proof/security/FO_UU.ec | 65 ++---- proof/security/PKE_ROM.ec | 413 +++++++++++++++----------------------- 3 files changed, 216 insertions(+), 366 deletions(-) diff --git a/proof/security/FO_TT.ec b/proof/security/FO_TT.ec index cb1f7f80..b2deba5f 100644 --- a/proof/security/FO_TT.ec +++ b/proof/security/FO_TT.ec @@ -67,8 +67,6 @@ op [lossless] randd : randomness distr. clone import PKE_ROM.PKE as PKE with type plaintext <- plaintext, - type OWvsIND_RO.RO.out_t <- randomness, - op OWvsIND_RO.RO.dout <- fun _ => randd, op dplaintext <- dplaintext, op MFinT.enum <- FinT.enum proof MFinT.enum_spec by apply FinT.enum_spec @@ -807,44 +805,10 @@ module AdvOW_query (A:PCVA_ADV) = { (**** MODULES REQUIRED FOR TIGHT IND-CPA***************) (******************************************************) - -module O_AdvOW_MERGE = { - var pk : pkey - proc pco(m : plaintext, c : ciphertext) : bool = { - var r, c'; - r <@ OWvsIND_RO.RO.RO.get(m); - c' <- enc r pk m; - return c = c'; - } - - proc cvo(c:ciphertext) : bool = { - var rv; - rv <- false; - if (c <> OW_PCVA.cc) - rv <- find (fun m r => c = enc r pk m) OWvsIND_RO.RO.RO.m <> None; - return rv; - } -}. - -module AdvOW_query_MERGE (A:PCVA_ADV) = { - import var OW_PCVA O_AdvOW_MERGE - - module A = A(CountH(OWvsIND_RO.RO.RO), CountO(O_AdvOW_MERGE)) - - proc main(pk0:pkey, c:ciphertext) : unit = { - var m' : plaintext option; - pk <- pk0; - OWvsIND_RO.RO.RO.init(); - cc <- c; - CountO(O_AdvOW_MERGE).init(); - m' <@ A.find(pk,cc); - } - - proc find(pk0:pkey, c:ciphertext) : plaintext option = { - var i : int; - main(pk0, c); - i <$ [0 .. qH + qP - 1]; - return Some (nth witness (elems (fdom OWvsIND_RO.RO.RO.m)) i); +module AdvOWL_query (A:PCVA_ADV) = { + proc find(pk0:pkey, c:ciphertext) : plaintext list = { + AdvOW_query(A).find(pk0,c); + return elems (fdom RO.RO.m); } }. @@ -853,10 +817,8 @@ module AdvOW_query_MERGE (A:PCVA_ADV) = { (******************************************************) section. - -declare module A <: PCVA_ADV { -RO.RO, -OW_PCVA, -RO.RO, -RO.FRO, -OW_CPA, - -CountO, -Gm, -O_AdvOW, -Correctness_Adv1, -B, -BOWp, -OWvsIND.Bow, - - OWvsIND_RO.RO.RO, -AdvOW_query_MERGE, -OWvsIND_RO.RO.RO.m}. +declare module A <: PCVA_ADV { -RO.RO, -OW_PCVA, -RO.RO, -RO.FRO, -OW_CPA, -OWL_CPA, + -CountO, -Gm, -O_AdvOW, -Correctness_Adv1, -B, -BOWp, -OWvsIND.Bowl}. local module PCO(RO:RO.RO) = { import var OW_PCVA @@ -2003,7 +1965,7 @@ local lemma G3_CPA_query &m : Pr[G3.main() @ &m : dec OW_PCVA.sk.`2 OW_PCVA.cc = Some Gm.m /\ Gm.m \in RO.RO.m] <= 2%r * ((qH + qP)%r * eps_msg + - `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r |). + `| Pr[PKE.CPA(BasePKE,OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r |). proof. move => A_count All. case (qH = 0 /\ qP = 0). @@ -2019,23 +1981,39 @@ case (qH = 0 /\ qP = 0). move => *. have : Pr[G3.main() @ &m :Gm.m \in RO.RO.m] <= 2%r * ((qH + qP)%r * eps_msg + - `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r |); last + `| Pr[PKE.CPA(BasePKE,OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r |); last by rewrite Pr[mu_split dec OW_PCVA.sk.`2 OW_PCVA.cc = Some Gm.m]; smt(mu_bounded). - (* PROBLEM INSTANTIATING: THIS PROOF WILL NEED TO BE DONE HERE UNLESS I CAN FIND A SOLUTION - TO THE MODULE RESTRICTIONS. - have := OWvsIND_RO.ow_ind_ro BasePKE (AdvOW_query_MERGE(A)) &m _ _ _ _;1..3:by islossless. - + (* lossless *) *) - have : Pr[OW_CPA(BasePKE, AdvOW_query_MERGE(A)).main() @ &m : OW_CPA.m \in OWvsIND_RO.RO.RO.m] <= - 2%r * ((qH + qP)%r * eps_msg + `|Pr[PKE.CPA(BasePKE, OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r / 2%r|) by admit. (* this goes away if instantiation possible *) - have -> : Pr[OW_CPA(BasePKE, AdvOW_query_MERGE(A)).main() @ &m : OW_CPA.m \in OWvsIND_RO.RO.RO.m] = + have := OWvsIND.ow_ind_l BasePKE (AdvOWL_query(A)) &m (qH + qP) _ _ _ _ _ _;2..4:by islossless. + + by smt(ge0_qH ge0_qP). + + islossless; 1: by apply (All (CountH(RO.RO)) (CountO(O_AdvOW))); islossless. + by smt(drange_ll ge0_qH ge0_qP). + + proc;inline *;rnd;conseq (:_ ==> card (fdom RO.RO.m) <= qH + qP); 1: by smt(). + call(: card (fdom RO.RO.m) = 0 /\ CountO.c_h = 0 /\ CountO.c_cvo = 0 /\ CountO.c_pco = 0 ==> + CountO.c_h <= qH /\ CountO.c_cvo <= qV /\ CountO.c_pco <= qP /\ + (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco)). + conseq (: CountO.c_h =0 /\ CountO.c_pco = 0 /\ + (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco) ==> + + (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco)) + (A_count (<:RO.RO) (<:O_AdvOW)) => />; 1: by smt(). + proc ( + (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco)) => //. + + by proc;inline *;auto. + + by proc;inline *;auto;smt(fdom_set fcardU fcard1 fcard_ge0). + + by proc;inline *;auto;smt(fdom_set fcardU fcard1 fcard_ge0). + by auto => />;smt(fcards0 fdom0). + + have -> : Pr[OWL_CPA(BasePKE, AdvOWL_query(A)).main() @ &m : OWL_CPA.m \in OWL_CPA.l] = Pr[G3.main() @ &m : Gm.m \in RO.RO.m]; last by done. - byequiv (_: _ ==> OWvsIND_RO.RO.RO.m{1} = RO.RO.m{2} /\ OW_CPA.m{1} = Gm.m{2} /\ O_AdvOW_MERGE.pk{1} = O_AdvOW.pk{2}) => //. - proc;inline *;wp;rnd{1};call(_: ={OW_PCVA.cc} /\ OWvsIND_RO.RO.RO.m{1} = RO.RO.m{2} /\ OW_CPA.m{1} = Gm.m{2} /\ O_AdvOW_MERGE.pk{1} = O_AdvOW.pk{2}). + byequiv => //. + proc;inline *;wp;rnd{1}; conseq (:_ ==> OWL_CPA.m{1} = Gm.m{2} /\ ={RO.RO.m}); + 1: by smt(mem_fdom drange_ll ge0_qH ge0_qP). + call(_: ={OW_PCVA.cc, RO.RO.m} /\ OWL_CPA.m{1} = Gm.m{2} /\ O_AdvOW.pk{1} = O_AdvOW.pk{2}). + by sim. + by sim. + by sim. - by auto => />;smt(drange_ll ge0_qH ge0_qP). + by auto => />. qed. lemma pre_conclusion_cpa &m gamma_spread : @@ -2050,9 +2028,9 @@ lemma pre_conclusion_cpa &m gamma_spread : islossless O.cvo => islossless O.pco => islossless H0.get => islossless A(H0, O).find) => Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <= - 2%r * `|Pr[PKE.CPA(BasePKE, OWvsIND.Bow(AdvOW(A))).main() @ &m : res] - 1%r / 2%r| - + 2%r * `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r | - + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query_MERGE(A))).main() @ &m : res ] + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(A)))).main() @ &m : res] - 1%r / 2%r| + + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r | + + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query(A))).main() @ &m : res ] + Pr[ PKE.Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(A))).main() @ &m : res] + Pr[ Correctness_Adv(RO.RO,TT,AdvCorr(A)).main() @ &m : res ] + qV%r * gamma_spread + 2%r * (qH + qP + 1)%r * eps_msg. @@ -2086,9 +2064,9 @@ lemma conclusion_cpa &m gamma_spread : islossless O.cvo => islossless O.pco => islossless H0.get => islossless A(H0, O).find) => Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <= - 2%r * `|Pr[PKE.CPA(BasePKE, OWvsIND.Bow(AdvOW(A))).main() @ &m : res] - 1%r / 2%r| - + 2%r * `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r | - + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query_MERGE(A))).main() @ &m : res ] + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(A)))).main() @ &m : res] - 1%r / 2%r| + + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r | + + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query(A))).main() @ &m : res ] + Pr[ PKE.Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(A))).main() @ &m : res] + (qH + qP + 2)%r * Pr[ PKE.Correctness_Adv(BasePKE,B(AdvCorr(A),RO.RO)).main() @ &m : res ] + qV%r * gamma_spread + 2%r * (qH + qP + 1)%r * eps_msg. @@ -2110,7 +2088,5 @@ proof. by smt(). qed. - - end section. diff --git a/proof/security/FO_UU.ec b/proof/security/FO_UU.ec index 04075461..15f48713 100644 --- a/proof/security/FO_UU.ec +++ b/proof/security/FO_UU.ec @@ -1313,48 +1313,15 @@ qed. (* Instantiation *) -(* lemma correctness: - forall (A0(H0 : PKEROM.POracle) <: - PKEROM.CORR_ADV{+all mem, -PKEROM.RO.RO, -PKEROM.RO.FRO, -Correctness_Adv1, -B} [find : {H0.get} ]) &m, - qHC < FinT.card - 1 => - (forall (RO <: PKEROM.RO.RO{+all mem, -CO1, -A0} ), - hoare[ Correctness_Adv1(RO, A0).A.find : CO1.counter = 0 ==> CO1.counter <= qHC]) => - (forall (H0 <: PKEROM.POracle{+all mem, -A0} ), islossless H0.get => islossless A0(H0).find) => - Pr[PKEROM.Correctness_Adv(PKEROM.RO.RO, TT, A0).main() @ &m : res] <= - (qHC + 1)%r * Pr[Correctness_Adv(BasePKE, B(A0, PKEROM.RO.RO)).main() @ &m : res]. *) - (* -lemma conclusion: - forall (A0(H0 : PKEROM.POracle, O : PKEROM.VA_ORC) <: - PKEROM.PCVA_ADV{+all mem, -PKEROM.RO.RO, -PKEROM.RO.FRO, -PKEROM.OW_PCVA, -Correctness_Adv1, -B, -CountO, -O_AdvOW, -Gm} - [find : {O.cvo, O.pco, H0.get} ]) &m (gamma_spread : real), - qH + qP + 1 = qHC => - qHC < FinT.card - 1 => - gamma_spread_ok gamma_spread => - (forall (RO <: PKEROM.POracle{+all mem, -CountO, -A0} ) (O <: PKEROM.VA_ORC{+all mem, -CountO, -A0} ), - hoare[ A0(CountH(RO), CountO(O)).find : - CountO.c_h = 0 /\ CountO.c_cvo = 0 /\ CountO.c_pco = 0 ==> - CountO.c_h <= qH /\ CountO.c_cvo <= qV /\ CountO.c_pco <= qP]) => - (forall (H0 <: PKEROM.POracle{+all mem, -A0} ) (O <: PKEROM.VA_ORC{+all mem, -A0} ), - islossless O.cvo => islossless O.pco => islossless H0.get => islossless A0(H0, O).find) => - Pr[PKEROM.OW_PCVA(PKEROM.RO.LRO, TT, A0).main() @ &m : res] <= - Pr[OW_CPA(BasePKE, AdvOW(A0)).main() @ &m : res] + - (qH + qP)%r * Pr[OW_CPA(BasePKE, AdvOW_query(A0)).main() @ &m : res] + - (qH + qP + 2)%r * Pr[Correctness_Adv(BasePKE, B(AdvCorr(A0), PKEROM.RO.RO)).main() @ &m : res] + - qV%r * gamma_spread. -*) + Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <= + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(A)))).main() @ &m : res] - 1%r / 2%r| + + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r | + + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query(A))).main() @ &m : res ] + + Pr[ PKE.Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(A))).main() @ &m : res] + + (qH + qP + 2)%r * Pr[ PKE.Correctness_Adv(BasePKE,B(AdvCorr(A),RO.RO)).main() @ &m : res ] + + qV%r * gamma_spread + 2%r * (qH + qP + 1)%r * eps_msg. -(* -lemma ow_ind &m : - islossless S.kg => - islossless S.enc => - islossless S.dec => - islossless A.find => - - Pr[ OW_CPA(S,A).main() @ &m : res ] <= - 2%r * (eps_msg + - `| Pr[CPA(S,Bow(A)).main() @ &m : res] - 1%r/2%r |) + - Pr[ Correctness_Adv(S,BOWp(S,A)).main() @ &m : res ]. *) end section. @@ -1362,10 +1329,10 @@ end section. section. declare module A <: CCA_ADV {-CCA, -RO1.RO, -RO1.FRO, -RO2.RO, -PRF, -RF, -UU2, -OW_CPA, - -RO1E.FunRO, -Gm2, -H2, -Gm3, -PKEROM.OW_PCVA, -H2BOWMod, + -RO1E.FunRO, -Gm2, -H2, -Gm3, -PKEROM.OW_PCVA, -H2BOWMod, -OWL_CPA, -PKEROM.RO.RO, -PKEROM.RO.FRO, -Correctness_Adv1, -B, -PKEROM.OW_PCVA, -Correctness_Adv1, -CountO, -O_AdvOW, -Gm, - -BOWp, -OWvsIND.Bow, -BasePKE, -AdvOW_query_MERGE, -OWvsIND_RO.RO.RO}. + -BOWp, -OWvsIND.Bowl, -BasePKE}. lemma conclusion &m : qH = qHU + 1 => @@ -1386,7 +1353,7 @@ lemma conclusion &m : (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(BUUCI(A), PKEROM.RO.RO)).main() @ &m : res] + (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(AdvCorr(BUUOWMod(A)), PKEROM.RO.RO)).main() @ &m : res] + Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(BUUOWMod(A)))).main() @ &m : res] + - 2%r * `|Pr[CPA(BasePKE, OWvsIND.Bow(AdvOW(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| + + 2%r * `|Pr[CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(BUUOWMod(A))))).main() @ &m : res] - 1%r / 2%r| + (qHU + 1)%r * Pr[OW_CPA(BasePKE, AdvOW_query(BUUOWMod(A))).main() @ &m : res] + 2%r * eps_msg. proof. @@ -1438,15 +1405,15 @@ lemma conclusion_cpa &m : islossless H0.get2 => islossless A(H0, O).guess) => `| Pr[ KEMROMx2.CCA(RO_x2(RO1.RO,RO2.RO), UU, A).main() @ &m : res ] - 1%r/2%r | <= - `|Pr [ J.IND(PRF,D(A)).main() @ &m : res ] - - Pr [ J.IND(RF, D(A)).main() @ &m : res ]| + + 2%r * `|Pr[CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(BUUOWMod(A))))).main() @ &m : res] - 1%r / 2%r| + + 2%r * `|Pr[CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| + (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(BUUC(A), PKEROM.RO.RO)).main() @ &m : res] + (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(BUUCI(A), PKEROM.RO.RO)).main() @ &m : res] + (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(AdvCorr(BUUOWMod(A)), PKEROM.RO.RO)).main() @ &m : res] + Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(BUUOWMod(A)))).main() @ &m : res] + - Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW_query_MERGE(BUUOWMod(A)))).main() @ &m : res] + - 2%r * `|Pr[CPA(BasePKE, OWvsIND.Bow(AdvOW(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| + - 2%r * `|Pr[CPA(BasePKE, OWvsIND_RO.BowROM(AdvOW_query_MERGE(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| + + Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW_query(BUUOWMod(A)))).main() @ &m : res] + + `|Pr [ J.IND(PRF,D(A)).main() @ &m : res ] - + Pr [ J.IND(RF, D(A)).main() @ &m : res ]| + 2%r * (qHU + 2)%r * eps_msg. proof. move => qhval qv0 qp0 qhphc qhcb A_ll. @@ -1478,7 +1445,7 @@ lemma conclusion_cpa &m : have ? : Pr[PKEROM.OW_PCVA(RO1.RO, TT, BUUOWMod(A)).main() @ &m : res] = Pr[PKEROM.OW_PCVA(PKEROM.RO.LRO, TT, BUUOWMod(A)).main() @ &m : res] by byequiv => //;proc;inline *;sim. - +move => *. smt(). qed. diff --git a/proof/security/PKE_ROM.ec b/proof/security/PKE_ROM.ec index 99bd3fb0..6d8e8a02 100644 --- a/proof/security/PKE_ROM.ec +++ b/proof/security/PKE_ROM.ec @@ -173,6 +173,7 @@ module OW_CPA (S:Scheme, A: OW_CPA_ADV) = { } }. + module BOWp(S : Scheme, A : OW_CPA_ADV) : CORR_ADV = { var m'' : plaintext option @@ -238,177 +239,41 @@ qed. end section. -(* Ind implies ow for large message spaces *) - -theory OWvsIND. - -module Bow(A : OW_CPA_ADV) : Adversary = { - var m0, m1 : plaintext - var m : plaintext option - var pk : pkey +(* Ind implies ow for large message spaces. We present a stronger + result for list-returning adversaries and then refine to the + case where only one message is returned. *) - proc choose(_pk : pkey) : plaintext * plaintext = { - pk <- _pk; - m0 <$ dplaintext; - m1 <$ dplaintext; - return (m0,m1); - } - - proc guess(c : ciphertext) : bool = { - var b; - b <$ {0,1}; - m <@ A.find(pk,c); - return if (m = Some m0) - then false - else if (m = Some m1) - then true - else b; - } +module type OWL_CPA_ADV = { + proc find(pk : pkey, c:ciphertext) : plaintext list }. -section. - - -declare module S <: Scheme {-Bow, -BOWp, -OW_CPA}. -declare module A <: OW_CPA_ADV {-S, -Bow, -BOWp, -OW_CPA}. +module OWL_CPA (S:Scheme, A: OWL_CPA_ADV) = { + var pk : pkey + var sk : skey + var m : plaintext + var cc : ciphertext + var l : plaintext list -local module Aux = { - proc main0() : bool = { - var pk,sk,c,b; - (pk, sk) <@ S.kg(); - Bow.pk <- pk; - Bow.m0 <$ dplaintext; - Bow.m1 <$ dplaintext; - c <@ S.enc(pk, Bow.m0); - b <$ {0,1}; - Bow.m <@ A.find(Bow.pk, c); - return if Bow.m = Some Bow.m0 then false else if Bow.m = Some Bow.m1 then true else b; - } + proc main() = { + (pk, sk) <@ S.kg(); + m <$ dplaintext; + cc <@ S.enc(pk, m); + l <@ A.find(pk,cc); + return (m \in l); - proc main1() : bool = { - var pk,sk,c,b; - (pk, sk) <@ S.kg(); - Bow.pk <- pk; - Bow.m0 <$ dplaintext; - Bow.m1 <$ dplaintext; - c <@ S.enc(pk, Bow.m1); - b <$ {0,1}; - Bow.m <@ A.find(Bow.pk, c); - return if Bow.m = Some Bow.m0 then false else if Bow.m = Some Bow.m1 then true else b; } - }. -print glob Bow. -pred bad(gB : glob Bow) = (gB.`1 = None \/ (gB.`1 <> Some gB.`2 /\ gB.`1 <> Some gB.`3)). - -lemma ow_ind &m : - islossless S.kg => - islossless S.enc => - islossless S.dec => - islossless A.find => - - Pr[ OW_CPA(S,A).main() @ &m : res ] <= - 2%r * (eps_msg + - `| Pr[CPA(S,Bow(A)).main() @ &m : res] - 1%r/2%r |) + - Pr[ Correctness_Adv(S,BOWp(S,A)).main() @ &m : res ]. -proof. -move => kg_ll enc_ll dec_ll A_ll. -have : Pr[ OW_CPA(S,A).main_perfect() @ &m : res ] <= - 2%r * (eps_msg + - `| Pr[CPA(S,Bow(A)).main() @ &m : res] - 1%r/2%r |); last - by move : (ow_perfect S A &m A_ll enc_ll dec_ll);smt(). - -rewrite RField.mulrDr -(pr_CPA_LR S (Bow(A)) &m kg_ll enc_ll); 1,2: by islossless. - -have -> : - Pr[CPA_L(S, Bow(A)).main() @ &m : res] = - Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)] + - Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ !bad (glob Bow)] -by rewrite Pr[mu_split bad (glob Bow)] => /#. - -have -> : - Pr[CPA_R(S, Bow(A)).main() @ &m : res] = - Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)] + - Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ !bad (glob Bow)] -by rewrite Pr[mu_split bad (glob Bow)] => /#. -have -> /=: - Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)] = - Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)]. -+ byequiv (: _ ==> (res /\ bad (glob Bow)){1} <=> - (res /\ bad (glob Bow)){2}) => //. - proc. - seq 2 2 : (={glob A, glob S, pk,sk, Bow.pk} /\ Bow.pk{1} = pk{1} /\ - Bow.m0{1} = Bow.m1{2} /\ Bow.m1{1} = Bow.m0{2} /\ - Bow.m0{1} = m0{1} /\ Bow.m1{1} = m1{1} /\ - Bow.m0{2} = m0{2} /\ Bow.m1{2} = m1{2}); - 1: by inline *;swap {1} 4 1;auto;call(_: true); auto. - by inline *;wp;call(_: true);rnd;wp;call(_:true);auto => /> /#. - -have H : - `| Pr[OW_CPA(S, A).main_perfect() @ &m : res] - - Pr[Aux.main1() @ &m : res /\ ! bad (glob Bow)]| <= - Pr[Aux.main1() @ &m : Bow.m = Some Bow.m0 ]. - + have -> : Pr[OW_CPA(S, A).main_perfect() @ &m : res] = - Pr[Aux.main1() @ &m : Bow.m = Some Bow.m1] - by byequiv => //;proc;inline*;wp;call(_: true);rnd{2}; - call(:true);rnd;rnd{2};wp;call(_: true);auto => />. - byequiv : (Bow.m = Some Bow.m0) => //. - proc;inline *. - by call(:true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /> /#. - -have H0 : - Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ ! bad (glob Bow)] <= eps_msg. -+ have -> : Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ ! bad (glob Bow)] = - Pr[Aux.main0() @ &m : res /\ ! bad (glob Bow)] - by byequiv => //;proc;inline *;wp;conseq />; sim. - byphoare => //. - proc;inline *; swap 4 3. - conseq (: _ ==> Some Bow.m1 = Bow.m); 1: by smt(). - seq 6 : true (1%r) (eps_msg) (0%r) (0%r). - + by trivial. - + by trivial. - + rnd; skip => /> &hr. - case(Bow.m{hr} = None); 1: by move => -> /=; rewrite mu0;smt(MFinT.card_gt0). - move => nnone. - have -> : (fun (x : plaintext) => Some x = Bow.m{hr}) = pred1 (oget Bow.m{hr}) - by apply fun_ext => x;smt(). - by smt(eps_msgE fun_ext). - + by hoare; trivial. - by trivial. - -have H1 : Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ ! bad (glob Bow)] = - Pr[Aux.main1() @ &m : res /\ ! bad (glob Bow)] - by byequiv => //;proc;inline*;wp;conseq />;sim. - -have : Pr[Aux.main1() @ &m : Bow.m = Some Bow.m0] <= eps_msg; last by smt(). -byphoare => //. -proc;inline *;swap 3 4. -conseq (: _ ==> Bow.m0 = oget Bow.m); 1: by smt(). -seq 6 : true (1%r) (eps_msg) (0%r) (0%r). -+ by trivial. -+ by islossless. -+ rnd; skip => />*; rewrite eps_msgE /#. -+ by hoare; trivial. -by trivial. -qed. - -end section. - -end OWvsIND. - -(* Ind tightly implies even list OW for large message spaces *) - -theory OWvsIND_RO. +theory OWvsIND. -clone import FullRO as RO with - type in_t <- plaintext - proof *. +(***) +(***) -module BowROM(A : OW_CPA_ADV) : Adversary = { +module Bowl(A : OWL_CPA_ADV) : Adversary = { var m0, m1 : plaintext var pk : pkey + var l : plaintext list proc choose(_pk : pkey) : plaintext * plaintext = { pk <- _pk; @@ -420,10 +285,10 @@ module BowROM(A : OW_CPA_ADV) : Adversary = { proc guess(c : ciphertext) : bool = { var b; b <$ {0,1}; - A.find(pk,c); - return if (m0 \in RO.m = m1 \in RO.m) + l <@ A.find(pk,c); + return if (m0 \in l = m1 \in l) then b - else if (m0 \in RO.m) + else if (m0 \in l) then false else true; } @@ -432,22 +297,22 @@ module BowROM(A : OW_CPA_ADV) : Adversary = { section. -declare module S <: Scheme {-BowROM, -BOWp, -OW_CPA}. -declare module A <: OW_CPA_ADV {-S, -BOWp, -OW_CPA, -BowROM}. +declare module S <: Scheme {-Bowl, -BOWp, -OWL_CPA}. +declare module A <: OWL_CPA_ADV {-S, -BOWp, -OWL_CPA, -Bowl}. local module Aux = { proc main0() : bool = { var pk,sk,c,b; (pk, sk) <@ S.kg(); - BowROM.pk <- pk; - BowROM.m0 <$ dplaintext; - BowROM.m1 <$ dplaintext; - c <@ S.enc(pk, BowROM.m0); + Bowl.pk <- pk; + Bowl.m0 <$ dplaintext; + Bowl.m1 <$ dplaintext; + c <@ S.enc(pk, Bowl.m0); b <$ {0,1}; - A.find(pk,c); - return if (BowROM.m0 \in RO.m = BowROM.m1 \in RO.m) + Bowl.l <@ A.find(pk,c); + return if (Bowl.m0 \in Bowl.l = Bowl.m1 \in Bowl.l) then b - else if (BowROM.m0 \in RO.m) + else if (Bowl.m0 \in Bowl.l) then false else true; } @@ -455,124 +320,130 @@ local module Aux = { proc main1() : bool = { var pk,sk,c,b; (pk, sk) <@ S.kg(); - BowROM.pk <- pk; - BowROM.m0 <$ dplaintext; - BowROM.m1 <$ dplaintext; - c <@ S.enc(pk, BowROM.m1); + Bowl.pk <- pk; + Bowl.m0 <$ dplaintext; + Bowl.m1 <$ dplaintext; + c <@ S.enc(pk, Bowl.m1); b <$ {0,1}; - A.find(pk,c); - return if (BowROM.m0 \in RO.m = BowROM.m1 \in RO.m) + Bowl.l <@ A.find(pk,c); + return if (Bowl.m0 \in Bowl.l = Bowl.m1 \in Bowl.l) then b - else if (BowROM.m0 \in RO.m) + else if (Bowl.m0 \in Bowl.l) then false else true; } }. -print glob BowROM. -pred bad(gB : glob BowROM) = (gB.`1 \in gB.`4 = gB.`2 \in gB.`4). -lemma ow_ind_ro &m MAX : +lemma boundl l MAX : + 0 <= MAX => + mu dplaintext (fun (x : plaintext) => size l <= MAX /\ x \in l) <= MAX%r * eps_msg. +proof. +case (!size l <= MAX) => *. ++ by have -> : (fun (x : plaintext) => size l <= MAX /\ (x \in l)) = pred0; + rewrite ?mu0 /=;smt(MFinT.card_gt0). +have := Mu_mem.mu_mem_le_size l dplaintext eps_msg _. ++ move => *; rewrite mu1_uni; 1: by smt(dplaintext_uni). + rewrite dplaintext_fu /= dplaintext_ll /eps_msg MFinT.card_size_to_seq. + by have -> : (support dplaintext) = predT; smt(dplaintext_fu is_fullP). +by have : (fun (x : plaintext) => size l <= MAX /\ (x \in l)) = + (mem l); smt(MFinT.card_gt0). +qed. + +print glob Bowl. +pred bad(gB : glob Bowl) = (gB.`2 \in gB.`1 = gB.`3 \in gB.`1). +lemma ow_ind_l &m MAX : 0 <= MAX => islossless S.kg => islossless S.enc => islossless S.dec => islossless A.find => - hoare [ A.find : true ==> card (fdom RO.m) <= MAX ] => + hoare [ A.find : true ==> size res <= MAX ] => - Pr[ OW_CPA(S,A).main() @ &m : OW_CPA.m \in RO.m] <= + Pr[ OWL_CPA(S,A).main() @ &m : OWL_CPA.m \in OWL_CPA.l] <= 2%r * (MAX%r * eps_msg + - `| Pr[CPA(S,BowROM(A)).main() @ &m : res] - 1%r/2%r |). + `| Pr[CPA(S,Bowl(A)).main() @ &m : res] - 1%r/2%r |). proof. move => max_ge0 kg_ll enc_ll dec_ll A_ll maxsize. -rewrite RField.mulrDr -(pr_CPA_LR S (BowROM(A)) &m kg_ll enc_ll); 1,2: by islossless. +rewrite RField.mulrDr -(pr_CPA_LR S (Bowl(A)) &m kg_ll enc_ll); 1,2: by islossless. have -> : - Pr[CPA_L(S, BowROM(A)).main() @ &m : res] = - Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)] + - Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ !bad (glob BowROM)] -by rewrite Pr[mu_split bad (glob BowROM)] => /#. + Pr[CPA_L(S, Bowl(A)).main() @ &m : res] = + Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)] + + Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ !bad (glob Bowl)] +by rewrite Pr[mu_split bad (glob Bowl)] => /#. have -> : - Pr[CPA_R(S, BowROM(A)).main() @ &m : res] = - Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)] + - Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ !bad (glob BowROM)] -by rewrite Pr[mu_split bad (glob BowROM)] => /#. + Pr[CPA_R(S, Bowl(A)).main() @ &m : res] = + Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)] + + Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ !bad (glob Bowl)] +by rewrite Pr[mu_split bad (glob Bowl)] => /#. have -> /=: - Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)] = - Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)]. -+ byequiv (: ={glob A,glob S, RO.m} ==> (res /\ bad (glob BowROM)){1} <=> - (res /\ bad (glob BowROM)){2}) => //. + Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)] = + Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)]. ++ byequiv (: ={glob A,glob S, Bowl.l} ==> (res /\ bad (glob Bowl)){1} <=> + (res /\ bad (glob Bowl)){2}) => //. proc. - seq 2 2 : (={glob A, glob S, pk,sk, BowROM.pk,RO.m} /\ - BowROM.m0{1} = BowROM.m1{2} /\ BowROM.m1{1} = BowROM.m0{2} /\ - BowROM.pk{1} = pk{1} /\ - BowROM.m0{1} = m0{1} /\ BowROM.m1{1} = m1{1} /\ - BowROM.m0{2} = m0{2} /\ BowROM.m1{2} = m1{2}); + seq 2 2 : (={glob A, glob S, pk,sk, Bowl.pk,Bowl.l} /\ + Bowl.m0{1} = Bowl.m1{2} /\ Bowl.m1{1} = Bowl.m0{2} /\ + Bowl.pk{1} = pk{1} /\ + Bowl.m0{1} = m0{1} /\ Bowl.m1{1} = m1{1} /\ + Bowl.m0{2} = m0{2} /\ Bowl.m1{2} = m1{2}); 1: by inline *; swap {1} 4 1;auto;call(_: true); auto. by inline *;wp;call(_: true);rnd;wp;call(_:true);auto => /> /#. -have H : `| Pr[OW_CPA(S, A).main() @ &m : OW_CPA.m \in RO.m ] - - Pr[Aux.main1() @ &m : res /\ ! bad (glob BowROM) ]| <= - Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m]. -+ have -> : Pr[OW_CPA(S, A).main() @ &m : OW_CPA.m \in RO.m] = - Pr[Aux.main1() @ &m : BowROM.m1 \in RO.m]. - + byequiv (: ={glob A,glob S, RO.m} ==> _) => //. - proc;inline*;wp;call{1}(_: true ==> true). - by wp;call(:true); rnd{2};call(:true);rnd;rnd{2};wp;call(_: true);auto. - byequiv : (BowROM.m0 \in RO.m) => //. +have H : `| Pr[OWL_CPA(S, A).main() @ &m : OWL_CPA.m \in OWL_CPA.l ] - + Pr[Aux.main1() @ &m : res /\ ! bad (glob Bowl) ]| <= + Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l]. ++ have -> : Pr[OWL_CPA(S, A).main() @ &m : OWL_CPA.m \in OWL_CPA.l] = + Pr[Aux.main1() @ &m : Bowl.m1 \in Bowl.l]. + + byequiv => //. + proc;inline*;wp. + by wp;call(:true); rnd{2};call(:true);rnd;rnd{2};wp;call(_: true);auto => />. + byequiv : (Bowl.m0 \in Bowl.l) => //. proc;inline *. by call(:true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /> /#. have H0 : - Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ ! bad (glob BowROM)] <= MAX%r * eps_msg. -+ have -> : Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ ! bad (glob BowROM)] = - Pr[Aux.main0() @ &m : res /\ !bad (glob BowROM)]. - + byequiv (:_ ==> ={res} /\ ((!bad (glob BowROM)){1} <=>(!bad (glob BowROM)){2})) => //; last by smt(). - by proc;inline *;wp;conseq (_: _ ==> ={BowROM.m1, BowROM.m0, RO.m,b});[ by smt() | by sim ]. - have -> : Pr[Aux.main0() @ &m : res /\ ! bad (glob BowROM)] = - Pr[Aux.main0() @ &m : res /\ card (fdom RO.m) <= MAX /\ ! bad (glob BowROM)]. - + have ?: `| Pr[Aux.main0() @ &m : res /\ !bad (glob BowROM)] - - Pr[Aux.main0() @ &m : res /\ card (fdom RO.m) <= MAX /\ !bad (glob BowROM)] | <= 0%r; last by smt(). - + have ->: 0%r = Pr[Aux.main0() @ &m : ! card (fdom RO.m) <= MAX] + Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ ! bad (glob Bowl)] <= MAX%r * eps_msg. ++ have -> : Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ ! bad (glob Bowl)] = + Pr[Aux.main0() @ &m : res /\ !bad (glob Bowl)]. + + byequiv (:_ ==> ={res} /\ ((!bad (glob Bowl)){1} <=>(!bad (glob Bowl)){2})) => //; last by smt(). + by proc;inline *;wp;conseq (_: _ ==> ={Bowl.m1, Bowl.m0, Bowl.l,b});[ by smt() | by sim ]. + have -> : Pr[Aux.main0() @ &m : res /\ ! bad (glob Bowl)] = + Pr[Aux.main0() @ &m : res /\ size Bowl.l <= MAX /\ ! bad (glob Bowl)]. + + have ?: `| Pr[Aux.main0() @ &m : res /\ !bad (glob Bowl)] - + Pr[Aux.main0() @ &m : res /\ size Bowl.l <= MAX /\ !bad (glob Bowl)] | <= 0%r; last by smt(). + + have ->: 0%r = Pr[Aux.main0() @ &m : ! size Bowl.l <= MAX] by byphoare => //;hoare => /=;proc;inline *;call maxsize;auto => />. - byequiv : (!card (fdom RO.m) <= MAX) =>//. + byequiv : (!size Bowl.l <= MAX) =>//. by proc;call(_: true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /> /#. byphoare => //. proc;inline *; swap 4 3. - conseq (: _ ==> card (fdom RO.m) <= MAX /\ BowROM.m1 \in RO.m); 1: by smt(). + conseq (: _ ==> size Bowl.l <= MAX /\ Bowl.m1 \in Bowl.l); 1: by smt(). seq 6 : true (1%r) (MAX%r * eps_msg) (0%r) (0%r). + by trivial. + by trivial. - + rnd; skip => /> &hr. - case (!card (fdom RO.m{hr}) <= MAX) => *. - + by have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = pred0; - rewrite ?mu0 /=;smt(MFinT.card_gt0). - have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = (mem (fdom RO.m{hr})) - by smt(mem_fdom). - have := Mu_mem.mu_mem_le (fdom RO.m{hr}) dplaintext eps_msg _; last by smt(MFinT.card_gt0). - move => *; rewrite mu1_uni; 1: by smt(dplaintext_uni). - rewrite dplaintext_fu /= dplaintext_ll /eps_msg MFinT.card_size_to_seq. - by have -> : (support dplaintext) = predT; smt(dplaintext_fu is_fullP). + + by rnd; auto => /> *;apply boundl =>/#. + by hoare; trivial. by trivial. -have -> : Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ !bad (glob BowROM)] = - Pr[Aux.main1() @ &m : res /\ !bad (glob BowROM)]. -+ byequiv (: ={glob A,glob S, RO.m} ==> _) => //. +have -> : Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ !bad (glob Bowl)] = + Pr[Aux.main1() @ &m : res /\ !bad (glob Bowl)]. ++ byequiv => //. by proc;inline*;wp;call(:true);rnd;wp;call(:true);wp;rnd;rnd;wp;call(:true);auto. -have : Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m] <= MAX%r * eps_msg; last by smt(). -have -> : Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m] = - Pr[Aux.main1() @ &m : card (fdom RO.m) <= MAX /\ BowROM.m0 \in RO.m]. -+ have : `| Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m] - - Pr[Aux.main1() @ &m : card (fdom RO.m) <= MAX /\ BowROM.m0 \in RO.m]| <= 0%r; last by smt(). - + have ->: 0%r = Pr[Aux.main1() @ &m : ! card (fdom RO.m) <= MAX] +have : Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l] <= MAX%r * eps_msg; last by smt(). +have -> : Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l] = + Pr[Aux.main1() @ &m : size Bowl.l <= MAX /\ Bowl.m0 \in Bowl.l]. ++ have : `| Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l] - + Pr[Aux.main1() @ &m : size Bowl.l <= MAX /\ Bowl.m0 \in Bowl.l]| <= 0%r; last by smt(). + + have ->: 0%r = Pr[Aux.main1() @ &m : ! size Bowl.l <= MAX] by byphoare => //;hoare => /=;proc;inline *;call maxsize;auto => />. - byequiv : (!card (fdom RO.m) <= MAX) =>//. + byequiv : (!size Bowl.l <= MAX) =>//. by proc;call(_: true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /#. byphoare => //. @@ -580,23 +451,59 @@ proc;inline *; swap 3 4. seq 6 : true (1%r) (MAX%r * eps_msg) (0%r) (0%r). + by trivial. + by trivial. -+ rnd; skip => /> &hr. - case (!card (fdom RO.m{hr}) <= MAX) => *. - + by have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = pred0; - rewrite ?mu0 /=;smt(MFinT.card_gt0). - have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = (mem (fdom RO.m{hr})) - by smt(mem_fdom). - have := Mu_mem.mu_mem_le (fdom RO.m{hr}) dplaintext eps_msg _; last by smt(MFinT.card_gt0). - move => *; rewrite mu1_uni; 1: by smt(dplaintext_uni). - rewrite dplaintext_fu /= dplaintext_ll /eps_msg MFinT.card_size_to_seq. - by have -> : (support dplaintext) = predT; smt(dplaintext_fu is_fullP). ++ by rnd; auto => /> *;apply boundl =>/#. + by hoare; trivial. by trivial. qed. end section. -end OWvsIND_RO. +section. + +declare module S <: Scheme {-Bowl, -BOWp, -OW_CPA, -OWL_CPA}. +declare module A <: OW_CPA_ADV {-S, -Bowl, -BOWp, -OW_CPA, -OWL_CPA}. + +module BL(A : OW_CPA_ADV) : OWL_CPA_ADV = { + proc find(pk : pkey, c : ciphertext) : plaintext list = { + var m'; + m' <@ A.find(pk,c); + return if m' = None then [] else [oget m']; + } +}. + +lemma ow_ind &m : + islossless S.kg => + islossless S.enc => + islossless S.dec => + islossless A.find => + + Pr[ OW_CPA(S,A).main() @ &m : res ] <= + 2%r * (eps_msg + + `| Pr[CPA(S,Bowl(BL(A))).main() @ &m : res] - 1%r/2%r |) + + Pr[ Correctness_Adv(S,BOWp(S,A)).main() @ &m : res ]. +proof. +move => kg_ll enc_ll dec_ll A_ll. +have : Pr[ OW_CPA(S,A).main_perfect() @ &m : res ] <= + 2%r * (eps_msg + + `| Pr[CPA(S,Bowl(BL(A))).main() @ &m : res] - 1%r/2%r |); last + by move : (ow_perfect S A &m A_ll enc_ll dec_ll);smt(). + +rewrite RField.mulrDr. + +have /= := ow_ind_l S (BL(A)) &m 1 _ kg_ll enc_ll dec_ll _ _ => //; 1: by islossless. ++ by proc;wp;call(_:true);auto;smt(). + +have -> : Pr[OWL_CPA(S, BL(A)).main() @ &m : OWL_CPA.m \in OWL_CPA.l] = + Pr[OW_CPA(S, A).main_perfect() @ &m : res]; last by smt(). + +byequiv => //; proc;inline {1} 4; wp. +conseq (: _ ==> OWL_CPA.m{1} = OW_CPA.m{2} /\ m'{1} = OW_CPA.m'{2}); 1: by auto => /> /#. +by sim. +qed. + +end section. + +end OWvsIND. end PKE.