Asymmetric Encryption Schemes

Core definitions for asymmetric encryption schemes and correctness.

structure AsymmEncAlg (m : Type → Type u) [Monad m] (M PK SK C : Type) : Type u

An AsymmEncAlg with message space M, key spaces PK and SK, and ciphertexts in C. m is the monad used to execute key generation, encryption, and decryption. The scheme data stays purely algorithmic; probabilistic semantics and public-randomness injection are supplied separately when defining security experiments.

• keygen : m (PK × SK)
• encrypt (pk : PK) (msg : M) : m C
• decrypt (sk : SK) (c : C) : m (Option M)

theorem AsymmEncAlg.ext_iff {m : Type → Type u} {inst✝ : Monad m} {M PK SK C : Type} {x y : AsymmEncAlg m M PK SK C} : x = y ↔ x.keygen = y.keygen ∧ x.encrypt = y.encrypt ∧ x.decrypt = y.decrypt

theorem AsymmEncAlg.ext {m : Type → Type u} {inst✝ : Monad m} {M PK SK C : Type} {x y : AsymmEncAlg m M PK SK C} (keygen : x.keygen = y.keygen) (encrypt : x.encrypt = y.encrypt) (decrypt : x.decrypt = y.decrypt) : x = y

structure AsymmEncAlg.ExplicitCoins (m : Type → Type u) [Monad m] (M PK SK R C : Type) : Type u

An explicit-coins asymmetric encryption scheme in the monad m.

Key generation runs in m, while encryption and decryption become pure once the randomness type R is supplied explicitly. This is the natural refinement used by FO-style transforms, where the coins are sampled externally or derived from an oracle.

• keygen : m (PK × SK)
• encrypt (pk : PK) (msg : M) (coins : R) : C
• decrypt (sk : SK) (c : C) : Option M

@[reducible, inline]

abbrev PKE_Alg (m : Type → Type u_1) [Monad m] (M PK SK C : Type) : Type u_1

def AsymmEncAlg.map {m : Type → Type v} [Monad m] {M PK SK C : Type} (encAlg : AsymmEncAlg m M PK SK C) {n : Type → Type w} [Monad n] (F : m →ᵐ n) : AsymmEncAlg n M PK SK C

Transport an asymmetric encryption scheme across a monad morphism by mapping each algorithmic component.

@[simp]

theorem AsymmEncAlg.map_keygen {m : Type → Type v} [Monad m] {M PK SK C : Type} {n : Type → Type w} [Monad n] {encAlg : AsymmEncAlg m M PK SK C} (F : m →ᵐ n) : (encAlg.map F).keygen = (fun {α : Type} (x : m α) => F.toFun α x) encAlg.keygen

@[simp]

theorem AsymmEncAlg.map_encrypt {m : Type → Type v} [Monad m] {M PK SK C : Type} {n : Type → Type w} [Monad n] {encAlg : AsymmEncAlg m M PK SK C} (F : m →ᵐ n) (pk : PK) (msg : M) : (encAlg.map F).encrypt pk msg = (fun {α : Type} (x : m α) => F.toFun α x) (encAlg.encrypt pk msg)

@[simp]

theorem AsymmEncAlg.map_decrypt {m : Type → Type v} [Monad m] {M PK SK C : Type} {n : Type → Type w} [Monad n] {encAlg : AsymmEncAlg m M PK SK C} (F : m →ᵐ n) (sk : SK) (c : C) : (encAlg.map F).decrypt sk c = (fun {α : Type} (x : m α) => F.toFun α x) (encAlg.decrypt sk c)

def AsymmEncAlg.CorrectExp {m : Type → Type v} [Monad m] {M PK SK C : Type} (encAlg : AsymmEncAlg m M PK SK C) [DecidableEq M] (msg : M) : m Bool

Correctness experiment: returns true iff decrypting the ciphertext recovers the message.

The game returns a Bool directly rather than using guard, so it does not require AlternativeMonad.

def AsymmEncAlg.PerfectlyCorrect {m : Type → Type v} [Monad m] {M PK SK C : Type} (encAlg : AsymmEncAlg m M PK SK C) [DecidableEq M] (runtime : ProbCompRuntime m) : Prop

An asymmetric encryption scheme is perfectly correct under the given runtime when decrypting a fresh encryption of any message succeeds with probability 1.

def AsymmEncAlg.ExplicitCoins.toAsymmEncAlg {m : Type → Type v} [Monad m] {M PK SK R C : Type} (encAlg : ExplicitCoins m M PK SK R C) [SampleableType R] (runtime : ProbCompRuntime m) : AsymmEncAlg m M PK SK C

Forget the explicit-coins presentation by sampling the coins through the ambient runtime's public-randomness capability.