Fixing dependencies on old stuff.

sandbox-quantum · Jan 8, 2025 · b2838c1 · b2838c1
1 parent 401fa2b
commit b2838c1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 17 deletions.
diff --git a/proofs/FO_T.eca b/proofs/FO_T.eca
@@ -41,13 +41,11 @@ clone import PublicKeyEncryptionROM as PKEROM with
   type ctxt_t <- ctxt_t,
 
   type in_t <- ptxt_t,
-  type out_t <- rand_t,
+  type out_t <- rand_t
 
-    op F_RO.dout <- drandm
-
   proof *.  
 
-import PKE F_RO.
+import PKE.
 import DeltaCorrectROM DeltaCorrect.
 
 (*

diff --git a/proofs/PublicKeyEncryptionROM.eca b/proofs/PublicKeyEncryptionROM.eca
@@ -960,19 +960,6 @@ module OW_CPA_O_ROM (RO : RandomOraclei) (S : Scheme_ROM) (O : Oracles_PCi_ROM)
   }
 }.
 
-(** OW-CPA (final check performed with oracle) security game in ROM **)
-module OW_CPA_O_ROM (RO : RandomOraclei, S : Scheme_ROM, O : Oracles_PCi_ROM, A : Adv_OWCPA_ROM) = {
-  proc main() : bool = {
-    var r : bool;
-
-    RO.init();
-
-    r <@ OW_CPA_O(S(RO), O(RO), A(RO)).main();
-
-    return r;    
-  }
-}.
-
 
 (* 
   One-Wayness under Plaintext-Checking Attacks (OW-PCA) in ROM