Skip to content

Commit 906574d

Browse files
SamuelSchlesingerSamuelSchlesinger
authored
feat(Cryptography): formalise perfect secrecy and the one-time pad (#464)
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) For some context, Katz reviewed this in its original home: SamuelSchlesinger/introduction-to-modern-cryptography#1.
1 parent d3a9006 commit 906574d

9 files changed

Lines changed: 523 additions & 0 deletions

File tree

‎Cslib.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,13 @@ public import Cslib.Computability.URM.Defs
3636
public import Cslib.Computability.URM.Execution
3737
public import Cslib.Computability.URM.StandardForm
3838
public import Cslib.Computability.URM.StraightLine
39+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic
40+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
41+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
42+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad
43+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy
44+
public import Cslib.Crypto.Protocols.PerfectSecrecy.OneTimePad
45+
public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities
3946
public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
4047
public import Cslib.Foundations.Control.Monad.Free
4148
public import Cslib.Foundations.Control.Monad.Free.Effects

‎Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
/-
2+
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Samuel Schlesinger
5+
-/
6+
7+
module
8+
9+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
10+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy
11+
12+
@[expose] public section
13+
14+
/-!
15+
# Perfect Secrecy
16+
17+
Characterisation theorems for perfect secrecy following
18+
[KatzLindell2020], Chapter 2.
19+
20+
## Main results
21+
22+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_iff_ciphertextIndist`:
23+
ciphertext indistinguishability characterization ([KatzLindell2020], Lemma 2.5)
24+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_keySpace_ge`:
25+
Shannon's theorem, `|K| ≥ |M|` ([KatzLindell2020], Theorem 2.12)
26+
27+
## References
28+
29+
* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
30+
-/
31+
32+
namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme
33+
34+
universe u
35+
variable {M K C : Type u}
36+
37+
/-- A scheme is perfectly secret iff the ciphertext distribution is
38+
independent of the plaintext ([KatzLindell2020], Lemma 2.5). -/
39+
theorem perfectlySecret_iff_ciphertextIndist (scheme : EncScheme M K C) :
40+
scheme.PerfectlySecret ↔ scheme.CiphertextIndist :=
41+
⟨PerfectSecrecy.ciphertextIndist_of_perfectlySecret scheme,
42+
PerfectSecrecy.perfectlySecret_of_ciphertextIndist scheme⟩
43+
44+
/-- Perfect secrecy requires `|K| ≥ |M|`
45+
([KatzLindell2020], Theorem 2.12). -/
46+
theorem perfectlySecret_keySpace_ge [Finite K]
47+
(scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
48+
Nat.card K ≥ Nat.card M :=
49+
PerfectSecrecy.shannonKeySpace scheme h
50+
51+
end Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme

‎Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
/-
2+
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Samuel Schlesinger
5+
-/
6+
7+
module
8+
9+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
10+
public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities
11+
public import Mathlib.Probability.ProbabilityMassFunction.Constructions
12+
13+
@[expose] public section
14+
15+
/-!
16+
# Perfect Secrecy: Definitions
17+
18+
Core definitions for perfect secrecy following [KatzLindell2020], Chapter 2.
19+
20+
## Main definitions
21+
22+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.ciphertextDist`:
23+
ciphertext distribution for a given message
24+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.jointDist`:
25+
joint (message, ciphertext) distribution given a message prior
26+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.marginalCiphertextDist`:
27+
marginal ciphertext distribution given a message prior
28+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgDist`:
29+
posterior message distribution `Pr[M | C = c]` as a `PMF`
30+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.PerfectlySecret`:
31+
perfect secrecy ([KatzLindell2020], Definition 2.3)
32+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.CiphertextIndist`:
33+
ciphertext indistinguishability ([KatzLindell2020], Lemma 2.5)
34+
-/
35+
36+
namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme
37+
38+
universe u
39+
variable {M K C : Type u}
40+
41+
/-- The distribution of `Enc_K(m)` when `K ← Gen`. -/
42+
noncomputable def ciphertextDist (scheme : EncScheme M K C) (m : M) : PMF C := do
43+
scheme.enc (← scheme.gen) m
44+
45+
/-- Joint distribution of `(M, C)` given a message prior. -/
46+
noncomputable def jointDist (scheme : EncScheme M K C) (msgDist : PMF M) : PMF (M × C) := do
47+
let m ← msgDist
48+
return (m, ← scheme.ciphertextDist m)
49+
50+
/-- Marginal ciphertext distribution given a message prior. -/
51+
noncomputable def marginalCiphertextDist (scheme : EncScheme M K C)
52+
(msgDist : PMF M) : PMF C := do
53+
scheme.ciphertextDist (← msgDist)
54+
55+
/-- The posterior message distribution `Pr[M | C = c]` as a probability
56+
distribution, given a message prior and a ciphertext in the support of
57+
the marginal distribution. -/
58+
noncomputable def posteriorMsgDist (scheme : EncScheme M K C)
59+
(msgDist : PMF M) (c : C)
60+
(hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) : PMF M :=
61+
PMFUtilities.posteriorDist msgDist scheme.ciphertextDist c hc
62+
63+
@[simp]
64+
theorem posteriorMsgDist_apply (scheme : EncScheme M K C)
65+
(msgDist : PMF M) (c : C)
66+
(hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) (m : M) :
67+
scheme.posteriorMsgDist msgDist c hc m =
68+
scheme.jointDist msgDist (m, c) / scheme.marginalCiphertextDist msgDist c :=
69+
rfl
70+
71+
/-- An encryption scheme is perfectly secret if the posterior message
72+
distribution equals the prior for every ciphertext with positive probability
73+
([KatzLindell2020], Definition 2.3). -/
74+
def PerfectlySecret (scheme : EncScheme M K C) : Prop :=
75+
∀ (msgDist : PMF M) (c : C)
76+
(hc : c ∈ (scheme.marginalCiphertextDist msgDist).support),
77+
scheme.posteriorMsgDist msgDist c hc = msgDist
78+
79+
/-- Ciphertext indistinguishability: the ciphertext distribution is the same
80+
for all messages ([KatzLindell2020], Lemma 2.5). -/
81+
def CiphertextIndist (scheme : EncScheme M K C) : Prop :=
82+
∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁
83+
84+
end Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme

‎Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/-
2+
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Samuel Schlesinger
5+
-/
6+
7+
module
8+
9+
public import Cslib.Init
10+
public import Mathlib.Probability.ProbabilityMassFunction.Monad
11+
12+
@[expose] public section
13+
14+
/-!
15+
# Private-Key Encryption Schemes (Information-Theoretic)
16+
17+
An information-theoretic private-key encryption scheme following
18+
[KatzLindell2020], Definition 2.1. Key generation and encryption are
19+
probability distributions over arbitrary types, with no computational
20+
constraints.
21+
22+
## Main definitions
23+
24+
- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme`:
25+
a private-key encryption scheme (Gen, Enc, Dec) with correctness
26+
27+
## References
28+
29+
* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020]
30+
-/
31+
32+
namespace Cslib.Crypto.Protocols.PerfectSecrecy
33+
34+
/--
35+
A private-key encryption scheme over message space `M`, key space `K`,
36+
and ciphertext space `C` ([KatzLindell2020], Definition 2.1).
37+
-/
38+
structure EncScheme (Message Key Ciphertext : Type*) where
39+
/-- Probabilistic key generation. -/
40+
gen : PMF Key
41+
/-- (Possibly randomized) encryption. -/
42+
enc (key : Key) (message : Message) : PMF Ciphertext
43+
/-- Deterministic decryption. -/
44+
dec (key : Key) (ciphertext : Ciphertext) : Message
45+
/-- Decryption inverts encryption for all keys in the support of `gen`. -/
46+
correct : ∀ key, key ∈ gen.support → ∀ message ciphertext,
47+
ciphertext ∈ (enc key message).support → dec key ciphertext = message
48+
49+
/-- Build an encryption scheme from deterministic pure encryption/decryption
50+
where decryption is a left inverse of encryption for every key. -/
51+
noncomputable def EncScheme.ofPure.{u} {Message Key Ciphertext : Type u} (gen : PMF Key)
52+
(enc : Key → Message → Ciphertext) (dec : Key → Ciphertext → Message)
53+
(h : ∀ key, Function.LeftInverse (dec key) (enc key)) :
54+
EncScheme Message Key Ciphertext where
55+
gen := gen
56+
enc key message := PMF.pure (enc key message)
57+
dec := dec
58+
correct key _ message _ hc := by
59+
rw [PMF.mem_support_pure_iff] at hc; subst hc; exact h key message
60+
61+
end Cslib.Crypto.Protocols.PerfectSecrecy

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

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
/-
2+
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Samuel Schlesinger
5+
-/
6+
7+
module
8+
9+
public import Cslib.Init
10+
public import Mathlib.Probability.Distributions.Uniform
11+
12+
@[expose] public section
13+
14+
/-!
15+
# One-Time Pad: Internal proofs
16+
17+
The OTP ciphertext distribution is uniform regardless of message.
18+
-/
19+
20+
namespace Cslib.Crypto.Protocols.PerfectSecrecy.OTP
21+
22+
-- TODO: upstream to Mathlib as a FinEnum instance for BitVec.
23+
instance bitVecFintype (n : ℕ) : Fintype (BitVec n) :=
24+
Fintype.ofEquiv (Fin (2 ^ n))
25+
⟨BitVec.ofFin, BitVec.toFin, fun x => by simp, fun x => by simp⟩
26+
27+
-- TODO: upstream to Mathlib — general BitVec XOR cancellation lemma.
28+
/-- XOR by a fixed mask is self-inverse on `BitVec`: `c = k ^^^ m ↔ c ^^^ m = k`. -/
29+
lemma eq_xor_iff_xor_eq {l : ℕ} (c m k : BitVec l) :
30+
(c = k ^^^ m) ↔ (c ^^^ m = k) := by grind
31+
32+
/-- The ciphertext distribution of the OTP is uniform, regardless of the message. -/
33+
theorem otp_ciphertextDist_eq_uniform (l : ℕ) (m : BitVec l) :
34+
(PMF.uniformOfFintype (BitVec l)).bind
35+
(fun k => PMF.pure (k ^^^ m)) =
36+
PMF.uniformOfFintype (BitVec l) := by simp [PMF.ext_iff, eq_xor_iff_xor_eq]
37+
38+
end Cslib.Crypto.Protocols.PerfectSecrecy.OTP

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

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
/-
2+
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Samuel Schlesinger
5+
-/
6+
7+
module
8+
9+
public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
10+
public import Mathlib.Probability.Distributions.Uniform
11+
12+
@[expose] public section
13+
14+
/-!
15+
# Perfect Secrecy: Internal proofs
16+
17+
Auxiliary lemmas for perfect secrecy:
18+
- Equivalence of the conditional-probability and independence formulations
19+
- Both directions of the ciphertext indistinguishability characterization
20+
([KatzLindell2020], Lemma 2.5)
21+
- Shannon's key-space bound ([KatzLindell2020], Theorem 2.12)
22+
-/
23+
24+
namespace Cslib.Crypto.Protocols.PerfectSecrecy
25+
26+
open PMF ENNReal
27+
28+
universe u
29+
variable {M K C : Type u}
30+
31+
/-- The joint distribution at `(m, c)` equals `msgDist m * ciphertextDist m c`. -/
32+
theorem jointDist_eq (scheme : EncScheme M K C) (msgDist : PMF M)
33+
(m : M) (c : C) :
34+
scheme.jointDist msgDist (m, c) = msgDist m * scheme.ciphertextDist m c :=
35+
PMFUtilities.bind_pair_apply msgDist scheme.ciphertextDist m c
36+
37+
/-- Summing the joint distribution over messages gives the marginal ciphertext distribution. -/
38+
theorem jointDist_tsum_fst (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) :
39+
∑' m, scheme.jointDist msgDist (m, c) = scheme.marginalCiphertextDist msgDist c :=
40+
PMFUtilities.bind_pair_tsum_fst msgDist scheme.ciphertextDist c
41+
42+
/-- Perfect secrecy is equivalent to message-ciphertext independence.
43+
The two formulations are related by multiplying/dividing by `marginal(c)`. -/
44+
theorem perfectlySecret_iff_indep (scheme : EncScheme M K C) :
45+
scheme.PerfectlySecret ↔
46+
∀ (msgDist : PMF M) (m : M) (c : C),
47+
scheme.jointDist msgDist (m, c) =
48+
msgDist m * scheme.marginalCiphertextDist msgDist c := by
49+
constructor
50+
· intro h msgDist m c
51+
by_cases hc : (scheme.marginalCiphertextDist msgDist) c = 0
52+
· have := ENNReal.tsum_eq_zero.mp
53+
((jointDist_tsum_fst scheme msgDist c).trans hc) m
54+
rw [this, hc, mul_zero]
55+
· have hne_top := ne_top_of_le_ne_top one_ne_top
56+
(PMF.coe_le_one (scheme.marginalCiphertextDist msgDist) c)
57+
have := DFunLike.congr_fun (h msgDist c ((PMF.mem_support_iff _ _).mpr hc)) m
58+
simp only [EncScheme.posteriorMsgDist_apply] at this
59+
rw [← this, ENNReal.div_mul_cancel hc hne_top]
60+
· intro h msgDist c hc; ext m
61+
simp only [EncScheme.posteriorMsgDist_apply]
62+
rw [h msgDist m c, ENNReal.mul_div_cancel_right
63+
((PMF.mem_support_iff _ _).mp hc)
64+
(ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one _ c))]
65+
66+
/-- Ciphertext indistinguishability implies message-ciphertext independence. -/
67+
theorem indep_of_ciphertextIndist (scheme : EncScheme M K C)
68+
(h : scheme.CiphertextIndist)
69+
(msgDist : PMF M) (m : M) (c : C) :
70+
scheme.jointDist msgDist (m, c) =
71+
msgDist m * scheme.marginalCiphertextDist msgDist c := by
72+
rw [jointDist_eq]; congr 1
73+
change scheme.ciphertextDist m c =
74+
PMF.bind msgDist (fun m' => scheme.ciphertextDist m') c
75+
rw [PMF.bind_apply]
76+
conv_rhs => arg 1; ext m'; rw [h m' m]
77+
rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul]
78+
79+
/-- Ciphertext indistinguishability implies perfect secrecy. -/
80+
theorem perfectlySecret_of_ciphertextIndist (scheme : EncScheme M K C)
81+
(h : scheme.CiphertextIndist) :
82+
scheme.PerfectlySecret :=
83+
(perfectlySecret_iff_indep scheme).mpr (fun msgDist m c =>
84+
indep_of_ciphertextIndist scheme h msgDist m c)
85+
86+
/-- Perfect secrecy implies ciphertext indistinguishability. -/
87+
theorem ciphertextIndist_of_perfectlySecret (scheme : EncScheme M K C)
88+
(h : scheme.PerfectlySecret) :
89+
scheme.CiphertextIndist := by
90+
classical
91+
rw [perfectlySecret_iff_indep] at h
92+
intro m₀ m₁; ext c
93+
have hs : ({m₀, m₁} : Finset M).Nonempty := ⟨m₀, Finset.mem_insert_self ..⟩
94+
set μ := PMF.uniformOfFinset _ hs
95+
suffices key : ∀ m ∈ ({m₀, m₁} : Finset M),
96+
scheme.ciphertextDist m c = scheme.marginalCiphertextDist μ c by
97+
exact (key m₀ (by simp)).trans (key m₁ (by simp)).symm
98+
intro m hm
99+
have hne := (PMF.mem_support_uniformOfFinset_iff hs m).mpr hm
100+
have hne_top := ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one μ m)
101+
exact (ENNReal.mul_right_inj hne hne_top).mp (by rw [← jointDist_eq]; exact h μ m c)
102+
103+
/-- If each message maps to a key that encrypts it to a common ciphertext,
104+
then the key assignment is injective (by correctness of decryption). -/
105+
lemma encrypt_key_injective (scheme : EncScheme M K C)
106+
(f : M → K) (c₀ : C)
107+
(hf_mem : ∀ m, f m ∈ scheme.gen.support)
108+
(hf_enc : ∀ m, c₀ ∈ (scheme.enc (f m) m).support) :
109+
Function.Injective f :=
110+
fun m₁ m₂ heq =>
111+
(scheme.correct _ (hf_mem m₁) m₁ c₀ (hf_enc m₁)).symm.trans
112+
(heq ▸ scheme.correct _ (hf_mem m₂) m₂ c₀ (hf_enc m₂))
113+
114+
/-- Perfect secrecy requires `|K| ≥ |M|` (Shannon's theorem). -/
115+
theorem shannonKeySpace [Finite K]
116+
(scheme : EncScheme M K C) (h : scheme.PerfectlySecret) :
117+
Nat.card K ≥ Nat.card M := by
118+
classical
119+
have hci := ciphertextIndist_of_perfectlySecret scheme h
120+
by_cases hM : IsEmpty M; · simp
121+
obtain ⟨m₀⟩ := not_isEmpty_iff.mp hM
122+
obtain ⟨c₀, hc₀⟩ := (scheme.ciphertextDist m₀).support_nonempty
123+
have key_exists : ∀ m, ∃ k ∈ scheme.gen.support, c₀ ∈ (scheme.enc k m).support := by
124+
intro m
125+
exact (PMF.mem_support_bind_iff _ _ _).mp
126+
(show c₀ ∈ (scheme.ciphertextDist m).support by rw [hci m m₀]; exact hc₀)
127+
choose f hf_mem hf_enc using key_exists
128+
exact Nat.card_le_card_of_injective f
129+
(encrypt_key_injective scheme f c₀ hf_mem hf_enc)
130+
131+
end Cslib.Crypto.Protocols.PerfectSecrecy

0 commit comments

Comments
 (0)