Perfect Secrecy

Characterisation theorems for perfect secrecy following [KL20], Chapter 2.

Main results

• 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.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.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| ([KL20], Theorem 2.12).