Perfect Secrecy: Internal proofs

Auxiliary lemmas for perfect secrecy:

• Equivalence of the conditional-probability and independence formulations
• Both directions of the ciphertext indistinguishability characterization ([KL20], Lemma 2.5)
• Shannon's key-space bound ([KL20], Theorem 2.12)

theorem Cslib.Crypto.Protocols.PerfectSecrecy.jointDist_eq {M K C : Type u} (scheme : EncScheme M K C) (msgDist : PMF M) (m : M) (c : C) : (scheme.jointDist msgDist) (m, c) = msgDist m * (scheme.ciphertextDist m) c

The joint distribution at (m, c) equals msgDist m * ciphertextDist m c.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.jointDist_tsum_fst {M K C : Type u} (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) : ∑' (m : M), (scheme.jointDist msgDist) (m, c) = (scheme.marginalCiphertextDist msgDist) c

Summing the joint distribution over messages gives the marginal ciphertext distribution.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.perfectlySecret_iff_indep {M K C : Type u} (scheme : EncScheme M K C) : scheme.PerfectlySecret ↔ ∀ (msgDist : PMF M) (m : M) (c : C), (scheme.jointDist msgDist) (m, c) = msgDist m * (scheme.marginalCiphertextDist msgDist) c

Perfect secrecy is equivalent to message-ciphertext independence. The two formulations are related by multiplying/dividing by marginal(c).

theorem Cslib.Crypto.Protocols.PerfectSecrecy.indep_of_ciphertextIndist {M K C : Type u} (scheme : EncScheme M K C) (h : scheme.CiphertextIndist) (msgDist : PMF M) (m : M) (c : C) : (scheme.jointDist msgDist) (m, c) = msgDist m * (scheme.marginalCiphertextDist msgDist) c

Ciphertext indistinguishability implies message-ciphertext independence.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.perfectlySecret_of_ciphertextIndist {M K C : Type u} (scheme : EncScheme M K C) (h : scheme.CiphertextIndist) : scheme.PerfectlySecret

Ciphertext indistinguishability implies perfect secrecy.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.ciphertextIndist_of_perfectlySecret {M K C : Type u} (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) : scheme.CiphertextIndist

Perfect secrecy implies ciphertext indistinguishability.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.encrypt_key_injective {M K C : Type u} (scheme : EncScheme M K C) (f : M → K) (c₀ : C) (hf_mem : ∀ (m : M), f m ∈ scheme.gen.support) (hf_enc : ∀ (m : M), c₀ ∈ (scheme.enc (f m) m).support) : Function.Injective f

If each message maps to a key that encrypts it to a common ciphertext, then the key assignment is injective (by correctness of decryption).

theorem Cslib.Crypto.Protocols.PerfectSecrecy.shannonKeySpace {M K C : Type u} [Finite K] (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) : Nat.card K ≥ Nat.card M

Perfect secrecy requires |K| ≥ |M| (Shannon's theorem).