OTP.KeyUniqueness.lean

Key Uniqueness in One-Time Pad (OTP)

This file proves properties of keys in the one-time pad (OTP) encryption scheme that are crucial for OTP's perfect secrecy.

These properties include:

• The involutive nature of the vec_xor _ k and vec_xor m _ operations
• The uniqueness of keys given a plaintext message and ciphertext
• The injectivity of encryption with a fixed key
• The injectivity of encryption of a fixed message
• The bijection between keys and ciphertexts for a fixed message
• The existence of a unique key for each ciphertext given a 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.

Properties of vec_xor

theorem vec_xor_left_involutive {n : ℕ} (m : Plaintext n) (k : Key n) : vec_xor m (vec_xor m k) = k

theorem vec_xor_right_involutive {n : ℕ} (m : Plaintext n) (k : Key n) : vec_xor (vec_xor m k) k = m

theorem decrypt_encrypt {n : ℕ} (m : Plaintext n) (k : Key n) : decrypt (encrypt m k) k = m

theorem encrypt_decrypt {n : ℕ} (c : Ciphertext n) (k : Key n) : encrypt (decrypt c k) k = c

theorem key_uniqueness {n : ℕ} (m : Plaintext n) (k : Key n) (c : Ciphertext n) : vec_xor m k = c ↔ k = vec_xor m c

vec_xor is a bijection between Key and Ciphertext

def xorEquiv {n : ℕ} (m : Plaintext n) : Key n ≃ Ciphertext n

Equations

• xorEquiv m = { toFun := vec_xor m, invFun := vec_xor m, left_inv := ⋯, right_inv := ⋯ }