Symmetric Encryption Schemes

This file defines SymmEncAlg m M K C, a monad-generic symmetric encryption scheme with message space M, key space K, and ciphertext space C.

The struct follows the same pattern as AsymmEncAlg, KEMScheme, MacAlg, etc.: it is parameterized by an ambient monad m and uses plain Type parameters. Asymptotic security statements are expressed externally by quantifying over a family (sp : ℕ) → SymmEncAlg m (M sp) (K sp) (C sp).

structure SymmEncAlg (m : Type → Type u) [Monad m] (M K C : Type) : Type u

• keygen : m K
• encrypt : K → M → m C
• decrypt : K → C → m (Option M)

def SymmEncAlg.CompleteExp {m : Type → Type u} [Monad m] {M K C : Type} (encAlg : SymmEncAlg m M K C) (msg : M) : m (Option M)

def SymmEncAlg.Complete {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : 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 : Type → Type u} [Monad m] {M K C : Type} (encAlg : SymmEncAlg m M K C) (mgen : m M) : m (M × C)

Joint message/ciphertext experiment used to express perfect secrecy.

def SymmEncAlg.PerfectSecrecyCipherExp {m : Type → Type u} [Monad m] {M K C : Type} (encAlg : SymmEncAlg m M K C) (mgen : m M) : m C

Ciphertext marginal induced by the perfect-secrecy experiment.

def SymmEncAlg.PerfectSecrecyCipherGivenMsgExp {m : Type → Type u} [Monad m] {M K C : Type} (encAlg : SymmEncAlg m M K C) (msg : M) : m C

Ciphertext experiment conditioned on a fixed message.

theorem SymmEncAlg.PerfectSecrecyExp_eq_bind {m : Type → Type u} [Monad m] {M K C : Type} [LawfulMonad m] (encAlg : SymmEncAlg m M K C) (mgen : m M) : encAlg.PerfectSecrecyExp mgen = do let msg ← mgen (fun (x : C) => (msg, x)) <$> encAlg.PerfectSecrecyCipherGivenMsgExp msg

theorem SymmEncAlg.PerfectSecrecyCipherExp_eq_bind {m : Type → Type u} [Monad m] {M K C : Type} [LawfulMonad m] (encAlg : SymmEncAlg m M K C) (mgen : m M) : encAlg.PerfectSecrecyCipherExp mgen = do let msg ← mgen encAlg.PerfectSecrecyCipherGivenMsgExp msg

theorem SymmEncAlg.probOutput_PerfectSecrecyExp_eq_mul_cipherGivenMsg {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] [LawfulMonad m] (encAlg : SymmEncAlg m M K C) (mgen : m M) (msg : M) (σ : C) : Pr[= (msg, σ) | encAlg.PerfectSecrecyExp mgen] = Pr[= msg | mgen] * Pr[= σ | encAlg.PerfectSecrecyCipherGivenMsgExp msg]

theorem SymmEncAlg.probOutput_PerfectSecrecyCipherExp_eq_tsum {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] [LawfulMonad m] (encAlg : SymmEncAlg m M K C) (mgen : m M) (σ : C) : Pr[= σ | encAlg.PerfectSecrecyCipherExp mgen] = ∑' (msg : M), Pr[= msg | mgen] * Pr[= σ | encAlg.PerfectSecrecyCipherGivenMsgExp msg]

def SymmEncAlg.perfectSecrecyAtAllPriors {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : Prop

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

def SymmEncAlg.ciphertextRowsEqualAt {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : Prop

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

theorem SymmEncAlg.perfectSecrecyAtAllPriors_iff_ciphertextRowsEqualAt {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) [Finite M] : encAlg.perfectSecrecyAtAllPriors ↔ encAlg.ciphertextRowsEqualAt

def SymmEncAlg.perfectSecrecyAt {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : Prop

Standard perfect secrecy expressed as independence: Pr[(M, C)] = Pr[M] * Pr[C].

def SymmEncAlg.perfectSecrecyPosteriorEqPriorAt {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : Prop

Posterior-equals-prior form, written in cross-multiplied form to avoid division.

def SymmEncAlg.perfectSecrecyJointFactorizationAt {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : Prop

Joint-factorization form (same mathematical statement as independence, with explicit named priors/marginals).

theorem SymmEncAlg.perfectSecrecyAt_iff_posteriorEqPriorAt {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : encAlg.perfectSecrecyAt ↔ encAlg.perfectSecrecyPosteriorEqPriorAt

theorem SymmEncAlg.perfectSecrecyAt_iff_jointFactorizationAt {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) : encAlg.perfectSecrecyAt ↔ encAlg.perfectSecrecyJointFactorizationAt

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

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 : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) [Fintype K] (deterministicEnc : ∀ (k : K) (msg : M), ∃ (c : C), support (encAlg.encrypt k msg) = {c}) (hKeyUniform : ∀ (k : K), Pr[= k | encAlg.keygen] = (↑(Fintype.card K))⁻¹) (hUniqueKey : ∀ (msg : M) (c : C), ∃! k : K, k ∈ support encAlg.keygen ∧ c ∈ support (encAlg.encrypt k msg)) : encAlg.ciphertextRowsEqualAt

theorem SymmEncAlg.perfectSecrecyAt_of_uniformKey_of_uniqueKey {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] [LawfulMonad m] (encAlg : SymmEncAlg m M K C) [Fintype K] (deterministicEnc : ∀ (k : K) (msg : M), ∃ (c : C), support (encAlg.encrypt k msg) = {c}) : ((∀ (k : K), Pr[= k | encAlg.keygen] = (↑(Fintype.card K))⁻¹) ∧ ∀ (msg : M) (c : C), ∃! k : K, k ∈ support encAlg.keygen ∧ c ∈ support (encAlg.encrypt k msg)) → encAlg.perfectSecrecyAt

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

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

theorem SymmEncAlg.perfectSecrecyAtAllPriors_of_uniformKey_of_uniqueKey {m : Type → Type u} [Monad m] {M K C : Type} [HasEvalPMF m] (encAlg : SymmEncAlg m M K C) [Finite M] [Fintype K] (deterministicEnc : ∀ (k : K) (msg : M), ∃ (c : C), support (encAlg.encrypt k msg) = {c}) : ((∀ (k : K), Pr[= k | encAlg.keygen] = (↑(Fintype.card K))⁻¹) ∧ ∀ (msg : M) (c : C), ∃! k : K, k ∈ support encAlg.keygen ∧ c ∈ support (encAlg.encrypt k msg)) → encAlg.perfectSecrecyAtAllPriors

Constructive Shannon direction for all priors: uniform keys plus uniqueness imply perfect secrecy for all prior distributions on messages.