Asymmetric Encryption Schemes.

This file defines a type AsymmEncAlg spec M PK SK C to represent an protocol for asymmetric encryption using oracles in spec, with message space M, public/secret keys PK and SK, and ciphertext space C.

structure AsymmEncAlg (m : Type → Type u) (M PK SK C : Type) extends ExecutionMethod m : Type (max 1 u)

An AsymmEncAlg with message space M, key spaces PK and SK, and ciphertexts in C. spec is the available oracle set and m is the monad used to execute the oracle calls. Extends ExecutionMethod spec m, in most cases will be ExecutionMethod.default.

• exec {α : Type} : m α → ProbComp α
• lift_probComp {α : Type} : ProbComp α → m α
• exec_lift_probComp {α : Type} (px : ProbComp α) : self.exec (self.lift_probComp px) = px
• keygen : m (PK × SK)
• encrypt (pk : PK) (msg : M) : m C
• decrypt (sk : SK) (c : C) : Option M

def PKE_Alg (m : Type → Type u) (M PK SK C : Type) : Type (max 1 u)

Alias of AsymmEncAlg.

---

An AsymmEncAlg with message space M, key spaces PK and SK, and ciphertexts in C. spec is the available oracle set and m is the monad used to execute the oracle calls. Extends ExecutionMethod spec m, in most cases will be ExecutionMethod.default.

Equations

• PKE_Alg = AsymmEncAlg

@[reducible, inline]

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

A SymmEncAlg is complete if decrypting an encrypted message always returns that original message, captured here by a guard statement.

Equations

• One or more equations did not get rendered due to their size.

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

Perfectly correct if messages never fail to decrypt back to themselves for any message.

Equations

• encAlg.PerfectlyCorrect = ∀ (msg : M), [⊥|encAlg.CorrectExp msg] = 0

@[simp]

theorem AsymmEncAlg.PerfectlyCorrect_iff {m : Type → Type v} {M PK SK C : Type} [DecidableEq M] [AlternativeMonad m] (encAlg : AsymmEncAlg m M PK SK C) : encAlg.PerfectlyCorrect ↔ ∀ (msg : M), [⊥|encAlg.CorrectExp msg] = 0

def AsymmEncAlg.decryptionOracle {m : Type → Type v} {M PK SK C : Type} [AlternativeMonad m] (encAlg : AsymmEncAlg m M PK SK C) (sk : SK) : QueryImpl (C →ₒ M) m

Oracle that uses a secret key to respond to decryption requests.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AsymmEncAlg.decryptionOracle.apply_eq {m : Type → Type v} {M PK SK C α : Type} [AlternativeMonad m] (encAlg : AsymmEncAlg m M PK SK C) (sk : SK) (q : (C →ₒ M).OracleQuery α) : (encAlg.decryptionOracle sk).impl q = match α, q with | .((C →ₒ M).range ()), OracleSpec.query PUnit.unit c => (encAlg.decrypt sk c).getM

def AsymmEncAlg.IND_CCA_oracleSpec {m : Type → Type v} {M PK SK C : Type} (_encAlg : AsymmEncAlg m M PK SK C) : OracleSpec (PUnit.{u_2 + 1} ⊕ PUnit.{u_1 + 1})

Two oracles for IND-CCA Experiment, the first for decrypting ciphertexts, and the second for getting a challenge from a pair of messages.

Equations

• _encAlg.IND_CCA_oracleSpec = (C →ₒ Option M) ++ₒ (M × M →ₒ C)

def AsymmEncAlg.IND_CCA_oracleImpl {m : Type → Type v} {M PK SK C : Type} [AlternativeMonad m] [DecidableEq C] (encAlg : AsymmEncAlg m M PK SK C) (pk : PK) (sk : SK) (b : Bool) : QueryImpl encAlg.IND_CCA_oracleSpec (StateT (Option C) m)

Implement oracles for IND-CCA security game. A state monad is to track the current challenge, if it exists, and is set by the adversary calling the second oracle. The decryption oracle checks to make sure it doesn't decrypt the challenge.

Equations

• One or more equations did not get rendered due to their size.

structure AsymmEncAlg.IND_CCA_Adversary {m : Type → Type v} {M PK SK C : Type} (encAlg : AsymmEncAlg m M PK SK C) : Type (max (max 1 u_1) u_2)

• main : PK → OracleComp encAlg.IND_CCA_oracleSpec Bool

def AsymmEncAlg.IND_CCA_Game {m : Type → Type v} {M PK SK C : Type} [AlternativeMonad m] [DecidableEq C] (encAlg : AsymmEncAlg m M PK SK C) (adversary : encAlg.IND_CCA_Adversary) : ProbComp Unit

Equations

• One or more equations did not get rendered due to their size.