feat(Cryptography): formalise perfect secrecy and the one-time pad

Cslib.lean

@@ -36,6 +36,12 @@ public import Cslib.Computability.URM.Defs
 public import Cslib.Computability.URM.Execution
 public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy
+public import Cslib.Crypto.Protocols.PerfectSecrecy.OneTimePad
 public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects

Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy
+
+@[expose] public section
+
+/-!
+# Perfect Secrecy
+
+Characterisation theorems for perfect secrecy following
+[KatzLindell2020], Chapter 2.
+
+## Main results
+
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_iff_ciphertextIndist`:
+  ciphertext indistinguishability characterization ([KatzLindell2020], Lemma 2.5)
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_iff_posteriorEq`:
+  perfect secrecy as equality of posterior and prior distributions
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_keySpace_ge`:
+  Shannon's theorem, `|K| ≥ |M|` ([KatzLindell2020], Theorem 2.12)
+
+## References
+
+* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
+-/
+
+namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme
+
+universe u
+variable {M K C : Type u}
+
+/-- A scheme is perfectly secret iff the ciphertext distribution is
+independent of the plaintext ([KatzLindell2020], Lemma 2.5). -/
+theorem perfectlySecret_iff_ciphertextIndist (scheme : EncScheme M K C) :
+    scheme.PerfectlySecret ↔ scheme.CiphertextIndist :=
+  ⟨PerfectSecrecy.ciphertextIndist_of_perfectlySecret scheme,
+   PerfectSecrecy.perfectlySecret_of_ciphertextIndist scheme⟩
+
+/-- Perfect secrecy requires `|K| ≥ |M|`
+([KatzLindell2020], Theorem 2.12). -/
+theorem perfectlySecret_keySpace_ge [Finite K]
+    (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
+    Nat.card K ≥ Nat.card M :=
+  PerfectSecrecy.shannonKeySpace scheme h
+
+end Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme

Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
+public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+
+@[expose] public section
+
+/-!
+# Perfect Secrecy: Definitions
+
+Core definitions for perfect secrecy following [KatzLindell2020], Chapter 2.
+
+## Main definitions
+
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.ciphertextDist`:
+  ciphertext distribution for a given message
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.jointDist`:
+  joint (message, ciphertext) distribution given a message prior
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.marginalCiphertextDist`:
+  marginal ciphertext distribution given a message prior
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgProb`:
+  posterior probability `Pr[M = m | C = c]`
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgDist`:
+  posterior message distribution as a `PMF` (defined in the internal file)
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.PerfectlySecret`:
+  perfect secrecy ([KatzLindell2020], Definition 2.3)
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.CiphertextIndist`:
+  ciphertext indistinguishability ([KatzLindell2020], Lemma 2.5)
+-/
+
+namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme
+
+universe u
+variable {M K C : Type u}
+
+/-- The distribution of `Enc_K(m)` when `K ← Gen`. -/
+noncomputable def ciphertextDist (scheme : EncScheme M K C) (m : M) : PMF C := do
+  let k ← scheme.gen
+  scheme.enc k m
+
+/-- Joint distribution of `(M, C)` given a message prior. -/
+noncomputable def jointDist (scheme : EncScheme M K C) (msgDist : PMF M) : PMF (M × C) := do
+  let m ← msgDist
+  let c ← scheme.ciphertextDist m
+  pure (m, c)
+
+/-- Marginal ciphertext distribution given a message prior. -/
+noncomputable def marginalCiphertextDist (scheme : EncScheme M K C)
+    (msgDist : PMF M) : PMF C := do
+  let m ← msgDist
+  scheme.ciphertextDist m
+
+-- TODO: posteriorMsgProb is itself a distribution — define it as a PMF
+-- (see posteriorMsgDist in Internal/PerfectSecrecy.lean) and express
+-- PerfectlySecret in terms of equality of distributions.
+/-- Posterior probability `Pr[M = m | C = c]`. -/
+noncomputable def posteriorMsgProb (scheme : EncScheme M K C)
+    (msgDist : PMF M) (c : C) (m : M) : ENNReal :=
+  scheme.jointDist msgDist (m, c) / scheme.marginalCiphertextDist msgDist c
+
+/-- An encryption scheme is perfectly secret if `Pr[M = m | C = c] = Pr[M = m]`
+for every prior, message, and ciphertext with positive probability
+([KatzLindell2020], Definition 2.3). -/
+def PerfectlySecret (scheme : EncScheme M K C) : Prop :=
+  ∀ (msgDist : PMF M) (m : M) (c : C),
+    c ∈ (scheme.marginalCiphertextDist msgDist).support →
+    scheme.posteriorMsgProb msgDist c m = msgDist m
+
+/-- Ciphertext indistinguishability: the ciphertext distribution is the same
+for all messages ([KatzLindell2020], Lemma 2.5). -/
+def CiphertextIndist (scheme : EncScheme M K C) : Prop :=
+  ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁
+
+end Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme

Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Probability.ProbabilityMassFunction.Monad
+
+@[expose] public section
+
+/-!
+# Private-Key Encryption Schemes (Information-Theoretic)
+
+An information-theoretic private-key encryption scheme following
+[KatzLindell2020], Definition 2.1. Key generation and encryption are
+probability distributions over arbitrary types, with no computational
+constraints.
+
+## Main definitions
+
+- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme`:
+  a private-key encryption scheme (Gen, Enc, Dec) with correctness
+
+## References
+
+* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
+-/
+
+namespace Cslib.Crypto.Protocols.PerfectSecrecy
+
+/--
+A private-key encryption scheme over message space `M`, key space `K`,
+and ciphertext space `C` ([KatzLindell2020], Definition 2.1).
+-/
+structure EncScheme.{u} (M K C : Type u) where
+  /-- Probabilistic key generation. -/
+  gen : PMF K
+  /-- (Possibly randomized) encryption. -/
+  enc : K → M → PMF C
+  /-- Deterministic decryption. -/
+  dec : K → C → M
+  /-- Decryption inverts encryption for all keys in the support of `gen`. -/
+  correct : ∀ k, k ∈ gen.support → ∀ m c, c ∈ (enc k m).support → dec k c = m
+
+end Cslib.Crypto.Protocols.PerfectSecrecy

Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Probability.Distributions.Uniform
+
+@[expose] public section
+
+/-!
+# One-Time Pad: Internal proofs
+
+The OTP ciphertext distribution is uniform regardless of message.
+-/
+
+namespace Cslib.Crypto.Protocols.PerfectSecrecy.OTP
+
+-- TODO: upstream to Mathlib as a FinEnum instance for BitVec.
+@[reducible] noncomputable def bitVecFintype (n : ℕ) : Fintype (BitVec n) :=
+  Fintype.ofEquiv (Fin (2 ^ n))
+    ⟨BitVec.ofFin, BitVec.toFin, fun x => by simp, fun x => by simp⟩
+
+-- TODO: upstream to Mathlib — general BitVec XOR cancellation lemma.
+/-- XOR by a fixed mask is self-inverse on `BitVec`: `c = k ^^^ m ↔ k = c ^^^ m`. -/
+lemma xor_right_eq_iff {l : ℕ} (c m k : BitVec l) :
+    (c = k ^^^ m) ↔ (k = c ^^^ m) := by grind
+
+/-- The ciphertext distribution of the OTP is uniform, regardless of the message. -/
+theorem otp_ciphertextDist_eq_uniform (l : ℕ) (m : BitVec l) :
+    haveI := bitVecFintype l
+    (PMF.uniformOfFintype (BitVec l)).bind
+      (fun k => PMF.pure (k ^^^ m)) =
+    PMF.uniformOfFintype (BitVec l) := by simp [PMF.ext_iff, xor_right_eq_iff]
+
+end Cslib.Crypto.Protocols.PerfectSecrecy.OTP