OTP.Distributions.lean

This file defines the probability distributions related to the one-time pad (OTP) cryptographic scheme. It includes:

• Uniform distribution over keys
• Joint distribution of plaintext and key
• Ciphertext distribution derived from plaintext and key
• Conditional distribution of ciphertext given plaintext

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.

instance key_fintype {n : ℕ} : Fintype (Key n)

Equations

• key_fintype = id inferInstance

instance key_nonempty {n : ℕ} : Nonempty (Key n)

Uniform Key Distribution

noncomputable def μK {n : ℕ} : PMF (Key n)

Equations

• μK = PMF.uniformOfFintype (Key n)

Independence and Joint Distribution

The crucial assumption for OTP's perfect secrecy is that the key is chosen independently of the message.

For pmfs μM : PMF (Plaintext n) and μK : PMF (Key n), their joint distribution μMK : PMF (Plaintext n × Key n) assigns probability (μM m) ⬝ (μK k) to the pair (m, k).

noncomputable def μMK {n : ℕ} (μM : PMF (Plaintext n)) : PMF (Plaintext n × Key n)

Equations

• μMK μM = μM.bind fun (m : Plaintext n) => PMF.map (fun (k : Key n) => (m, k)) μK

Ciphertext Distribution

noncomputable def μC {n : ℕ} (μM : PMF (Plaintext n)) : PMF (Ciphertext n)

Equations

• μC μM = (μMK μM).bind fun (x : Plaintext n × Key n) => match x with | (m, k) => PMF.pure (encrypt m k)

ℙ(C = c | M = m)

This represents the probability of observing ciphertext c, given the message is M = m.

If the message is m, the ciphertext r.v. C = encrypt(m, K) depends only on the randomly chosen key (which follows the μK distribution).

noncomputable def μC_M {n : ℕ} (m : Plaintext n) : PMF (Ciphertext n)

Equations

• μC_M m = PMF.map (fun (k : Key n) => encrypt m k) μK