orginization

dtumad · Feb 24, 2024 · 5c71a50 · 5c71a50
1 parent c110435
commit 5c71a50
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 35 deletions.
diff --git a/src/crypto_constructions/hhs_asymm_enc.lean b/src/crypto_constructions/hhs_asymm_enc.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Devon Tuma
 -/
-import crypto_foundations.primitives.asymm_encryption.asymm_enc_scheme
+import crypto_foundations.primitives.asymm_enc
 import crypto_foundations.hardness_assumptions.hard_homogeneous_space
 
 /-!

diff --git a/...tives/asymm_encryption/asymm_enc_alg.lean → ...pto_foundations/primitives/asymm_enc.lean b/...tives/asymm_encryption/asymm_enc_alg.lean → ...pto_foundations/primitives/asymm_enc.lean
@@ -169,7 +169,18 @@ end ind_cpa
 
 end asymm_enc_alg
 
+def asymm_enc_scheme (spec : ℕ → oracle_spec) (M PK SK C : ℕ → Type) :=
+Π (sp : ℕ), asymm_enc_alg (spec sp) (M sp) (PK sp) (SK sp) (C sp)
+
 namespace asymm_enc_scheme
 
+open asymm_enc_alg
+
+variables {spec : ℕ → oracle_spec} {M PK SK C : ℕ → Type}
+  [∀ sp, coin_spec ⊂ₒ spec sp]
+
+def ind_cpa_secure (enc_scheme : asymm_enc_scheme spec M PK SK C) : Prop :=
+∀ (adv : Π (sp : ℕ), (enc_scheme sp).ind_cpa_adv),
+  negligable (λ sp, (ind_cpa_exp (adv sp)).advantage)
 
-end asymm_enc_scheme
+end asymm_enc_scheme
diff --git a/src/crypto_foundations/primitives/asymm_encryption/asymm_enc_scheme.lean b/src/crypto_foundations/primitives/asymm_encryption/asymm_enc_scheme.lean