From 060f0304819b6f5486b43900044b37ba62b416b4 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Wed, 1 Apr 2026 10:06:06 -0400
Subject: [PATCH 1/3] feat: formalise perfect secrecy and the one-time pad
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds `Cslib.Cryptography.PerfectSecrecy` with information-theoretic
private-key encryption schemes and perfect secrecy following
Katz-Lindell, Chapter 2:

- `EncScheme`: private-key encryption (Definition 2.1)
- `PerfectlySecret`: perfect secrecy (Definition 2.3)
- `perfectlySecret_iff_ciphertextIndist`: ciphertext indistinguishability
  characterization (Lemma 2.5)
- `otp`: the one-time pad construction (Construction 2.9)
- `otp_perfectlySecret`: the OTP is perfectly secret (Theorem 2.10)
- `perfectlySecret_keySpace_ge`: Shannon's theorem, |K| ≥ |M|
  (Theorem 2.12)
---
 Cslib.lean                                    |   7 +
 Cslib/Cryptography/PerfectSecrecy.lean        |  11 ++
 .../PerfectSecrecy/Encryption.lean            |  48 +++++
 .../PerfectSecrecy/Internal/OneTimePad.lean   |  36 ++++
 .../Internal/PerfectSecrecy.lean              | 164 ++++++++++++++++++
 .../PerfectSecrecy/OneTimePad.lean            |  53 ++++++
 .../PerfectSecrecy/PerfectSecrecy.lean        |  51 ++++++
 .../PerfectSecrecy/PerfectSecrecy/Defs.lean   |  68 ++++++++
 8 files changed, 438 insertions(+)
 create mode 100644 Cslib/Cryptography/PerfectSecrecy.lean
 create mode 100644 Cslib/Cryptography/PerfectSecrecy/Encryption.lean
 create mode 100644 Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean
 create mode 100644 Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean
 create mode 100644 Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean
 create mode 100644 Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean
 create mode 100644 Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy/Defs.lean

diff --git a/Cslib.lean b/Cslib.lean
index a621d6e1..36cbc3b9 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -36,6 +36,13 @@ 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.Cryptography.PerfectSecrecy
+public import Cslib.Cryptography.PerfectSecrecy.Encryption
+public import Cslib.Cryptography.PerfectSecrecy.Internal.OneTimePad
+public import Cslib.Cryptography.PerfectSecrecy.Internal.PerfectSecrecy
+public import Cslib.Cryptography.PerfectSecrecy.OneTimePad
+public import Cslib.Cryptography.PerfectSecrecy.PerfectSecrecy
+public import Cslib.Cryptography.PerfectSecrecy.PerfectSecrecy.Defs
 public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
diff --git a/Cslib/Cryptography/PerfectSecrecy.lean b/Cslib/Cryptography/PerfectSecrecy.lean
new file mode 100644
index 00000000..a4c6e580
--- /dev/null
+++ b/Cslib/Cryptography/PerfectSecrecy.lean
@@ -0,0 +1,11 @@
+/-
+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.Cryptography.PerfectSecrecy.Encryption
+public import Cslib.Cryptography.PerfectSecrecy.PerfectSecrecy
+public import Cslib.Cryptography.PerfectSecrecy.OneTimePad
diff --git a/Cslib/Cryptography/PerfectSecrecy/Encryption.lean b/Cslib/Cryptography/PerfectSecrecy/Encryption.lean
new file mode 100644
index 00000000..9195faef
--- /dev/null
+++ b/Cslib/Cryptography/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
+[KatzLindell2021], Definition 2.1. Key generation and encryption are
+probability distributions over arbitrary types, with no computational
+constraints.
+
+## Main definitions
+
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme`:
+  a private-key encryption scheme (Gen, Enc, Dec) with correctness
+
+## References
+
+* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2021]
+-/
+
+namespace Cslib.Cryptography.PerfectSecrecy
+
+/--
+A private-key encryption scheme over message space `M`, key space `K`,
+and ciphertext space `C` ([KatzLindell2021], 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.Cryptography.PerfectSecrecy
diff --git a/Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean
new file mode 100644
index 00000000..832fb752
--- /dev/null
+++ b/Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean
@@ -0,0 +1,36 @@
+/-
+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.Cryptography.PerfectSecrecy.OTP
+
+/-- The ciphertext distribution of the OTP is uniform, regardless of the message. -/
+theorem otp_ciphertextDist_eq_uniform (l : ℕ) (m : Fin l → Bool) :
+    (PMF.uniformOfFintype (Fin l → Bool)).bind
+      (fun k => PMF.pure (fun i => k i ^^ m i)) =
+    PMF.uniformOfFintype (Fin l → Bool) := by
+  ext c
+  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, PMF.pure_apply]
+  have heq : ∀ a : Fin l → Bool,
+      (c = fun i => a i ^^ m i) ↔ (a = fun i => c i ^^ m i) :=
+    fun a => ⟨fun h => funext fun i => by have := congr_fun h i; simp_all,
+              fun h => funext fun i => by have := congr_fun h i; simp_all⟩
+  simp_rw [heq]
+  simp
+
+end Cslib.Cryptography.PerfectSecrecy.OTP
diff --git a/Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean
new file mode 100644
index 00000000..5c022362
--- /dev/null
+++ b/Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean
@@ -0,0 +1,164 @@
+/-
+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.Cryptography.PerfectSecrecy.PerfectSecrecy.Defs
+public import Mathlib.Probability.Distributions.Uniform
+
+@[expose] public section
+
+/-!
+# Perfect Secrecy: Internal proofs
+
+Auxiliary lemmas for perfect secrecy:
+- Equivalence of the conditional-probability and independence formulations
+- Both directions of the ciphertext indistinguishability characterization
+  ([KatzLindell2021], Lemma 2.5)
+- Shannon's key-space bound ([KatzLindell2021], Theorem 2.12)
+-/
+
+namespace Cslib.Cryptography.PerfectSecrecy
+
+open PMF ENNReal
+
+universe u
+variable {M K C : Type u}
+
+/-- The joint distribution at `(m, c)` equals `msgDist m * ciphertextDist m c`. -/
+theorem jointDist_eq (scheme : EncScheme M K C) (msgDist : PMF M)
+    (m : M) (c : C) :
+    scheme.jointDist msgDist (m, c) = msgDist m * scheme.ciphertextDist m c := by
+  change PMF.bind msgDist (fun m' =>
+    PMF.bind (scheme.ciphertextDist m') (fun c' => PMF.pure (m', c'))) (m, c) = _
+  rw [PMF.bind_apply]
+  rw [tsum_eq_single m]
+  · rw [PMF.bind_apply]
+    congr 1
+    rw [tsum_eq_single c]
+    · simp [PMF.pure_apply]
+    · intro c' hc'; simp [PMF.pure_apply, hc'.symm]
+  · intro m' hm'
+    rw [PMF.bind_apply]
+    simp [PMF.pure_apply, hm'.symm]
+
+/-- Summing the joint distribution over messages gives the marginal ciphertext distribution. -/
+theorem jointDist_tsum_fst (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) :
+    ∑' m, scheme.jointDist msgDist (m, c) = scheme.marginalCiphertextDist msgDist c := by
+  simp_rw [jointDist_eq]
+  change ∑' m, msgDist m * scheme.ciphertextDist m c =
+    PMF.bind msgDist (fun m => scheme.ciphertextDist m) c
+  rw [PMF.bind_apply]
+
+/-- Perfect secrecy is equivalent to message-ciphertext independence. -/
+theorem perfectlySecret_iff_indep (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 := by
+  constructor
+  · intro h msgDist m c
+    classical
+    by_cases hc : c ∈ (scheme.marginalCiphertextDist msgDist).support
+    · have hne : (scheme.marginalCiphertextDist msgDist) c ≠ 0 :=
+        (PMF.mem_support_iff _ _).mp hc
+      have hne_top : (scheme.marginalCiphertextDist msgDist) c ≠ ⊤ :=
+        ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one _ c)
+      have := h msgDist m c hc
+      simp only [EncScheme.posteriorMsgProb] at this
+      rw [← this]
+      exact (ENNReal.div_mul_cancel hne hne_top).symm
+    · simp only [PMF.mem_support_iff, not_not] at hc
+      have hj : scheme.jointDist msgDist (m, c) = 0 := by
+        have htsum := jointDist_tsum_fst scheme msgDist c
+        rw [hc] at htsum
+        exact (ENNReal.tsum_eq_zero.mp htsum) m
+      rw [hj, hc, mul_zero]
+  · intro h msgDist m c hc
+    have hne : (scheme.marginalCiphertextDist msgDist) c ≠ 0 :=
+      (PMF.mem_support_iff _ _).mp hc
+    have hne_top : (scheme.marginalCiphertextDist msgDist) c ≠ ⊤ :=
+      ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one _ c)
+    simp only [EncScheme.posteriorMsgProb]
+    rw [h msgDist m c, ENNReal.mul_div_cancel_right hne hne_top]
+
+/-- Ciphertext indistinguishability implies message-ciphertext independence. -/
+theorem indep_of_ciphertextIndist (scheme : EncScheme M K C)
+    (h : ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁)
+    (msgDist : PMF M) (m : M) (c : C) :
+    scheme.jointDist msgDist (m, c) =
+      msgDist m * scheme.marginalCiphertextDist msgDist c := by
+  rw [jointDist_eq]
+  congr 1
+  change scheme.ciphertextDist m c =
+    PMF.bind msgDist (fun m' => scheme.ciphertextDist m') c
+  rw [PMF.bind_apply]
+  have hd : ∀ m', scheme.ciphertextDist m' = scheme.ciphertextDist m :=
+    fun m' => h m' m
+  conv_rhs => arg 1; ext m'; rw [hd m']
+  rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul]
+
+/-- Ciphertext indistinguishability implies perfect secrecy. -/
+theorem backward (scheme : EncScheme M K C)
+    (h : ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁) :
+    scheme.PerfectlySecret :=
+  (perfectlySecret_iff_indep scheme).mpr (fun msgDist m c =>
+    indep_of_ciphertextIndist scheme h msgDist m c)
+
+/-- Perfect secrecy implies ciphertext indistinguishability. -/
+theorem forward (scheme : EncScheme M K C)
+    (h : scheme.PerfectlySecret) :
+    ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁ := by
+  classical
+  rw [perfectlySecret_iff_indep] at h
+  intro m₀ m₁
+  ext c
+  set s : Finset M := {m₀, m₁}
+  have hs : s.Nonempty := ⟨m₀, Finset.mem_insert_self m₀ {m₁}⟩
+  set μ := PMF.uniformOfFinset s hs
+  have key : ∀ m, μ m * scheme.ciphertextDist m c =
+      μ m * scheme.marginalCiphertextDist μ c := by
+    intro m
+    have := h μ m c
+    rw [jointDist_eq] at this
+    exact this
+  have hm₀ : μ m₀ ≠ 0 :=
+    (PMF.mem_support_uniformOfFinset_iff hs m₀).mpr (Finset.mem_insert_self m₀ {m₁})
+  have hm₁ : μ m₁ ≠ 0 :=
+    (PMF.mem_support_uniformOfFinset_iff hs m₁).mpr
+      (Finset.mem_insert_of_mem (Finset.mem_singleton_self m₁))
+  have hm₀_top : μ m₀ ≠ ⊤ := ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one μ m₀)
+  have hm₁_top : μ m₁ ≠ ⊤ := ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one μ m₁)
+  have h₀ : scheme.ciphertextDist m₀ c = scheme.marginalCiphertextDist μ c := by
+    have := key m₀; rw [mul_comm, mul_comm (μ m₀)] at this
+    exact (ENNReal.mul_left_inj hm₀ hm₀_top).mp this
+  have h₁ : scheme.ciphertextDist m₁ c = scheme.marginalCiphertextDist μ c := by
+    have := key m₁; rw [mul_comm, mul_comm (μ m₁)] at this
+    exact (ENNReal.mul_left_inj hm₁ hm₁_top).mp this
+  exact h₀.trans h₁.symm
+
+/-- Perfect secrecy requires `|K| ≥ |M|` (Shannon's theorem). -/
+theorem shannonKeySpace [Fintype M] [Fintype K]
+    (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
+    Fintype.card K ≥ Fintype.card M := by
+  classical
+  have hci := forward scheme h
+  by_cases hM : IsEmpty M
+  · simp [Fintype.card_eq_zero]
+  · rw [not_isEmpty_iff] at hM
+    obtain ⟨m₀⟩ := hM
+    obtain ⟨c₀, hc₀⟩ := (scheme.ciphertextDist m₀).support_nonempty
+    have key_exists : ∀ m, ∃ k ∈ scheme.gen.support, c₀ ∈ (scheme.enc k m).support := by
+      intro m
+      have : c₀ ∈ (scheme.ciphertextDist m).support := by rw [hci m m₀]; exact hc₀
+      exact (PMF.mem_support_bind_iff _ _ _).mp this
+    choose f hf_mem hf_enc using key_exists
+    exact Fintype.card_le_of_injective f fun m₁ m₂ heq => by
+      have h₁ := scheme.correct _ (hf_mem m₁) m₁ c₀ (hf_enc m₁)
+      have h₂ := scheme.correct _ (hf_mem m₂) m₂ c₀ (hf_enc m₂)
+      rw [heq] at h₁; exact h₁.symm.trans h₂
+
+end Cslib.Cryptography.PerfectSecrecy
diff --git a/Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean b/Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean
new file mode 100644
index 00000000..b1bd1ea5
--- /dev/null
+++ b/Cslib/Cryptography/PerfectSecrecy/OneTimePad.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.Cryptography.PerfectSecrecy.PerfectSecrecy
+public import Cslib.Cryptography.PerfectSecrecy.Internal.OneTimePad
+public import Mathlib.Probability.Distributions.Uniform
+
+@[expose] public section
+
+/-!
+# One-Time Pad
+
+The one-time pad (Vernam cipher) over `{0,1}^l`
+([KatzLindell2021], Construction 2.9).
+
+## Main definitions
+
+- `Cslib.Cryptography.PerfectSecrecy.otp`: the one-time pad encryption scheme
+
+## Main results
+
+- `Cslib.Cryptography.PerfectSecrecy.otp_perfectlySecret`:
+  the one-time pad is perfectly secret ([KatzLindell2021], Theorem 2.10)
+
+## References
+
+* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2021]
+-/
+
+namespace Cslib.Cryptography.PerfectSecrecy
+
+/-- The one-time pad over `l`-bit strings. Encryption and decryption
+are pointwise XOR ([KatzLindell2021], Construction 2.9). -/
+noncomputable def otp (l : ℕ) : EncScheme (Fin l → Bool) (Fin l → Bool) (Fin l → Bool) where
+  gen := PMF.uniformOfFintype _
+  enc := fun k m => PMF.pure (fun i => k i ^^ m i)
+  dec := fun k c => fun i => k i ^^ c i
+  correct := by intro k _ m c hc; simp at hc; simp [hc]
+
+/-- The one-time pad is perfectly secret ([KatzLindell2021], Theorem 2.10). -/
+theorem otp_perfectlySecret (l : ℕ) : (otp l).PerfectlySecret := by
+  rw [EncScheme.perfectlySecret_iff_ciphertextIndist]
+  intro m₀ m₁
+  simp only [EncScheme.ciphertextDist, otp]
+  exact (OTP.otp_ciphertextDist_eq_uniform l m₀).trans
+    (OTP.otp_ciphertextDist_eq_uniform l m₁).symm
+
+end Cslib.Cryptography.PerfectSecrecy
diff --git a/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean b/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean
new file mode 100644
index 00000000..faa7aa0a
--- /dev/null
+++ b/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean
@@ -0,0 +1,51 @@
+/-
+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.Cryptography.PerfectSecrecy.PerfectSecrecy.Defs
+public import Cslib.Cryptography.PerfectSecrecy.Internal.PerfectSecrecy
+
+@[expose] public section
+
+/-!
+# Perfect Secrecy
+
+Characterisation theorems for perfect secrecy following
+[KatzLindell2021], Chapter 2.
+
+## Main results
+
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme.perfectlySecret_iff_ciphertextIndist`:
+  ciphertext indistinguishability characterization ([KatzLindell2021], Lemma 2.5)
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme.perfectlySecret_keySpace_ge`:
+  Shannon's theorem, `|K| ≥ |M|` ([KatzLindell2021], Theorem 2.12)
+
+## References
+
+* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2021]
+-/
+
+namespace Cslib.Cryptography.PerfectSecrecy.EncScheme
+
+universe u
+variable {M K C : Type u}
+
+/-- A scheme is perfectly secret iff the ciphertext distribution is
+independent of the plaintext ([KatzLindell2021], Lemma 2.5). -/
+theorem perfectlySecret_iff_ciphertextIndist (scheme : EncScheme M K C) :
+    scheme.PerfectlySecret ↔
+    ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁ :=
+  ⟨PerfectSecrecy.forward scheme, PerfectSecrecy.backward scheme⟩
+
+/-- Perfect secrecy requires `|K| ≥ |M|`
+([KatzLindell2021], Theorem 2.12). -/
+theorem perfectlySecret_keySpace_ge [Fintype M] [Fintype K]
+    (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
+    Fintype.card K ≥ Fintype.card M :=
+  PerfectSecrecy.shannonKeySpace scheme h
+
+end Cslib.Cryptography.PerfectSecrecy.EncScheme
diff --git a/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy/Defs.lean b/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy/Defs.lean
new file mode 100644
index 00000000..21a6007a
--- /dev/null
+++ b/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy/Defs.lean
@@ -0,0 +1,68 @@
+/-
+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.Cryptography.PerfectSecrecy.Encryption
+public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+
+@[expose] public section
+
+/-!
+# Perfect Secrecy: Definitions
+
+Core definitions for perfect secrecy following [KatzLindell2021], Chapter 2.
+
+## Main definitions
+
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme.ciphertextDist`:
+  ciphertext distribution for a given message
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme.jointDist`:
+  joint (message, ciphertext) distribution given a message prior
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme.marginalCiphertextDist`:
+  marginal ciphertext distribution given a message prior
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme.posteriorMsgProb`:
+  posterior probability `Pr[M = m | C = c]`
+- `Cslib.Cryptography.PerfectSecrecy.EncScheme.PerfectlySecret`:
+  perfect secrecy ([KatzLindell2021], Definition 2.3)
+-/
+
+namespace Cslib.Cryptography.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
+
+/-- 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
+([KatzLindell2021], 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
+
+end Cslib.Cryptography.PerfectSecrecy.EncScheme

From 85d3c1b52d584edba1787e6b1fc409ab52df83fc Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Wed, 1 Apr 2026 14:08:17 -0400
Subject: [PATCH 2/3] refactor: address PR review feedback for perfect secrecy
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Addresses reviewer comments from linesthatinterlace and fmontesi.

Definitions and naming:
- Define `CiphertextIndist` predicate for ciphertext indistinguishability
- Define `posteriorMsgDist : PMF M` proving the posterior is a valid
  distribution, with `perfectlySecret_iff_posteriorEq`
- Rename `backward`/`forward` to `perfectlySecret_of_ciphertextIndist`
  and `ciphertextIndist_of_perfectlySecret`
- Extract `xor_right_eq_iff` and `encrypt_key_injective` as lemmas

OTP and types:
- Use `BitVec l` instead of `Fin l → Bool` for the one-time pad,
  with a `Fintype (BitVec n)` instance via `Fin (2^n)`

Generalisations:
- Weaken Shannon's bound from `[Fintype]` to `[Finite]` with `Nat.card`
- Shorten `perfectlySecret_iff_indep` proof

Housekeeping:
- Add KatzLindell2020 to references.bib (3rd ed., CRC Press, 2020)
- Fix citation key from KatzLindell2021 to KatzLindell2020
- Eliminate `PerfectSecrecy/PerfectSecrecy/` double directory
- Remove umbrella re-export module (not a pattern used in cslib)
- Revert unrelated CI workflow and .gitignore changes
---
 Cslib.lean                                    |  13 +-
 Cslib/Crypto/PerfectSecrecy/Basic.lean        |  53 ++++++++
 .../PerfectSecrecy/Defs.lean                  |  31 +++--
 .../PerfectSecrecy/Encryption.lean            |  12 +-
 .../PerfectSecrecy/Internal/OneTimePad.lean   |  45 +++++++
 .../Internal/PerfectSecrecy.lean              | 127 +++++++++++++-----
 Cslib/Crypto/PerfectSecrecy/OneTimePad.lean   |  58 ++++++++
 Cslib/Cryptography/PerfectSecrecy.lean        |  11 --
 .../PerfectSecrecy/Internal/OneTimePad.lean   |  36 -----
 .../PerfectSecrecy/OneTimePad.lean            |  53 --------
 .../PerfectSecrecy/PerfectSecrecy.lean        |  51 -------
 references.bib                                |  10 ++
 12 files changed, 288 insertions(+), 212 deletions(-)
 create mode 100644 Cslib/Crypto/PerfectSecrecy/Basic.lean
 rename Cslib/{Cryptography/PerfectSecrecy => Crypto}/PerfectSecrecy/Defs.lean (61%)
 rename Cslib/{Cryptography => Crypto}/PerfectSecrecy/Encryption.lean (80%)
 create mode 100644 Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
 rename Cslib/{Cryptography => Crypto}/PerfectSecrecy/Internal/PerfectSecrecy.lean (55%)
 create mode 100644 Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
 delete mode 100644 Cslib/Cryptography/PerfectSecrecy.lean
 delete mode 100644 Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean
 delete mode 100644 Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean
 delete mode 100644 Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean

diff --git a/Cslib.lean b/Cslib.lean
index 36cbc3b9..30d3fe1c 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -36,13 +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.Cryptography.PerfectSecrecy
-public import Cslib.Cryptography.PerfectSecrecy.Encryption
-public import Cslib.Cryptography.PerfectSecrecy.Internal.OneTimePad
-public import Cslib.Cryptography.PerfectSecrecy.Internal.PerfectSecrecy
-public import Cslib.Cryptography.PerfectSecrecy.OneTimePad
-public import Cslib.Cryptography.PerfectSecrecy.PerfectSecrecy
-public import Cslib.Cryptography.PerfectSecrecy.PerfectSecrecy.Defs
+public import Cslib.Crypto.PerfectSecrecy.Basic
+public import Cslib.Crypto.PerfectSecrecy.Defs
+public import Cslib.Crypto.PerfectSecrecy.Encryption
+public import Cslib.Crypto.PerfectSecrecy.Internal.OneTimePad
+public import Cslib.Crypto.PerfectSecrecy.Internal.PerfectSecrecy
+public import Cslib.Crypto.PerfectSecrecy.OneTimePad
 public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
diff --git a/Cslib/Crypto/PerfectSecrecy/Basic.lean b/Cslib/Crypto/PerfectSecrecy/Basic.lean
new file mode 100644
index 00000000..03603e97
--- /dev/null
+++ b/Cslib/Crypto/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.PerfectSecrecy.Defs
+public import Cslib.Crypto.PerfectSecrecy.Internal.PerfectSecrecy
+
+@[expose] public section
+
+/-!
+# Perfect Secrecy
+
+Characterisation theorems for perfect secrecy following
+[KatzLindell2020], Chapter 2.
+
+## Main results
+
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.perfectlySecret_iff_ciphertextIndist`:
+  ciphertext indistinguishability characterization ([KatzLindell2020], Lemma 2.5)
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.perfectlySecret_iff_posteriorEq`:
+  perfect secrecy as equality of posterior and prior distributions
+- `Cslib.Crypto.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.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 M] [Finite K]
+    (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
+    Nat.card K ≥ Nat.card M :=
+  PerfectSecrecy.shannonKeySpace scheme h
+
+end Cslib.Crypto.PerfectSecrecy.EncScheme
diff --git a/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy/Defs.lean b/Cslib/Crypto/PerfectSecrecy/Defs.lean
similarity index 61%
rename from Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy/Defs.lean
rename to Cslib/Crypto/PerfectSecrecy/Defs.lean
index 21a6007a..c02a724e 100644
--- a/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy/Defs.lean
+++ b/Cslib/Crypto/PerfectSecrecy/Defs.lean
@@ -6,7 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Cryptography.PerfectSecrecy.Encryption
+public import Cslib.Crypto.PerfectSecrecy.Encryption
 public import Mathlib.Probability.ProbabilityMassFunction.Constructions
 
 @[expose] public section
@@ -14,23 +14,27 @@ public import Mathlib.Probability.ProbabilityMassFunction.Constructions
 /-!
 # Perfect Secrecy: Definitions
 
-Core definitions for perfect secrecy following [KatzLindell2021], Chapter 2.
+Core definitions for perfect secrecy following [KatzLindell2020], Chapter 2.
 
 ## Main definitions
 
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme.ciphertextDist`:
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.ciphertextDist`:
   ciphertext distribution for a given message
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme.jointDist`:
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.jointDist`:
   joint (message, ciphertext) distribution given a message prior
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme.marginalCiphertextDist`:
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.marginalCiphertextDist`:
   marginal ciphertext distribution given a message prior
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme.posteriorMsgProb`:
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.posteriorMsgProb`:
   posterior probability `Pr[M = m | C = c]`
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme.PerfectlySecret`:
-  perfect secrecy ([KatzLindell2021], Definition 2.3)
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.posteriorMsgDist`:
+  posterior message distribution as a `PMF` (defined in the internal file)
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.PerfectlySecret`:
+  perfect secrecy ([KatzLindell2020], Definition 2.3)
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.CiphertextIndist`:
+  ciphertext indistinguishability ([KatzLindell2020], Lemma 2.5)
 -/
 
-namespace Cslib.Cryptography.PerfectSecrecy.EncScheme
+namespace Cslib.Crypto.PerfectSecrecy.EncScheme
 
 universe u
 variable {M K C : Type u}
@@ -59,10 +63,15 @@ noncomputable def posteriorMsgProb (scheme : EncScheme M K 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
-([KatzLindell2021], Definition 2.3). -/
+([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
 
-end Cslib.Cryptography.PerfectSecrecy.EncScheme
+/-- 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.PerfectSecrecy.EncScheme
diff --git a/Cslib/Cryptography/PerfectSecrecy/Encryption.lean b/Cslib/Crypto/PerfectSecrecy/Encryption.lean
similarity index 80%
rename from Cslib/Cryptography/PerfectSecrecy/Encryption.lean
rename to Cslib/Crypto/PerfectSecrecy/Encryption.lean
index 9195faef..248f6cc9 100644
--- a/Cslib/Cryptography/PerfectSecrecy/Encryption.lean
+++ b/Cslib/Crypto/PerfectSecrecy/Encryption.lean
@@ -15,25 +15,25 @@ public import Mathlib.Probability.ProbabilityMassFunction.Monad
 # Private-Key Encryption Schemes (Information-Theoretic)
 
 An information-theoretic private-key encryption scheme following
-[KatzLindell2021], Definition 2.1. Key generation and encryption are
+[KatzLindell2020], Definition 2.1. Key generation and encryption are
 probability distributions over arbitrary types, with no computational
 constraints.
 
 ## Main definitions
 
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme`:
+- `Cslib.Crypto.PerfectSecrecy.EncScheme`:
   a private-key encryption scheme (Gen, Enc, Dec) with correctness
 
 ## References
 
-* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2021]
+* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
 -/
 
-namespace Cslib.Cryptography.PerfectSecrecy
+namespace Cslib.Crypto.PerfectSecrecy
 
 /--
 A private-key encryption scheme over message space `M`, key space `K`,
-and ciphertext space `C` ([KatzLindell2021], Definition 2.1).
+and ciphertext space `C` ([KatzLindell2020], Definition 2.1).
 -/
 structure EncScheme.{u} (M K C : Type u) where
   /-- Probabilistic key generation. -/
@@ -45,4 +45,4 @@ structure EncScheme.{u} (M K C : Type u) where
   /-- 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.Cryptography.PerfectSecrecy
+end Cslib.Crypto.PerfectSecrecy
diff --git a/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
new file mode 100644
index 00000000..b82df67d
--- /dev/null
+++ b/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
@@ -0,0 +1,45 @@
+/-
+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.PerfectSecrecy.OTP
+
+noncomputable instance (n : ℕ) : Fintype (BitVec n) :=
+  Fintype.ofEquiv (Fin (2 ^ n))
+    ⟨BitVec.ofFin, BitVec.toFin, fun x => by simp, fun x => by simp⟩
+
+/-- 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
+  constructor
+  · rintro rfl
+    rw [BitVec.xor_assoc, BitVec.xor_self, BitVec.xor_zero]
+  · rintro rfl
+    rw [BitVec.xor_assoc, BitVec.xor_self, BitVec.xor_zero]
+
+/-- The ciphertext distribution of the OTP is uniform, regardless of the message. -/
+theorem otp_ciphertextDist_eq_uniform (l : ℕ) (m : BitVec l) :
+    (PMF.uniformOfFintype (BitVec l)).bind
+      (fun k => PMF.pure (k ^^^ m)) =
+    PMF.uniformOfFintype (BitVec l) := by
+  ext c
+  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, PMF.pure_apply]
+  simp_rw [xor_right_eq_iff c m]
+  simp
+
+end Cslib.Crypto.PerfectSecrecy.OTP
diff --git a/Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
similarity index 55%
rename from Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean
rename to Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
index 5c022362..0d7e012f 100644
--- a/Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean
+++ b/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
@@ -6,7 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Cryptography.PerfectSecrecy.PerfectSecrecy.Defs
+public import Cslib.Crypto.PerfectSecrecy.Defs
 public import Mathlib.Probability.Distributions.Uniform
 
 @[expose] public section
@@ -17,11 +17,11 @@ public import Mathlib.Probability.Distributions.Uniform
 Auxiliary lemmas for perfect secrecy:
 - Equivalence of the conditional-probability and independence formulations
 - Both directions of the ciphertext indistinguishability characterization
-  ([KatzLindell2021], Lemma 2.5)
-- Shannon's key-space bound ([KatzLindell2021], Theorem 2.12)
+  ([KatzLindell2020], Lemma 2.5)
+- Shannon's key-space bound ([KatzLindell2020], Theorem 2.12)
 -/
 
-namespace Cslib.Cryptography.PerfectSecrecy
+namespace Cslib.Crypto.PerfectSecrecy
 
 open PMF ENNReal
 
@@ -53,7 +53,57 @@ theorem jointDist_tsum_fst (scheme : EncScheme M K C) (msgDist : PMF M) (c : C)
     PMF.bind msgDist (fun m => scheme.ciphertextDist m) c
   rw [PMF.bind_apply]
 
-/-- Perfect secrecy is equivalent to message-ciphertext independence. -/
+/-- The posterior message probabilities sum to 1 when the ciphertext
+has positive probability. -/
+theorem posteriorMsgProb_hasSum (scheme : EncScheme M K C)
+    (msgDist : PMF M) (c : C)
+    (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) :
+    HasSum (fun m => scheme.posteriorMsgProb msgDist c m) 1 := by
+  have hne := (PMF.mem_support_iff _ _).mp hc
+  have hne_top := ne_top_of_le_ne_top one_ne_top
+    (PMF.coe_le_one (scheme.marginalCiphertextDist msgDist) c)
+  have : ∑' m, scheme.posteriorMsgProb msgDist c m = 1 := by
+    simp only [EncScheme.posteriorMsgProb, div_eq_mul_inv]
+    rw [ENNReal.tsum_mul_right, jointDist_tsum_fst]
+    exact ENNReal.mul_inv_cancel hne hne_top
+  exact this ▸ ENNReal.summable.hasSum
+
+namespace EncScheme
+
+/-- The posterior message distribution `Pr[M | C = c]` as a probability
+distribution, given a message prior and a ciphertext in the support of
+the marginal distribution. -/
+noncomputable def posteriorMsgDist (scheme : EncScheme M K C)
+    (msgDist : PMF M) (c : C)
+    (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) : PMF M :=
+  ⟨fun m => scheme.posteriorMsgProb msgDist c m,
+   posteriorMsgProb_hasSum scheme msgDist c hc⟩
+
+@[simp]
+theorem posteriorMsgDist_apply (scheme : EncScheme M K C)
+    (msgDist : PMF M) (c : C)
+    (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) (m : M) :
+    scheme.posteriorMsgDist msgDist c hc m =
+      scheme.posteriorMsgProb msgDist c m :=
+  rfl
+
+/-- Perfect secrecy: the posterior message distribution equals the prior. -/
+theorem perfectlySecret_iff_posteriorEq (scheme : EncScheme M K C) :
+    scheme.PerfectlySecret ↔
+    ∀ (msgDist : PMF M) (c : C)
+      (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support),
+      scheme.posteriorMsgDist msgDist c hc = msgDist := by
+  constructor
+  · intro h msgDist c hc
+    ext m
+    simp [h msgDist m c hc]
+  · intro h msgDist m c hc
+    simpa using DFunLike.congr_fun (h msgDist c hc) m
+
+end EncScheme
+
+/-- Perfect secrecy is equivalent to message-ciphertext independence.
+The two formulations are related by multiplying/dividing by `marginal(c)`. -/
 theorem perfectlySecret_iff_indep (scheme : EncScheme M K C) :
     scheme.PerfectlySecret ↔
     ∀ (msgDist : PMF M) (m : M) (c : C),
@@ -62,32 +112,25 @@ theorem perfectlySecret_iff_indep (scheme : EncScheme M K C) :
   constructor
   · intro h msgDist m c
     classical
-    by_cases hc : c ∈ (scheme.marginalCiphertextDist msgDist).support
-    · have hne : (scheme.marginalCiphertextDist msgDist) c ≠ 0 :=
-        (PMF.mem_support_iff _ _).mp hc
-      have hne_top : (scheme.marginalCiphertextDist msgDist) c ≠ ⊤ :=
-        ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one _ c)
-      have := h msgDist m c hc
+    by_cases hc : (scheme.marginalCiphertextDist msgDist) c = 0
+    · have := ENNReal.tsum_eq_zero.mp
+        ((jointDist_tsum_fst scheme msgDist c).trans hc) m
+      rw [this, hc, mul_zero]
+    · have hne_top := ne_top_of_le_ne_top one_ne_top
+        (PMF.coe_le_one (scheme.marginalCiphertextDist msgDist) c)
+      have := h msgDist m c ((PMF.mem_support_iff _ _).mpr hc)
       simp only [EncScheme.posteriorMsgProb] at this
-      rw [← this]
-      exact (ENNReal.div_mul_cancel hne hne_top).symm
-    · simp only [PMF.mem_support_iff, not_not] at hc
-      have hj : scheme.jointDist msgDist (m, c) = 0 := by
-        have htsum := jointDist_tsum_fst scheme msgDist c
-        rw [hc] at htsum
-        exact (ENNReal.tsum_eq_zero.mp htsum) m
-      rw [hj, hc, mul_zero]
+      rw [← this, ENNReal.div_mul_cancel hc hne_top]
   · intro h msgDist m c hc
-    have hne : (scheme.marginalCiphertextDist msgDist) c ≠ 0 :=
-      (PMF.mem_support_iff _ _).mp hc
-    have hne_top : (scheme.marginalCiphertextDist msgDist) c ≠ ⊤ :=
-      ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one _ c)
+    have hne := (PMF.mem_support_iff _ _).mp hc
+    have hne_top := ne_top_of_le_ne_top one_ne_top
+      (PMF.coe_le_one (scheme.marginalCiphertextDist msgDist) c)
     simp only [EncScheme.posteriorMsgProb]
     rw [h msgDist m c, ENNReal.mul_div_cancel_right hne hne_top]
 
 /-- Ciphertext indistinguishability implies message-ciphertext independence. -/
 theorem indep_of_ciphertextIndist (scheme : EncScheme M K C)
-    (h : ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁)
+    (h : scheme.CiphertextIndist)
     (msgDist : PMF M) (m : M) (c : C) :
     scheme.jointDist msgDist (m, c) =
       msgDist m * scheme.marginalCiphertextDist msgDist c := by
@@ -102,16 +145,16 @@ theorem indep_of_ciphertextIndist (scheme : EncScheme M K C)
   rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul]
 
 /-- Ciphertext indistinguishability implies perfect secrecy. -/
-theorem backward (scheme : EncScheme M K C)
-    (h : ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁) :
+theorem perfectlySecret_of_ciphertextIndist (scheme : EncScheme M K C)
+    (h : scheme.CiphertextIndist) :
     scheme.PerfectlySecret :=
   (perfectlySecret_iff_indep scheme).mpr (fun msgDist m c =>
     indep_of_ciphertextIndist scheme h msgDist m c)
 
 /-- Perfect secrecy implies ciphertext indistinguishability. -/
-theorem forward (scheme : EncScheme M K C)
+theorem ciphertextIndist_of_perfectlySecret (scheme : EncScheme M K C)
     (h : scheme.PerfectlySecret) :
-    ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁ := by
+    scheme.CiphertextIndist := by
   classical
   rw [perfectlySecret_iff_indep] at h
   intro m₀ m₁
@@ -140,14 +183,26 @@ theorem forward (scheme : EncScheme M K C)
     exact (ENNReal.mul_left_inj hm₁ hm₁_top).mp this
   exact h₀.trans h₁.symm
 
+/-- If each message maps to a key that encrypts it to a common ciphertext,
+then the key assignment is injective (by correctness of decryption). -/
+lemma encrypt_key_injective (scheme : EncScheme M K C)
+    (f : M → K) (c₀ : C)
+    (hf_mem : ∀ m, f m ∈ scheme.gen.support)
+    (hf_enc : ∀ m, c₀ ∈ (scheme.enc (f m) m).support) :
+    Function.Injective f :=
+  fun m₁ m₂ heq => by
+    have h₁ := scheme.correct _ (hf_mem m₁) m₁ c₀ (hf_enc m₁)
+    have h₂ := scheme.correct _ (hf_mem m₂) m₂ c₀ (hf_enc m₂)
+    rw [heq] at h₁; exact h₁.symm.trans h₂
+
 /-- Perfect secrecy requires `|K| ≥ |M|` (Shannon's theorem). -/
-theorem shannonKeySpace [Fintype M] [Fintype K]
+theorem shannonKeySpace [Finite M] [Finite K]
     (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
-    Fintype.card K ≥ Fintype.card M := by
+    Nat.card K ≥ Nat.card M := by
   classical
-  have hci := forward scheme h
+  have hci := ciphertextIndist_of_perfectlySecret scheme h
   by_cases hM : IsEmpty M
-  · simp [Fintype.card_eq_zero]
+  · simp
   · rw [not_isEmpty_iff] at hM
     obtain ⟨m₀⟩ := hM
     obtain ⟨c₀, hc₀⟩ := (scheme.ciphertextDist m₀).support_nonempty
@@ -156,9 +211,7 @@ theorem shannonKeySpace [Fintype M] [Fintype K]
       have : c₀ ∈ (scheme.ciphertextDist m).support := by rw [hci m m₀]; exact hc₀
       exact (PMF.mem_support_bind_iff _ _ _).mp this
     choose f hf_mem hf_enc using key_exists
-    exact Fintype.card_le_of_injective f fun m₁ m₂ heq => by
-      have h₁ := scheme.correct _ (hf_mem m₁) m₁ c₀ (hf_enc m₁)
-      have h₂ := scheme.correct _ (hf_mem m₂) m₂ c₀ (hf_enc m₂)
-      rw [heq] at h₁; exact h₁.symm.trans h₂
+    exact Nat.card_le_card_of_injective f
+      (encrypt_key_injective scheme f c₀ hf_mem hf_enc)
 
-end Cslib.Cryptography.PerfectSecrecy
+end Cslib.Crypto.PerfectSecrecy
diff --git a/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean b/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
new file mode 100644
index 00000000..c391b997
--- /dev/null
+++ b/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
@@ -0,0 +1,58 @@
+/-
+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.PerfectSecrecy.Basic
+public import Cslib.Crypto.PerfectSecrecy.Internal.OneTimePad
+public import Mathlib.Probability.Distributions.Uniform
+
+@[expose] public section
+
+/-!
+# One-Time Pad
+
+The one-time pad (Vernam cipher) over `BitVec l`
+([KatzLindell2020], Construction 2.9).
+
+## Main definitions
+
+- `Cslib.Crypto.PerfectSecrecy.otp`: the one-time pad encryption scheme
+
+## Main results
+
+- `Cslib.Crypto.PerfectSecrecy.otp_perfectlySecret`:
+  the one-time pad is perfectly secret ([KatzLindell2020], Theorem 2.10)
+
+## References
+
+* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
+-/
+
+namespace Cslib.Crypto.PerfectSecrecy
+
+/-- The one-time pad over `l`-bit strings. Encryption and decryption
+are XOR ([KatzLindell2020], Construction 2.9). -/
+noncomputable def otp (l : ℕ) :
+    EncScheme (BitVec l) (BitVec l) (BitVec l) where
+  gen := PMF.uniformOfFintype _
+  enc := fun k m => PMF.pure (k ^^^ m)
+  dec := fun k c => k ^^^ c
+  correct := by
+    intro k _ m c hc
+    rw [PMF.mem_support_pure_iff] at hc
+    subst hc
+    rw [← BitVec.xor_assoc, BitVec.xor_self, BitVec.zero_xor]
+
+/-- The one-time pad is perfectly secret ([KatzLindell2020], Theorem 2.10). -/
+theorem otp_perfectlySecret (l : ℕ) : (otp l).PerfectlySecret := by
+  rw [EncScheme.perfectlySecret_iff_ciphertextIndist]
+  intro m₀ m₁
+  simp only [EncScheme.ciphertextDist, otp]
+  exact (OTP.otp_ciphertextDist_eq_uniform l m₀).trans
+    (OTP.otp_ciphertextDist_eq_uniform l m₁).symm
+
+end Cslib.Crypto.PerfectSecrecy
diff --git a/Cslib/Cryptography/PerfectSecrecy.lean b/Cslib/Cryptography/PerfectSecrecy.lean
deleted file mode 100644
index a4c6e580..00000000
--- a/Cslib/Cryptography/PerfectSecrecy.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-/-
-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.Cryptography.PerfectSecrecy.Encryption
-public import Cslib.Cryptography.PerfectSecrecy.PerfectSecrecy
-public import Cslib.Cryptography.PerfectSecrecy.OneTimePad
diff --git a/Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean
deleted file mode 100644
index 832fb752..00000000
--- a/Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-/-
-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.Cryptography.PerfectSecrecy.OTP
-
-/-- The ciphertext distribution of the OTP is uniform, regardless of the message. -/
-theorem otp_ciphertextDist_eq_uniform (l : ℕ) (m : Fin l → Bool) :
-    (PMF.uniformOfFintype (Fin l → Bool)).bind
-      (fun k => PMF.pure (fun i => k i ^^ m i)) =
-    PMF.uniformOfFintype (Fin l → Bool) := by
-  ext c
-  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, PMF.pure_apply]
-  have heq : ∀ a : Fin l → Bool,
-      (c = fun i => a i ^^ m i) ↔ (a = fun i => c i ^^ m i) :=
-    fun a => ⟨fun h => funext fun i => by have := congr_fun h i; simp_all,
-              fun h => funext fun i => by have := congr_fun h i; simp_all⟩
-  simp_rw [heq]
-  simp
-
-end Cslib.Cryptography.PerfectSecrecy.OTP
diff --git a/Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean b/Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean
deleted file mode 100644
index b1bd1ea5..00000000
--- a/Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean
+++ /dev/null
@@ -1,53 +0,0 @@
-/-
-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.Cryptography.PerfectSecrecy.PerfectSecrecy
-public import Cslib.Cryptography.PerfectSecrecy.Internal.OneTimePad
-public import Mathlib.Probability.Distributions.Uniform
-
-@[expose] public section
-
-/-!
-# One-Time Pad
-
-The one-time pad (Vernam cipher) over `{0,1}^l`
-([KatzLindell2021], Construction 2.9).
-
-## Main definitions
-
-- `Cslib.Cryptography.PerfectSecrecy.otp`: the one-time pad encryption scheme
-
-## Main results
-
-- `Cslib.Cryptography.PerfectSecrecy.otp_perfectlySecret`:
-  the one-time pad is perfectly secret ([KatzLindell2021], Theorem 2.10)
-
-## References
-
-* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2021]
--/
-
-namespace Cslib.Cryptography.PerfectSecrecy
-
-/-- The one-time pad over `l`-bit strings. Encryption and decryption
-are pointwise XOR ([KatzLindell2021], Construction 2.9). -/
-noncomputable def otp (l : ℕ) : EncScheme (Fin l → Bool) (Fin l → Bool) (Fin l → Bool) where
-  gen := PMF.uniformOfFintype _
-  enc := fun k m => PMF.pure (fun i => k i ^^ m i)
-  dec := fun k c => fun i => k i ^^ c i
-  correct := by intro k _ m c hc; simp at hc; simp [hc]
-
-/-- The one-time pad is perfectly secret ([KatzLindell2021], Theorem 2.10). -/
-theorem otp_perfectlySecret (l : ℕ) : (otp l).PerfectlySecret := by
-  rw [EncScheme.perfectlySecret_iff_ciphertextIndist]
-  intro m₀ m₁
-  simp only [EncScheme.ciphertextDist, otp]
-  exact (OTP.otp_ciphertextDist_eq_uniform l m₀).trans
-    (OTP.otp_ciphertextDist_eq_uniform l m₁).symm
-
-end Cslib.Cryptography.PerfectSecrecy
diff --git a/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean b/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean
deleted file mode 100644
index faa7aa0a..00000000
--- a/Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-/-
-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.Cryptography.PerfectSecrecy.PerfectSecrecy.Defs
-public import Cslib.Cryptography.PerfectSecrecy.Internal.PerfectSecrecy
-
-@[expose] public section
-
-/-!
-# Perfect Secrecy
-
-Characterisation theorems for perfect secrecy following
-[KatzLindell2021], Chapter 2.
-
-## Main results
-
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme.perfectlySecret_iff_ciphertextIndist`:
-  ciphertext indistinguishability characterization ([KatzLindell2021], Lemma 2.5)
-- `Cslib.Cryptography.PerfectSecrecy.EncScheme.perfectlySecret_keySpace_ge`:
-  Shannon's theorem, `|K| ≥ |M|` ([KatzLindell2021], Theorem 2.12)
-
-## References
-
-* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2021]
--/
-
-namespace Cslib.Cryptography.PerfectSecrecy.EncScheme
-
-universe u
-variable {M K C : Type u}
-
-/-- A scheme is perfectly secret iff the ciphertext distribution is
-independent of the plaintext ([KatzLindell2021], Lemma 2.5). -/
-theorem perfectlySecret_iff_ciphertextIndist (scheme : EncScheme M K C) :
-    scheme.PerfectlySecret ↔
-    ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁ :=
-  ⟨PerfectSecrecy.forward scheme, PerfectSecrecy.backward scheme⟩
-
-/-- Perfect secrecy requires `|K| ≥ |M|`
-([KatzLindell2021], Theorem 2.12). -/
-theorem perfectlySecret_keySpace_ge [Fintype M] [Fintype K]
-    (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
-    Fintype.card K ≥ Fintype.card M :=
-  PerfectSecrecy.shannonKeySpace scheme h
-
-end Cslib.Cryptography.PerfectSecrecy.EncScheme
diff --git a/references.bib b/references.bib
index edb111f4..1f108c99 100644
--- a/references.bib
+++ b/references.bib
@@ -123,6 +123,16 @@ @article{         Hennessy1985
   bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
+@book{             KatzLindell2020,
+  author       = {Jonathan Katz and
+                  Yehuda Lindell},
+  title        = {Introduction to Modern Cryptography},
+  edition      = {3rd},
+  publisher    = {CRC Press},
+  year         = {2020},
+  isbn         = {9780815354369}
+}
+
 @inproceedings{   Kiselyov2015,
   author    = {Kiselyov, Oleg and Ishii, Hiromi},
   title     = {Freer Monads, More Extensible Effects},

From b091bc2f5c4bb15b270c210fef43c97cef8d4e50 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Wed, 1 Apr 2026 15:21:32 -0400
Subject: [PATCH 3/3] fix: drop unused Finite M, replace orphan BitVec Fintype
 instance

- Remove unused `[Finite M]` from `shannonKeySpace` /
  `perfectlySecret_keySpace_ge` (caught by unusedArguments linter).
- Replace orphan `Fintype (BitVec n)` instance with a named
  `@[reducible] def bitVecFintype`, used locally via `haveI`.
---
 Cslib/Crypto/PerfectSecrecy/Basic.lean        |  2 +-
 .../PerfectSecrecy/Internal/OneTimePad.lean   |  4 +++-
 .../Internal/PerfectSecrecy.lean              |  2 +-
 Cslib/Crypto/PerfectSecrecy/OneTimePad.lean   | 19 ++++++++++---------
 4 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/Cslib/Crypto/PerfectSecrecy/Basic.lean b/Cslib/Crypto/PerfectSecrecy/Basic.lean
index 03603e97..1ecd01b5 100644
--- a/Cslib/Crypto/PerfectSecrecy/Basic.lean
+++ b/Cslib/Crypto/PerfectSecrecy/Basic.lean
@@ -45,7 +45,7 @@ theorem perfectlySecret_iff_ciphertextIndist (scheme : EncScheme M K C) :
 
 /-- Perfect secrecy requires `|K| ≥ |M|`
 ([KatzLindell2020], Theorem 2.12). -/
-theorem perfectlySecret_keySpace_ge [Finite M] [Finite K]
+theorem perfectlySecret_keySpace_ge [Finite K]
     (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
     Nat.card K ≥ Nat.card M :=
   PerfectSecrecy.shannonKeySpace scheme h
diff --git a/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
index b82df67d..e5438627 100644
--- a/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
+++ b/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
@@ -19,7 +19,7 @@ The OTP ciphertext distribution is uniform regardless of message.
 
 namespace Cslib.Crypto.PerfectSecrecy.OTP
 
-noncomputable instance (n : ℕ) : Fintype (BitVec n) :=
+@[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⟩
 
@@ -34,9 +34,11 @@ lemma xor_right_eq_iff {l : ℕ} (c m k : BitVec l) :
 
 /-- 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
+  haveI := bitVecFintype l
   ext c
   simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, PMF.pure_apply]
   simp_rw [xor_right_eq_iff c m]
diff --git a/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
index 0d7e012f..65200980 100644
--- a/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
+++ b/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
@@ -196,7 +196,7 @@ lemma encrypt_key_injective (scheme : EncScheme M K C)
     rw [heq] at h₁; exact h₁.symm.trans h₂
 
 /-- Perfect secrecy requires `|K| ≥ |M|` (Shannon's theorem). -/
-theorem shannonKeySpace [Finite M] [Finite K]
+theorem shannonKeySpace [Finite K]
     (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
     Nat.card K ≥ Nat.card M := by
   classical
diff --git a/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean b/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
index c391b997..856db144 100644
--- a/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
+++ b/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
@@ -37,15 +37,16 @@ namespace Cslib.Crypto.PerfectSecrecy
 /-- The one-time pad over `l`-bit strings. Encryption and decryption
 are XOR ([KatzLindell2020], Construction 2.9). -/
 noncomputable def otp (l : ℕ) :
-    EncScheme (BitVec l) (BitVec l) (BitVec l) where
-  gen := PMF.uniformOfFintype _
-  enc := fun k m => PMF.pure (k ^^^ m)
-  dec := fun k c => k ^^^ c
-  correct := by
-    intro k _ m c hc
-    rw [PMF.mem_support_pure_iff] at hc
-    subst hc
-    rw [← BitVec.xor_assoc, BitVec.xor_self, BitVec.zero_xor]
+    EncScheme (BitVec l) (BitVec l) (BitVec l) :=
+  haveI := OTP.bitVecFintype l
+  { gen := PMF.uniformOfFintype _
+    enc := fun k m => PMF.pure (k ^^^ m)
+    dec := fun k c => k ^^^ c
+    correct := by
+      intro k _ m c hc
+      rw [PMF.mem_support_pure_iff] at hc
+      subst hc
+      rw [← BitVec.xor_assoc, BitVec.xor_self, BitVec.zero_xor] }
 
 /-- The one-time pad is perfectly secret ([KatzLindell2020], Theorem 2.10). -/
 theorem otp_perfectlySecret (l : ℕ) : (otp l).PerfectlySecret := by