OTP.PerfectSecrecy.lean

This file proves properties of perfect secrecy in the one-time pad (OTP) cryptographic scheme. It includes:

• The definition of perfect secrecy
• The proof that OTP achieves perfect secrecy
• The relationship between the key and ciphertext distributions
• The uniformity of the ciphertext distribution given a message
• The uniformity of the ciphertext distribution overall
• The law of total probability for the ciphertext distribution

Files in this series:

• OTP.Basic: Basic definitions and operations for OTP
• OTP.KeyUniqueness: Properties of keys in OTP
• OTP.Distributions: Probability distributions related to OTP
• OTP.PerfectSecrecy: Properties of perfect secrecy in OTP
• OTP.Examples: Concrete examples and demos of OTP operations and properties
• OTP.SimpleSecrecy: Simplified version of OTP.PerfectSecrecy where we assume the message distribution is uniform.

A brief note about coercions

Coercion is a mechanism to convert a term of one type to another to prevent a type error.

For instance, given n : ℕ and a function that expects an integer f (x : ℤ), you can explicitly write f ↑n to show the coercion from ℕ to ℤ.

As far as I can tell, ↑a signifies coercion of "standard" types, while ⇑e signifies coercion of more complicated types.

To type the coercion symbol in the VSCode editor with the Lean4 extension,

• For ↑, type \u or \uparrow followed by a space or tab.

• For ⇑, type \u= or \Uparrow followed by a space or tab.

You can discover all available Unicode symbol abbreviations within VSCode by opening the Command Palette (Ctrl+Shift+P or Cmd+Shift+P on Mac) and searching for "Lean 4: Show Unicode Input Abbreviations".

A brief note about universe levels

Types form a hierarchy that is parameterized by universe levels. The assertion that α is a type at universe level ℓ is expressed as α : Type ℓ. Fortunately, in most cases we can elide this technicality by declaring our types with the special Lean syntax α : Type*, which tells Lean to select a fresh universe level for α and make that level an implicit parameter.

LEMMA 1. Mapping a uniform PMF through a bijection is uniform

This lemma involves proving that two PMFs are equal. How is this done? Let's look at the definition of PMF in mathlib/Mathlib/Probability/ProbabilityMassFunction/Basic.lean.

definition of PMF:

def PMF.{u} (α : Type u) : Type u :=
  { f : α → ℝ≥0∞ // HasSum f 1 }

namespace PMF

instance instFunLike : FunLike (PMF α) α ℝ≥0∞ where
  coe p a := p.1 a
  coe_injective' _ _ h := Subtype.eq h

@[ext]
protected theorem ext {p q : PMF α} (h : ∀ x, p x = q x) : p = q :=
  DFunLike.ext p q h

There is an instance of FunLike for PMF α, which means that we can treat a PMF as a function from α to ℝ≥0∞. This is crucial for proving that two PMFs are equal: we can show that they assign the same probability to each possible value of the random variable. Indeed, the ext theorem for PMF is essentially function extensionality for PMFs.

theorem map_uniformOfFintype_equiv {α : Type u_1} [Fintype α] [Nonempty α] {β : Type u_2} [Fintype β] [Nonempty β] (e : α ≃ β) : PMF.map (⇑e) (PMF.uniformOfFintype α) = PMF.uniformOfFintype β

LEMMA 2. The ciphertext-given-message distribution is uniform

instance ciphertext_fintype {n : ℕ} : Fintype (Ciphertext n)

Equations

• ciphertext_fintype = id inferInstance

instance ciphertext_nonempty {n : ℕ} : Nonempty (Ciphertext n)

theorem C_given_M_eq_inv_card_key {n : ℕ} (m : Plaintext n) (c : Ciphertext n) : (μC_M m) c = 1 / ↑(Fintype.card (Key n))

Example

For a 3-bit message and ciphertext, the conditional distribution is uniform:

∀ c, P(C = c | M = m) = 1/8

theorem C_given_M_eq_inv_card_key_ennreal {n : ℕ} (m : Plaintext n) (c : Ciphertext n) : (μC_M m) c = (↑(Fintype.card (Key n)))⁻¹

theorem conditional_independent_of_message {n : ℕ} (m₁ m₂ : Plaintext n) (c : Ciphertext n) : (μC_M m₁) c = (μC_M m₂) c

LEMMA 2: The overall ciphertext distribution μC is also uniform.-----------

The probability P(C = c) that ciphertext c is observed (which is (μC μM) c), is uniform over the ciphertext space. That is: (μC μM) c = 1 / (card (Ciphertext n))

Since card (Key n) = card (Ciphertext n) (due to xorEquiv), this would imply that (μC μM) c is also equal 1 / card (Key n).

Law of Total Probability for Discrete Distributions in Lean 4

REVIEW: Probability in Lean/Mathlib

In Mathlib, discrete probability distributions are represented using the PMF (Probability Mass Function) type.

• PMF α represents a probability distribution over a type α
• For p : PMF α and a : α, the expression p a gives the probability of outcome a
• Probabilities are represented as NNReal (non-negative real numbers) in [0, ∞)
• When doing arithmetic, we often coerce to ENNReal (extended non-negative reals) in [0, ∞]

REVIEW: Random Variables and Transformations

In probability theory, if X is a random variable with distribution μX, and Y = f(X) for some function f, then the distribution of Y can be computed using:

• PMF.map f μX - the distribution of f(X)
• PMF.bind μX g - for dependent distributions, where g : α → PMF β

REVIEW: The Law of Total Probability

For random variables X and Y, the law of total probability states: P(Y = y) = Σ_x P(Y = y , X = x) = Σ_x P(Y = y | X = x) P(X = x)

In our case:

• X is the message M with distribution μM
• Y is the ciphertext C with distribution μC
• P(C = c | M = m) is given by μC_M m c

theorem pmf_bind_expanded {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (b : β) : (p.bind f) b = ∑' (a : α), p a * (f a) b

The Most Basic Statement: P(C = c) = Σ_{m,k} P(C = c ∧ M = m ∧ K = k)

theorem marginal_probability_direct {n : ℕ} (μM : PMF (Plaintext n)) (c : Ciphertext n) : (μC μM) c = ∑' (mk : Plaintext n × Key n), if c = encrypt mk.1 mk.2 then (μMK μM) mk else 0

theorem law_of_total_probability {n : ℕ} (μM : PMF (Plaintext n)) (c : Ciphertext n) : (μC μM) c = ∑' (m : Plaintext n), μM m * (μC_M m) c

The law of total probability for PMFs: P(Y = y) = Σ_x P(X = x) * P(Y = y | X = x)

theorem prob_C_uniform_ennreal {n : ℕ} (μM : PMF (Plaintext n)) (c : Ciphertext n) : (μC μM) c = (↑(Fintype.card (Key n)))⁻¹

theorem μC_is_uniform {n : ℕ} (μM : PMF (Plaintext n)) : μC μM = PMF.uniformOfFintype (Ciphertext n)

Perfect Secrecy Theorem ---------------------------------------------

The theorem states that the probability of a ciphertext given a specific plaintext is equal to the probability of that plaintext, which is the essence of perfect secrecy. This means that knowing the ciphertext does not give any information about the plaintext. The proof uses the uniformity of the ciphertext distribution and the independence of the key.

Perfect Secrecy: The Clean Version

theorem perfect_secrecy_clean {n : ℕ} (μM : PMF (Plaintext n)) (m : Plaintext n) (c : Ciphertext n) : (μC_M m) c = (μC μM) c

theorem no_information_leakage {n : ℕ} (μM : PMF (Plaintext n)) (m : Plaintext n) (c : Ciphertext n) (h_pos : (μC μM) c ≠ 0) : (μC_M m) c * μM m / (μC μM) c = μM m

theorem both_distributions_uniform {n : ℕ} (μM : PMF (Plaintext n)) : (∀ (m : Plaintext n), μC_M m = PMF.uniformOfFintype (Ciphertext n)) ∧ μC μM = PMF.uniformOfFintype (Ciphertext n)

theorem perfect_secrecy {n : ℕ} (μM : PMF (Plaintext n)) (m₀ : Plaintext n) (c₀ : Ciphertext n) : (μC_M m₀) c₀ * μM m₀ / (μC μM) c₀ = μM m₀