feat(Cryptography): formalise perfect secrecy and the one-time pad by SamuelSchlesinger · Pull Request #464 · leanprover/cslib

SamuelSchlesinger · 2026-04-01T14:12:10Z

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.

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)

SamuelSchlesinger · 2026-04-01T14:13:54Z

I'd be quite interested in helping with future review in this Cryptography folder, if there is interest in including it.

Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean

linesthatinterlace · 2026-04-01T14:39:08Z

Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean

+    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,


This should probably be a lemma of some kind (might be easier in BitVec, not sure).

linesthatinterlace · 2026-04-01T14:40:38Z

Cslib/Crypto/PerfectSecrecy/Encryption.lean

+-/
+structure EncScheme.{u} (M K C : Type u) where
+  /-- Probabilistic key generation. -/
+  gen : PMF K


We have briefly spoken about this, but it is worth considering whether rational probabilities might be desirable. The concern would be that sometimes you do want to be able to take limits of probabilities etc.

I think given that this is really not going to be reused very much (the rest of the book defined encryption schemes totally differently), I feel we shouldn't define a custom notion of rational distributions just for this.

That said, I am very open to computable probability distributions being defined somewhere if they're going to be useful broadly.

linesthatinterlace · 2026-04-01T14:42:45Z

Cslib/Crypto/PerfectSecrecy/Encryption.lean

+  /-- 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


This looks like the right statement of correctness to me. I wonder if "gen.support" (the set of valid keys) and (enc k m),support (the set of valid encryptions for a give k) want names/definitions (or at least abbreviations).

To me, support feels like the right phrasing, but I am open to suggestions.

linesthatinterlace · 2026-04-01T14:45:03Z

Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean

+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₁ :=


This seems sensible to me and must be a pattern that occurs elsewhere.

linesthatinterlace · 2026-04-01T14:49:46Z

Cslib/Crypto/PerfectSecrecy/Defs.lean

+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


This is very nearly equivalent to:
∀ (msgDist : PMF M) (c : C),
c ∈ (scheme.marginalCiphertextDist msgDist).support →
scheme.posteriorMsgProb msgDist c = msgDist

The issue is that the types don't match. But I think scheme.posteriorMsgProb msgDist c is a distribution!

linesthatinterlace · 2026-04-01T14:53:59Z

Cslib/Crypto/PerfectSecrecy/Defs.lean

+
+/-- Posterior probability `Pr[M = m | C = c]`. -/
+noncomputable def posteriorMsgProb (scheme : EncScheme M K C)
+    (msgDist : PMF M) (c : C) (m : M) : ENNReal :=


I think scheme.posteriorMsgProb msgDist c is a distribution. It would be good to define it in these terms. It will require a little proof (but do we not already have this in Mathlib? Maybe not).

linesthatinterlace · 2026-04-01T15:00:33Z

Cslib/Cryptography/PerfectSecrecy/OneTimePad.lean

+
+/-- 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


I like this. However I do want to suggest that you could do this a different way - one could start with the (uniform) bernoulli distribution on Bool and show the most trivial case (when l = 1). Then maybe there's a way to meaningfully take the "product". Thought I'm not sure the concept of a product of an encryption scheme exists in the literature (I would argue it's perfectly sensible though).

linesthatinterlace · 2026-04-01T15:02:28Z

Cslib/Crypto/PerfectSecrecy/Internal/PerfectSecrecy.lean

+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)


I really do feel this ought to be in Mathlib (sans the encryption context) because I can't see that anything here uses the particular properties of the encryption scheme?

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean

linesthatinterlace · 2026-04-01T15:05:23Z

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean

+  rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul]
+
+/-- Ciphertext indistinguishability implies perfect secrecy. -/
+theorem backward (scheme : EncScheme M K C)


Not a good theorem name.

linesthatinterlace · 2026-04-01T15:06:34Z

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean

+/-- 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


Might be true with Nat.card?

linesthatinterlace · 2026-04-01T15:07:55Z

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean

+      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


I see an injectivity proof in a theorem, I think it should be a lemma (even if it is on the choice here).

linesthatinterlace

In general I think this is a good start on this stuff. My concern right now is about theorem organization and structure (including naming), and about whether any of the results you've proved should be Mathlib results or at least separated out (i.e. they are not really results about cryptographic concepts specifically).

SamuelSchlesinger · 2026-04-01T15:48:15Z

In general I think this is a good start on this stuff. My concern right now is about theorem organization and structure (including naming), and about whether any of the results you've proved should be Mathlib results or at least separated out (i.e. they are not really results about cryptographic concepts specifically).

Thanks for the feedback! I'll work on a follow up commit today that addresses each of these concerns. Re: Mathlib results, not totally sure how to approach it, I'll wait for more advice there.

fmontesi · 2026-04-01T16:23:53Z

Regarding the directory name, is it open also to cryptology stuff in the future? If so, we could consider calling it simply 'Crypto'.

SamuelSchlesinger · 2026-04-01T16:34:46Z

Regarding the directory name, is it open also to cryptology stuff in the future? If so, we could consider calling it simply 'Crypto'.

Great idea. I was actually considering adding some of the ciphers from the first chapter of the book originally, that could be fun to have around pedagogically.

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean

fmontesi · 2026-04-01T16:55:55Z

Cslib/Crypto/PerfectSecrecy/Defs.lean

Double directory name?

fmontesi · 2026-04-01T16:59:40Z

Cslib/Cryptography/PerfectSecrecy/PerfectSecrecy.lean

PerfectSecrecy is used a lot as directory and file name. :-)
Here it looks a bit generic. Could this be called something else?

Yes, I'll fix that similarly to the double directory name. Comes from the copy-paste from the previous home.

fmontesi · 2026-04-01T17:00:35Z

Cslib/Cryptography/PerfectSecrecy.lean

What's the purpose of this file?

Another copy-paste overlook, will reorganize.

Ah no its not, its intentional. Its where we re-export all of these things from. I will add a doc comment.

I think it should just be removed completely, we avoid this pattern in general.

Sounds good to me.

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

SamuelSchlesinger · 2026-04-01T18:49:38Z

I believe all the current feedback should be addressed now, let me know if there are more nits or issues.

linesthatinterlace · 2026-04-01T18:55:01Z

Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean

+
+namespace Cslib.Crypto.PerfectSecrecy.OTP
+
+noncomputable instance (n : ℕ) : Fintype (BitVec n) :=


No point having a Fintype instance be non-computable. Surprised this even needs to be. I would suggest actually FinEnum is most suitable here - and that could probably be added in Mathlib.

Ah oops I was meaning to remove this before pushing. I'm nearly sure this is an unnecessary orphan, I bet its somewhere on Mathlib.

Huh, it doesn't seem to be upstream AFAICT. I think you're right that we should upstream this as a FinEnum instance.

I'm going to try to sidestep the need for it for now.

I'm not following the details here, but if you need an instance that should eventually be upstreamed, this is fine to have in CSLib. We just ask that you leave a TODO comment. (There's an action configured that opens issues for these with links to the source code.)

Couldn't quite sidestep it, but at least made it local.

linesthatinterlace · 2026-04-01T18:56:47Z

Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean

+
+/-- 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


I think there's a special tactic to discharge bitvec goals. Ask around (I am not sure). This should definitely be upstream.

Oh neat. I can grep around in Mathlib for it.

bv_decide doesn't seem to work, if that's what you meant

- 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`.

linesthatinterlace · 2026-04-01T19:32:33Z

Cslib/Crypto/PerfectSecrecy/Internal/OneTimePad.lean

+    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) :


module public import Cslib.Init public import Mathlib.Probability.Distributions.Uniform public import Mathlib.Data.BitVec @[expose] public section /-! # One-Time Pad: Internal proofs The OTP ciphertext distribution is uniform regardless of message. -/ namespace Cslib.Crypto.PerfectSecrecy.OTP instance (n : ℕ) : Fintype (BitVec n) := Fintype.ofEquiv (Fin (2 ^ n)) BitVec.equivFin.symm.toEquiv /-- XOR by a fixed mask is self-inverse on `BitVec`: `c = k ^^^ m ↔ k = c ^^^ m`. -/ lemma xor_right_eq_iff {l : ℕ} (c m k : BitVec l) : (c = k ^^^ m) ↔ (k = c ^^^ m) := by grind /-- The ciphertext distribution of the OTP is uniform, regardless of the message. -/ theorem otp_ciphertextDist_eq_uniform {l : ℕ} (m : BitVec l) : (PMF.uniformOfFintype _).bind (PMF.pure <| · ^^^ m) = PMF.uniformOfFintype _ := by simp [PMF.ext_iff, xor_right_eq_iff] end Cslib.Crypto.PerfectSecrecy.OTP

linesthatinterlace

Posted some golfing.

SamuelSchlesinger requested review from chenson2018 and fmontesi as code owners April 1, 2026 14:12

linesthatinterlace reviewed Apr 1, 2026

View reviewed changes

Cslib/Cryptography/PerfectSecrecy/Internal/OneTimePad.lean Outdated Show resolved Hide resolved

linesthatinterlace reviewed Apr 1, 2026

View reviewed changes

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean Outdated Show resolved Hide resolved

linesthatinterlace reviewed Apr 1, 2026

View reviewed changes

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean Outdated Show resolved Hide resolved

linesthatinterlace reviewed Apr 1, 2026

View reviewed changes

fmontesi reviewed Apr 1, 2026

View reviewed changes

Cslib/Cryptography/PerfectSecrecy/Internal/PerfectSecrecy.lean Outdated Show resolved Hide resolved

fmontesi reviewed Apr 1, 2026

View reviewed changes

Cslib/Crypto/PerfectSecrecy/Defs.lean

Copy link
Copy Markdown

Collaborator

fmontesi Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Double directory name?

SamuelSchlesinger reacted with thumbs up emoji

fmontesi reviewed Apr 1, 2026

View reviewed changes

SamuelSchlesinger requested review from fmontesi and linesthatinterlace April 1, 2026 18:52

linesthatinterlace reviewed Apr 1, 2026

View reviewed changes


		namespace Cslib.Crypto.PerfectSecrecy.OTP

		noncomputable instance (n : ℕ) : Fintype (BitVec n) :=

Conversation

SamuelSchlesinger commented Apr 1, 2026

Uh oh!

SamuelSchlesinger commented Apr 1, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

linesthatinterlace left a comment

Choose a reason for hiding this comment

Uh oh!

SamuelSchlesinger commented Apr 1, 2026

Uh oh!

fmontesi commented Apr 1, 2026

Uh oh!

SamuelSchlesinger commented Apr 1, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

SamuelSchlesinger commented Apr 1, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!