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

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.IND_CPA_oracleSpec {M PK SK C : Type} (_encAlg : AsymmEncAlg ProbComp M PK SK C) : OracleSpec (ℕ ⊕ PUnit.{u_1 + 1})

Equations

• _encAlg.IND_CPA_oracleSpec = unifSpec ++ₒ (M × M →ₒ C)

def AsymmEncAlg.IND_CPA_adversary {M PK SK C : Type} (encAlg : AsymmEncAlg ProbComp M PK SK C) : Type (max 1 u_1)

Equations

• encAlg.IND_CPA_adversary = (PK → OracleComp encAlg.IND_CPA_oracleSpec Bool)

def AsymmEncAlg.IND_CPA_queryImpl' {M PK SK C : Type} [DecidableEq M] [DecidableEq C] (encAlg : AsymmEncAlg ProbComp M PK SK C) (pk : PK) (b : Bool) : QueryImpl encAlg.IND_CPA_oracleSpec (StateT (M × M →ₒ C).QueryCache ProbComp)

Can be shown this is equivalent to below definition for asymptotic security.

Equations

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

def AsymmEncAlg.IND_CPA_queryImpl {M PK SK C : Type} (encAlg : AsymmEncAlg ProbComp M PK SK C) (pk : PK) (b : Bool) : QueryImpl encAlg.IND_CPA_oracleSpec (StateT (M × M →ₒ C).QueryCache ProbComp)

Equations

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

def AsymmEncAlg.IND_CPA_experiment {M PK SK C : Type} [DecidableEq M] [DecidableEq C] {encAlg : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg.IND_CPA_adversary) : ProbComp Unit

Equations

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

noncomputable def AsymmEncAlg.IND_CPA_advantage {M PK SK C : Type} [DecidableEq M] [DecidableEq C] {encAlg : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg.IND_CPA_adversary) : ENNReal

Equations

• AsymmEncAlg.IND_CPA_advantage adversary = [=()|AsymmEncAlg.IND_CPA_experiment adversary] - 1 / 2

theorem AsymmEncAlg.probOutput_IND_CPA_experiment_eq_add {M PK SK C : Type} [DecidableEq M] [DecidableEq C] {encAlg : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg.IND_CPA_adversary) : [=()|IND_CPA_experiment adversary] = [=()|do let __discr ← encAlg.keygen match __discr with | (pk, _sk) => do let b ← (OracleComp.simulateQ (encAlg.IND_CPA_queryImpl' pk true) (adversary pk)).run' ∅ guard (b = true)] / ↑2 + [=()|do let __discr ← encAlg.keygen match __discr with | (pk, _sk) => do let b ← (OracleComp.simulateQ (encAlg.IND_CPA_queryImpl' pk false) (adversary pk)).run' ∅ guard ¬b = true] / 2

The probability of the IND-CPA experiment is the average of the probability of the experiment with the challenge being true and the probability of the experiment with the challenge being false.

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.

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

IND_CPA_adv M PK C is an adversary for IND-CPA security game on an asymmetric encryption with public keys in PK, messages in M, and ciphertexts in C. The adversary consists of two functions:

• chooseMessages: given a public key, returns a pair of messages that it thinks it can distinguish the encryption of, and a private state.
• distinguish: given a private state and an encryption, returns whether it is an encryption of the first message or the second message

• State : Type
• chooseMessages : PK → m (M × M × self.State)
• distinguish : self.State → C → m Bool

def AsymmEncAlg.IND_CPA_OneTime_Game {ι : Type} {spec : OracleSpec ι} {M PK SK C : Type} {encAlg : AsymmEncAlg (OracleComp spec) M PK SK C} (adv : encAlg.IND_CPA_Adv) : ProbComp Bool

Experiment for one-time IND-CPA security of an asymmetric encryption algorithm:

1. Run keygen to get a public key and a private key.
2. Run adv.chooseMessages on pk to get a pair of messages and a private state.
3. The challenger then tosses a coin and encrypts one of the messages, returning the ciphertext c.
4. Run adv.distinguish on the private state and the ciphertext to get a boolean.
5. Return a Boolean indicating whether the adversary's guess is correct.

Note: we do not want to end with a guard statement, as this can be biased by the adversary potentially always failing.

Equations

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

noncomputable def AsymmEncAlg.IND_CPA_OneTime_Advantage {ι : Type} {spec : OracleSpec ι} {M PK SK C : Type} (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C) (adv : encAlg.IND_CPA_Adv) : ℝ

Equations

• encAlg.IND_CPA_OneTime_Advantage adv = (AsymmEncAlg.IND_CPA_OneTime_Game adv).advantage'