OTP: Perfect Secrecy in Lean#
The standard way to prove the perfect secrecy of OTP is to show that for any fixed
plaintext m
, the conditional distribution of ciphertexts is uniform.
Proof Setup#
We define the conditional distribution μC_M m
by mapping the encryption function
over the uniform key distribution.
-- The distribution of ciphertexts, conditioned on a fixed message `m`.
noncomputable def μC_M {n : ℕ} (m : Plaintext n) : PMF (Ciphertext n) :=
PMF.map (encrypt m) μK
Our goal is to prove that this distribution is uniform.
Theorem: ∀ (m : Plaintext n), μC_M m = PMF.uniformOfFintype (Ciphertext n)
A Detour into Equivalences (≃
)#
Key mathematical insight: for a fixed m
, the function encrypt m
is a bijection.
In Lean, such a bijection is captured by the type Equiv
, written α ≃ β
.
What is an Equiv
?#
An Equiv
is a structure that bundles a function, its inverse, and proofs that they
are indeed inverses of each other. It represents an isomorphism between types.
The formal definition in Mathlib is:
structure Equiv (α : Sort*) (β : Sort*) where
toFun : α → β -- The forward function
invFun : β → α -- The inverse function
left_inv : Function.LeftInverse invFun toFun -- proof of invFun (toFun x) = x
right_inv : Function.RightInverse invFun toFun -- proof of toFun (invFun y) = y
How to Construct an Equiv
(Intro)#
There are two main ways to build an equivalence.
-
From an Involutive Function (High-Level)
If a function is its own inverse, like
not
or ourencrypt m
, you can use the constructorEquiv.ofInvolutive
.-- Helper lemma: For a fixed message m, encryption is its own inverse. lemma encrypt_involutive {n : ℕ} (m : Plaintext n) : Function.Involutive (encrypt m) := by ... -- We build the Equiv directly from this property. def encrypt_equiv {n : ℕ} (m : Plaintext n) : Key n ≃ Ciphertext n := Equiv.ofInvolutive (encrypt m) (encrypt_involutive m)
-
By Hand (Low-Level)
You can construct one by providing all four fields. This is useful for simple cases.
How to Use an Equiv
(Elim)#
Once you have an Equiv
, you can use it in several ways.
-
As a Function. Lean knows how to treat an
Equiv
e
as a function. You can just writee x
. -
Accessing the Inverse. The inverse is available as
e.symm
. So you can writee.symm y
. -
Using the Proofs. The proofs
e.left_inv
ande.right_inv
are powerful tools for rewriting.
example (e : α ≃ β) (x : α) : e.symm (e x) = x := by
-- The goal is exactly the statement of the left_inv property.
simp [e.left_inv]
-
Understanding how to construct and use equivalences is crucial for many proofs involving bijections.
-
The final step of our OTP theorem would be to find the right Mathlib lemma that uses this
encrypt_equiv
to prove that themap
of a uniform distribution is still uniform.
Next#
-
A detailed Markdown explanation of our proof for
otp_perfect_secrecy_lemma
. -
An explanation for why
encrypt_equiv
must benoncomputable
whilexorEquiv
is not.
Let's tackle the noncomputable
question first, as it's a deep and important concept in Lean.
Computable vs. Noncomputable Definitions#
The reason one definition is noncomputable
and the other is not comes down to how the inverse function is provided.
It's a classic case of being constructive versus classical.
def xorEquiv
(Constructive)#
def xorEquiv {n : ℕ} (m : Plaintext n) : Key n ≃ Ciphertext n where
toFun := encrypt m
invFun := vec_xor m -- We explicitly provide the inverse function
left_inv := by ...
right_inv := by ...
Here, we create the Equiv
structure by hand. We provide all four components:
-
toFun
: The forward function,encrypt m
. -
invFun
: The inverse function,vec_xor m
. We explicitly construct and provid this function. -
left_inv
: A proof thatvec_xor m (encrypt m k) = k
. -
right_inv
: A proof thatencrypt m (vec_xor m c) = c
.
Because every component is explicitly defined and computable, the entire xorEquiv
definition is computable.
noncomputable def encrypt_equiv
(Classical)#
noncomputable def encrypt_equiv {n : ℕ} (m : Plaintext n) : Key n ≃ Ciphertext n :=
Equiv.ofBijective (encrypt m) (encrypt_bijective m)
Here, we use the high-level constructor Equiv.ofBijective
. We provide it with:
-
A function,
encrypt m
. -
A proof,
encrypt_bijective m
, which proves that the function is both injective and surjective.
But notice what's missing: we never told Lean what the inverse function is!
The Equiv.ofBijective
constructor has to create the inverse function for us.
How does it do that? It uses the proof of surjectivity.
A proof of Surjective (encrypt m)
says "for every ciphertext c
, there exists a key k
such that encrypt m k = c
."
To define an inverse function, Lean must choose such a k
for each c
.
This act of choosing an object from a proof of its existence requires the axiom of
choice (Classical.choice
).
In Lean's constructive logic, any definition that depends on the axiom of choice is marked as noncomputable
.
In short:
-
xorEquiv
is computable because we did the work of providing the inverse function constructively. -
encrypt_equiv
is noncomputable because we asked Lean to conjure the inverse function out of a classical existence proof, forcing it to use the noncomputable axiom of choice.
Explaining the otp_perfect_secrecy_lemma
Proof#
Theorem to Prove:
theorem otp_perfect_secrecy_lemma {n : ℕ} :
∀ (m : Plaintext n), μC_M m = PMF.uniformOfFintype (Ciphertext n)
The Proof, Explained:
theorem otp_perfect_secrecy_lemma {n : ℕ} :
∀ (m : Plaintext n), μC_M m = PMF.uniformOfFintype (Ciphertext n) := by
intro m
have hμ : μC_M m = PMF.uniformOfFintype (Ciphertext n) := by
apply map_uniformOfFintype_equiv (xorEquiv m)
simp [hμ, PMF.uniformOfFintype_apply]
-
Tactic
intro m
- What it does: The proof begins by addressing the "for all
m
" part of the theorem.
The
intro
tactic introduces an arbitrary but fixed messagem
that we can work with for the rest of the proof.-
Goal State:
- What it does: The proof begins by addressing the "for all
-
Tactic
have hμ : ... := by ...
-
What it does: This is the main logical step. The
have
tactic lets us prove a helper fact, or lemma, which we can then use to prove our main goal. Here, we are proving a fact namedhμ
. Coincidentally,hμ
is the exact statement of our main goal. -
The Sub-Proof: The proof of
hμ
isapply map_uniformOfFintype_equiv (xorEquiv m)
. This applies the helper lemma you proved earlier, which states that mapping a uniform distribution over an equivalence (xorEquiv m
) results in a uniform distribution. This single line brilliantly captures the core mathematical argument. -
Goal State (after the
have
block is complete):
-
-
Tactic
simp [hμ, PMF.uniformOfFintype_apply]
-
What it does: This tactic finishes the proof using the fact
hμ
we just proved. Thesimp [hμ]
part tells Lean to rewrite the goal usinghμ
. -
How it Works:
simp
seesμC_M m
on the left side of the goal⊢
and sees the hypothesishμ
which statesμC_M m = ...
. It substitutes the left side with the right side ofhμ
. -
Goal State (after
simp [hμ]
): -
This goal is true by reflexivity, and
simp
is able to solve it completely. (The extraPMF.uniformOfFintype_apply
is not strictly necessary here, ashμ
is sufficient, but it doesn't hurt). A more direct way to finish after thehave
block would simply beexact hμ
.
-