Perfect Secrecy

Characterisation theorems for perfect secrecy following [KL20], Chapter 2: the equivalence with message-ciphertext independence, the ciphertext indistinguishability characterization, and Shannon's key-space bound.

Main results

• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_iff_indep: perfect secrecy is exactly message-ciphertext independence
• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_iff_ciphertextIndist: ciphertext indistinguishability characterization ([KL20], Lemma 2.5)
• Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_keySpace_ge: Shannon's theorem, |K| ≥ |M| ([KL20], Theorem 2.12)

References

• J. Katz, Y. Lindell, Introduction to Modern Cryptography

theorem Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.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.EncScheme.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.EncScheme.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.EncScheme.perfectlySecret_iff_ciphertextIndist {M K C : Type u} (scheme : EncScheme M K C) : scheme.PerfectlySecret ↔ scheme.CiphertextIndist

A scheme is perfectly secret iff the ciphertext distribution is independent of the plaintext ([KL20], Lemma 2.5).

theorem Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.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.EncScheme.perfectlySecret_keySpace_ge {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 ([KL20], Theorem 2.12).