diff --git a/Cslib.lean b/Cslib.lean
index a621d6e1..30d3fe1c 100644
--- a/Cslib.lean
+++ b/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.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..1ecd01b5
--- /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 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/Crypto/PerfectSecrecy/Defs.lean b/Cslib/Crypto/PerfectSecrecy/Defs.lean
new file mode 100644
index 00000000..c02a724e
--- /dev/null
+++ b/Cslib/Crypto/PerfectSecrecy/Defs.lean
@@ -0,0 +1,77 @@
+/-
+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.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.PerfectSecrecy.EncScheme.ciphertextDist`:
+  ciphertext distribution for a given message
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.jointDist`:
+  joint (message, ciphertext) distribution given a message prior
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.marginalCiphertextDist`:
+  marginal ciphertext distribution given a message prior
+- `Cslib.Crypto.PerfectSecrecy.EncScheme.posteriorMsgProb`:
+  posterior probability `Pr[M = m | C = c]`
+- `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.Crypto.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
+([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.PerfectSecrecy.EncScheme
diff --git a/Cslib/Crypto/PerfectSecrecy/Encryption.lean b/Cslib/Crypto/PerfectSecrecy/Encryption.lean
new file mode 100644
index 00000000..248f6cc9
--- /dev/null
+++ b/Cslib/Crypto/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.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.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.PerfectSecrecy
diff --git a/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
new file mode 100644
index 00000000..e5438627
--- /dev/null
+++ b/Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean
@@ -0,0 +1,47 @@
+/-
+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
+
+@[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⟩
+
+/-- 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) :
+    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]
+  simp
+
+end Cslib.Crypto.PerfectSecrecy.OTP
diff --git a/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
new file mode 100644
index 00000000..65200980
--- /dev/null
+++ b/Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean
@@ -0,0 +1,217 @@
+/-
+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 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
+  ([KatzLindell2020], Lemma 2.5)
+- Shannon's key-space bound ([KatzLindell2020], Theorem 2.12)
+-/
+
+namespace Cslib.Crypto.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]
+
+/-- 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),
+      scheme.jointDist msgDist (m, c) =
+        msgDist m * scheme.marginalCiphertextDist msgDist c := by
+  constructor
+  · intro h msgDist m c
+    classical
+    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, ENNReal.div_mul_cancel hc hne_top]
+  · intro h msgDist m c hc
+    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 : scheme.CiphertextIndist)
+    (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 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 ciphertextIndist_of_perfectlySecret (scheme : EncScheme M K C)
+    (h : scheme.PerfectlySecret) :
+    scheme.CiphertextIndist := 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
+
+/-- 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 [Finite K]
+    (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
+    Nat.card K ≥ Nat.card M := by
+  classical
+  have hci := ciphertextIndist_of_perfectlySecret scheme h
+  by_cases hM : IsEmpty M
+  · simp
+  · 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 Nat.card_le_card_of_injective f
+      (encrypt_key_injective scheme f c₀ hf_mem hf_enc)
+
+end Cslib.Crypto.PerfectSecrecy
diff --git a/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean b/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
new file mode 100644
index 00000000..856db144
--- /dev/null
+++ b/Cslib/Crypto/PerfectSecrecy/OneTimePad.lean
@@ -0,0 +1,59 @@
+/-
+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) :=
+  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
+  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/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},