Symmetric Encryption Schemes.

This file defines a type SymmEncAlg spec M K C to represent a protocol for symmetric encryption using oracles in spec, with message space M, secret keys of type K, and ciphertext space C.

structure SymmEncAlg (M K C : ℕ → Type) (Q : Type v) extends OracleContext Q ProbComp : Type (v + 1)

• spec : OracleSpec Q
• impl : QueryImpl self.spec ProbComp
• keygen (sp : ℕ) : OracleComp self.spec (K sp)
• encrypt {sp : ℕ} (k : K sp) (msg : M sp) : OracleComp self.spec (C sp)
• decrypt {sp : ℕ} (k : K sp) (c : C sp) : OptionT (OracleComp self.spec) (M sp)

def SymmEncAlg.CompleteExp {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) {sp : ℕ} (m : M sp) : OptionT (OracleComp encAlg.spec) (M sp)

def SymmEncAlg.Complete {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : Prop

Definitions and Equivalences

perfectSecrecyAt is the canonical notion (independence form). We also provide equivalent formulations:

• perfectSecrecyPosteriorEqPriorAt (cross-multiplied posterior/prior form),
• perfectSecrecyJointFactorizationAt (same factorization with named marginals).

The _iff_ lemmas below record equivalence between these forms.

def SymmEncAlg.PerfectSecrecyExp {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (mgen : OracleComp encAlg.spec (M sp)) : ProbComp (M sp × C sp)

Joint message/ciphertext experiment used to express perfect secrecy.

def SymmEncAlg.PerfectSecrecyCipherExp {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (mgen : OracleComp encAlg.spec (M sp)) : ProbComp (C sp)

Ciphertext marginal induced by the perfect-secrecy experiment.

def SymmEncAlg.PerfectSecrecyPriorExp {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (mgen : OracleComp encAlg.spec (M sp)) : ProbComp (M sp)

Message prior induced by the message generator.

def SymmEncAlg.PerfectSecrecyCipherGivenMsgExp {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (msg : M sp) : ProbComp (C sp)

Ciphertext experiment conditioned on a fixed message.

theorem SymmEncAlg.PerfectSecrecyExp_eq_bind {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (mgen : OracleComp encAlg.spec (M sp)) : encAlg.PerfectSecrecyExp sp mgen = do let msg ← encAlg.PerfectSecrecyPriorExp sp mgen (fun (x : C sp) => (msg, x)) <$> encAlg.PerfectSecrecyCipherGivenMsgExp sp msg

theorem SymmEncAlg.PerfectSecrecyCipherExp_eq_bind {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (mgen : OracleComp encAlg.spec (M sp)) : encAlg.PerfectSecrecyCipherExp sp mgen = do let msg ← encAlg.PerfectSecrecyPriorExp sp mgen encAlg.PerfectSecrecyCipherGivenMsgExp sp msg

theorem SymmEncAlg.probOutput_PerfectSecrecyExp_eq_mul_cipherGivenMsg {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (mgen : OracleComp encAlg.spec (M sp)) (msg : M sp) (σ : C sp) : Pr[=(msg, σ) | encAlg.PerfectSecrecyExp sp mgen] = Pr[=msg | encAlg.PerfectSecrecyPriorExp sp mgen] * Pr[=σ | encAlg.PerfectSecrecyCipherGivenMsgExp sp msg]

theorem SymmEncAlg.probOutput_PerfectSecrecyCipherExp_eq_tsum {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) (mgen : OracleComp encAlg.spec (M sp)) (σ : C sp) : Pr[=σ | encAlg.PerfectSecrecyCipherExp sp mgen] = ∑' (msg : M sp), Pr[=msg | encAlg.PerfectSecrecyPriorExp sp mgen] * Pr[=σ | encAlg.PerfectSecrecyCipherGivenMsgExp sp msg]

def SymmEncAlg.perfectSecrecyAtAllPriors {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) : Prop

Strong perfect secrecy at a fixed security parameter: ciphertexts are independent of messages for every prior distribution on messages (PMF-level quantification).

def SymmEncAlg.ciphertextRowsEqualAt {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) : Prop

Equivalent channel-style formulation: every message induces the same ciphertext distribution.

theorem SymmEncAlg.perfectSecrecyAtAllPriors_iff_ciphertextRowsEqualAt {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) [Fintype (M sp)] : encAlg.perfectSecrecyAtAllPriors sp ↔ encAlg.ciphertextRowsEqualAt sp

def SymmEncAlg.perfectSecrecyAt {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) : Prop

Standard perfect secrecy at one security parameter, expressed as independence: Pr[(M, C)] = Pr[M] * Pr[C]. This is the canonical code-level definition.

def SymmEncAlg.perfectSecrecy {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : Prop

Canonical asymptotic perfect secrecy notion.

def SymmEncAlg.perfectSecrecyPosteriorEqPriorAt {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) : Prop

Posterior-equals-prior form, written in cross-multiplied form to avoid division. This is equivalent to perfectSecrecyAt.

def SymmEncAlg.perfectSecrecyJointFactorizationAt {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) : Prop

Joint-factorization form (same mathematical statement as independence, with explicit named priors/marginals). This is equivalent to perfectSecrecyAt.

def SymmEncAlg.perfectSecrecyPosteriorEqPrior {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : Prop

def SymmEncAlg.perfectSecrecyJointFactorization {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : Prop

theorem SymmEncAlg.perfectSecrecyAt_iff_posteriorEqPriorAt {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) : encAlg.perfectSecrecyAt sp ↔ encAlg.perfectSecrecyPosteriorEqPriorAt sp

theorem SymmEncAlg.perfectSecrecyAt_iff_jointFactorizationAt {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) : encAlg.perfectSecrecyAt sp ↔ encAlg.perfectSecrecyJointFactorizationAt sp

theorem SymmEncAlg.perfectSecrecy_iff_posteriorEqPrior {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : encAlg.perfectSecrecy ↔ encAlg.perfectSecrecyPosteriorEqPrior

theorem SymmEncAlg.perfectSecrecy_iff_jointFactorization {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) : encAlg.perfectSecrecy ↔ encAlg.perfectSecrecyJointFactorization

theorem SymmEncAlg.cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) [Fintype (K sp)] (deterministicEnc : ∀ (k : K sp) (msg : M sp), ∃ (c : C sp), support (simulateQ encAlg.impl (encAlg.encrypt k msg)) = {c}) (hKeyUniform : ∀ (k : K sp), Pr[=k | simulateQ encAlg.impl (encAlg.keygen sp)] = (↑(Fintype.card (K sp)))⁻¹) (hUniqueKey : ∀ (msg : M sp) (c : C sp), ∃! k : K sp, k ∈ support (simulateQ encAlg.impl (encAlg.keygen sp)) ∧ c ∈ support (simulateQ encAlg.impl (encAlg.encrypt k msg))) (msg : M sp) (σ : C sp) : Pr[=σ | encAlg.PerfectSecrecyCipherGivenMsgExp sp msg] = (↑(Fintype.card (K sp)))⁻¹

Core uniformity lemma: uniform keygen plus unique key per (message, ciphertext) pair implies every (message, ciphertext) conditional has probability (card K)⁻¹. Both Shannon theorems follow from this.

theorem SymmEncAlg.ciphertextRowsEqualAt_of_uniformKey_of_uniqueKey {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) [Fintype (K sp)] (deterministicEnc : ∀ (k : K sp) (msg : M sp), ∃ (c : C sp), support (simulateQ encAlg.impl (encAlg.encrypt k msg)) = {c}) (hKeyUniform : ∀ (k : K sp), Pr[=k | simulateQ encAlg.impl (encAlg.keygen sp)] = (↑(Fintype.card (K sp)))⁻¹) (hUniqueKey : ∀ (msg : M sp) (c : C sp), ∃! k : K sp, k ∈ support (simulateQ encAlg.impl (encAlg.keygen sp)) ∧ c ∈ support (simulateQ encAlg.impl (encAlg.encrypt k msg))) : encAlg.ciphertextRowsEqualAt sp

theorem SymmEncAlg.perfectSecrecyAt_of_uniformKey_of_uniqueKey {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) [Fintype (M sp)] [Fintype (K sp)] [Fintype (C sp)] (deterministicEnc : ∀ (k : K sp) (msg : M sp), ∃ (c : C sp), support (simulateQ encAlg.impl (encAlg.encrypt k msg)) = {c}) : ((∀ (k : K sp), Pr[=k | simulateQ encAlg.impl (encAlg.keygen sp)] = (↑(Fintype.card (K sp)))⁻¹) ∧ ∀ (msg : M sp) (c : C sp), ∃! k : K sp, k ∈ support (simulateQ encAlg.impl (encAlg.keygen sp)) ∧ c ∈ support (simulateQ encAlg.impl (encAlg.encrypt k msg))) → encAlg.perfectSecrecyAt sp

Constructive Shannon direction at fixed security parameter: if keygen is uniform and each (message, ciphertext) pair is realized by a unique key in support, then perfect secrecy holds (perfectSecrecyAt).

deterministicEnc asserts encryption is deterministic in distribution (singleton support for each fixed (key, message)).

Note: the converse direction requires stronger prior expressivity assumptions than perfectSecrecyAt currently encodes; see perfectSecrecyAtAllPriors.

theorem SymmEncAlg.perfectSecrecyAtAllPriors_of_card_eq_of_uniform_unique {M K C : ℕ → Type} {Q : Type v} (encAlg : SymmEncAlg M K C Q) (sp : ℕ) [Fintype (M sp)] [Fintype (K sp)] [Fintype (C sp)] (_hComplete : encAlg.Complete) (_h1 : Fintype.card (M sp) = Fintype.card (K sp)) (_h2 : Fintype.card (K sp) = Fintype.card (C sp)) (deterministicEnc : ∀ (k : K sp) (msg : M sp), ∃ (c : C sp), support (simulateQ encAlg.impl (encAlg.encrypt k msg)) = {c}) : ((∀ (k : K sp), Pr[=k | simulateQ encAlg.impl (encAlg.keygen sp)] = (↑(Fintype.card (K sp)))⁻¹) ∧ ∀ (msg : M sp) (c : C sp), ∃! k : K sp, k ∈ support (simulateQ encAlg.impl (encAlg.keygen sp)) ∧ c ∈ support (simulateQ encAlg.impl (encAlg.encrypt k msg))) → encAlg.perfectSecrecyAtAllPriors sp

Strong constructive Shannon direction with cardinality/completeness context: uniform keys plus uniqueness imply perfect secrecy for all priors.