OTP.Basic.lean

This is the first file in a collection of Lean programs about the one-time pad (OTP) cryptographic scheme. It defines the basic types and operations needed for OTP, including:

• Types for plaintext, key, and ciphertext
• Boolean xor operation
• Pointwise xor operation for boolean vectors
• Encrypt and decrypt operations
• Properties of xor and vector xor operations
• Demos of basic OTP operations and xor properties

Other files in the collection prove properties like key uniqueness and perfect secrecy.

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.

Types for the one-time pad (OTP) and properties of xor

Types for the OTP

def Plaintext (n : ℕ) : Type

Equations

• Plaintext n = List.Vector Bool n

def Key (n : ℕ) : Type

Equations

• Key n = List.Vector Bool n

def Ciphertext (n : ℕ) : Type

Equations

• Ciphertext n = List.Vector Bool n

Definition of Boolean xor

This is actually a build-in function in Lean, called Bool.xor, but we define it here for clarity.

def XOR (a b : Bool) : Bool

Equations

• XOR true true = false
• XOR true false = true
• XOR false true = true
• XOR false false = false

xor is associative

Definition of vec_xor operation: point-wise xor for boolean vectors

def vec_xor {n : ℕ} (v₁ v₂ : List.Vector Bool n) : List.Vector Bool n

Equations

• vec_xor v₁ v₂ = List.Vector.map₂ xor v₁ v₂

Definitions of encrypt and decrypt operations

def encrypt {n : ℕ} (m : Plaintext n) (k : Key n) : Ciphertext n

Equations

• encrypt m k = vec_xor m k

def decrypt {n : ℕ} (c : Ciphertext n) (k : Key n) : Plaintext n

Equations

• decrypt c k = vec_xor c k

Demo 1: Basic OTP Operations

def msg : Plaintext 4

Equations

• msg = ⟨[true, false, true, true], msg._proof_1⟩

def key : Key 4

Equations

• key = ⟨[false, true, false, true], key._proof_1⟩

def key2 : Key 4

Equations

• key2 = ⟨[true, true, false, false], key2._proof_1⟩

Demo 2: xor properties

theorem xor_aab_eq_b (a b : Bool) : (a ^^ (a ^^ b)) = b

theorem xor_abb_eq_a (a b : Bool) : (a ^^ b ^^ b) = a

theorem xor_ab_eq_c_iff_b_eq_ac (a b c : Bool) : (a ^^ b) = c ↔ b = (a ^^ c)