saving work

formosa-crypto · Oct 29, 2023 · 55f200a · 55f200a
1 parent 283ebf3
commit 55f200a
Show file tree

Hide file tree

Showing 3 changed files with 470 additions and 44 deletions.
diff --git a/proof/security/FO_TT.ec b/proof/security/FO_TT.ec
@@ -62,8 +62,13 @@ op [full lossless uniform]dplaintext : plaintext distr.
 clone import FinType as FinT with 
    type t <- plaintext.
 
+type randomness.
+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
@@ -74,13 +79,9 @@ clone import PKE_ROM.PKE as PKE with
 
 op [lossless] kg : (pkey * skey) distr.
 
-type randomness.
-
 op enc : randomness -> pkey -> plaintext -> ciphertext.
 op dec : skey -> ciphertext -> plaintext option.
 
-op [lossless] randd : randomness distr.
-
 module BasePKE : PKE.Scheme = {
   proc kg() : pkey * skey = {
      var kpair;
@@ -802,10 +803,60 @@ 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);
+  }
+}.
+
+(******************************************************)
+(**** END MODULES REQUIRED FOR TIGHT IND-CPA************)
+(******************************************************)
+
 section. 
 
-declare module A <: PCVA_ADV { -OW_PCVA, -RO.RO, -RO.FRO, 
-               -CountO, -Gm, -O_AdvOW, -Correctness_Adv1, -B}.
+declare module A <: PCVA_ADV { -RO.RO, -OW_PCVA, -RO.RO, -RO.FRO, -OW_CPA,
+               -CountO, -Gm, -O_AdvOW, -Correctness_Adv1, -B, -BOWp, 
+               - OWvsIND_RO.RO.RO, -AdvOW_query_MERGE}.
 
 local module PCO(RO:RO.RO) = {
   import var OW_PCVA
@@ -1937,5 +1988,108 @@ lemma conclusion &m :
     + (qV + qP)%r * gamma_spread.
 *)
 
+(********** TIGHT REDUCTION TO IND-CPA ***************)
+
+
+local lemma G3_CPA_query &m : 
+
+ (forall (RO<:POracle{ -CountO, -A })(O<:VA_ORC { -CountO, -A }), 
+  hoare [A(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 <: POracle { -A }) (O <: VA_ORC { -A }),
+  islossless O.cvo => islossless O.pco => islossless H0.get => islossless A(H0, O).find) =>
+
+  Pr[G3.main() @ &m : dec OW_PCVA.sk.`2 OW_PCVA.cc = Some Gm.m /\ Gm.m \in RO.RO.m] <=
+     2%r * (eps_msg + 
+        `| 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 ].
+proof.
+move => A_count All.
+case(qH = 0). admit.
+move => *.
+  have : Pr[G3.main() @ &m :Gm.m \in RO.RO.m] <=
+     2%r * (eps_msg + 
+        `| 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 ]; last
+      by rewrite Pr[mu_split dec OW_PCVA.sk.`2 OW_PCVA.cc = Some Gm.m]; smt(mu_bounded).
+  have := OWvsIND_RO.ow_ind_ro BasePKE (AdvOW_query_MERGE(A)) &m _ _ _ _;1..3:by islossless.
+  + admit. (* lossless *)
+  have  -> : Pr[OW_CPA(BasePKE, AdvOW_query_MERGE(A)).main() @ &m : OW_CPA.m \in OWvsIND_RO.RO.RO.m] =
+             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}).
+  + by sim.
+  + by sim.
+  + by sim.
+  by auto => />;smt(drange_ll ge0_qH ge0_qP).
+qed.
+
+lemma pre_conclusion_cpa &m gamma_spread :
+ gamma_spread_ok gamma_spread =>
+
+ (forall (RO<:POracle{ -CountO, -A })(O<:VA_ORC { -CountO, -A }), 
+  hoare [A(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 <: POracle { -A }) (O <: VA_ORC { -A }),
+  islossless O.cvo => islossless O.pco => islossless H0.get => islossless A(H0, O).find) =>
+
+  Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <=
+      Pr[OW_CPA(BasePKE, AdvOW(A)).main() @ &m : res]
+    + 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 ]
+    + Pr[ Correctness_Adv(RO.RO,TT,AdvCorr(A)).main() @ &m : res ]
+    + qV%r * gamma_spread + 2%r * eps_msg.
+proof.
+  move => gs_ok A_count A_ll.
+  by move: (OW_PCVA_gamma &m gamma_spread gs_ok A_count A_ll) (G1_G2 &m A_ll) (G2_correctness &m) (G2_G3 &m  A_ll)
+     (G3_OW_CPA &m) (G3_CPA_query &m  A_count A_ll)  => /#.
+qed.
+
+lemma conclusion_cpa &m gamma_spread :
+ qH + qP + 1 = qHC =>
+
+ qHC < FinT.card -1 =>
+
+ gamma_spread_ok gamma_spread =>
+
+ (forall (RO<:POracle{ -CountO, -A })(O<:VA_ORC {-CountO, -A}), 
+  hoare [A(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 <: POracle { -A }) (O <: VA_ORC { -A }),
+  islossless O.cvo => islossless O.pco => islossless H0.get => islossless A(H0, O).find) =>
+
+  Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <=
+      Pr[OW_CPA(BasePKE, AdvOW(A)).main() @ &m : res]
+    + 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 ]
+    + (qH + qP + 2)%r * Pr[ PKE.Correctness_Adv(BasePKE,B(AdvCorr(A),RO.RO)).main() @ &m : res ]
+    + qV%r * gamma_spread + 2%r * eps_msg.
+proof.
+  move => counts qhc_small gs_ok A_count A_ll.
+  move: (pre_conclusion_cpa &m gamma_spread gs_ok A_count A_ll).
+  move: (correctness (AdvCorr(A)) &m qhc_small _ _). 
+  + move => RO; proc;wp.
+    call (corr_red_count RO).
+    inline *;wp;conseq />.
+    seq 6 : #pre; 1: by auto.
+    if;if. 
+    + wp;call(_:true);auto => /#.
+    + wp;call(_:true);auto => /#.
+    + wp;call(_:true);auto => /#.
+    auto => /#.
+  move => H0 H0_ll;proc;inline *;wp.
+  by call(_: true); islossless. 
+  by smt().
+qed.
+
+
+
 end section.
 
diff --git a/proof/security/FO_UU.ec b/proof/security/FO_UU.ec
@@ -1361,11 +1361,11 @@ end section.
 
 section.
 
-declare module A <: CCA_ADV  {-CCA, -RO1.RO, -RO1.FRO, -RO2.RO, -PRF, -RF, -UU2, 
+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, 
                      -PKEROM.RO.RO, -PKEROM.RO.FRO, -Correctness_Adv1, -B,
                      -PKEROM.OW_PCVA, -Correctness_Adv1, -CountO, -O_AdvOW, -Gm, 
-                     -BOWp, -Bow, -BasePKE} .
+                     -BOWp, -OWvsIND.Bow, -BasePKE, -AdvOW_query_MERGE, -OWvsIND_RO.RO.RO}.
 
 lemma conclusion &m : 
   qH = qHU + 1 =>
@@ -1386,7 +1386,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, Bow(AdvOW(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| +
+              2%r * `|Pr[CPA(BasePKE, OWvsIND.Bow(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.
@@ -1397,12 +1397,12 @@ lemma conclusion &m :
   + admit. (*lossless*)
   have corruu2 := Top.TT.correctness (BUUCI(A)) &m qhcb _ _. 
   + admit. (*count*)
-  + admit. (*lossless*)
+  + admit. (*lossless*) print Top.TT.conclusion.
   have owcca := Top.TT.conclusion (BUUOWMod(A)) &m 1%r _ qhcb _ _ _;1: smt().
   + admit. (*gamma trivial*) 
   + admit. (*count*)
   + admit. (*lossless*)
-  have ow2ind := ow_ind BasePKE(AdvOW(BUUOWMod(A))) &m _ _ _ _; 1..3: by islossless.
+  have ow2ind := OWvsIND.ow_ind BasePKE(AdvOW(BUUOWMod(A))) &m _ _ _ _; 1..3: by islossless.
   + admit. (*lossless*)
 
   rewrite qv0 /= in owcca. 
@@ -1419,9 +1419,65 @@ lemma conclusion &m :
            Pr[PKEROM.OW_PCVA(PKEROM.RO.LRO, TT, BUUOWMod(A)).main() @ &m : res]
     by byequiv => //;proc;inline *;sim.
 
+   smt().
+qed.
+
+lemma conclusion_cpa &m : 
+  qH = qHU + 1 =>
+  qV = 0 =>
+  qP = 0 =>
+  qH + 1 = qHC =>
+  qHC < FinT.card - 1 =>
+
+  (forall (H0 <: POracle_x2{-A} ) (O <: CCA_ORC{ -A} ),
+  islossless O.dec => 
+  islossless H0.get1 => 
+  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 ]|  + 
+           (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| +
+                   4%r * eps_msg. 
+  proof.
+  move => qhval qv0 qp0 qhphc qhcb A_ll.
+  have concuu:= conclusion_cca_pre A &m A_ll.
+  have corruu1 := Top.TT.correctness (BUUC(A)) &m qhcb _ _. 
+  + admit. (*count*)
+  + admit. (*lossless*)
+  have corruu2 := Top.TT.correctness (BUUCI(A)) &m qhcb _ _. 
+  + admit. (*count*)
+  + admit. (*lossless*) print Top.TT.conclusion.
+  have owcca := Top.TT.conclusion_cpa (BUUOWMod(A)) &m 1%r _ qhcb _ _ _;1: smt().
+  + admit. (*gamma trivial*) 
+  + admit. (*count*)
+  + admit. (*lossless*) print conclusion.
+  have ow2ind := OWvsIND.ow_ind BasePKE(AdvOW(BUUOWMod(A))) &m _ _ _ _; 1..3: by islossless.
+  + admit. (*lossless*)
+
+  rewrite qv0 /= in owcca. 
+
+  have ? : Pr[PKEROM.Correctness_Adv(RO1.RO, TT, BUUC(A)).main() @ &m : res] =
+            Pr[PKEROM.Correctness_Adv(PKEROM.RO.RO, TT, BUUC(A)).main() @ &m : res] 
+    by byequiv => //;proc;inline *;sim.
+
+  have ? : Pr[PKEROM.Correctness_Adv(RO1.RO, TT, BUUCI(A)).main() @ &m : res] =
+            Pr[PKEROM.Correctness_Adv(PKEROM.RO.RO, TT, BUUCI(A)).main() @ &m : res] 
+    by byequiv => //;proc;inline *;sim.
+
+  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.
 
    smt().
 qed.
 
+
 end section.