XOR Bijection Library

This file provides reusable XOR bijection infrastructure for cryptographic proofs.

Overview

Many CatCrypt proofs rely on the fact that XOR with a fixed value is a bijection. This file centralizes the definition and key theorems, eliminating duplication across 20+ example files.

Main definitions

• xorEquiv - General XOR bijection for any type with an involutive XOR operation
• boolXorBij - XOR bijection on Bool (the most commonly used specialization)

Main results

• rHoare_sample_xor - Sampling a key and applying XOR has the same distribution as sampling directly (coupling lemma)
• advantage_zero_of_xor - Zero advantage corollary for XOR-based games

References

• [Shannon, Communication Theory of Secrecy Systems, 1949]

General XOR Equivalence

def CatCrypt.Prob.XorBij.xorEquiv {α : Type} (op : α → α → α) (hInvol : ∀ (a b : α), op (op a b) b = a) (x : α) : α ≃ α

XOR with a fixed value is an equivalence for any involutive binary operation.

Given an operation op satisfying op (op a b) b = a for all a b, xorEquiv op h x is the equivalence a ↦ op a x with inverse r ↦ op r x.

Equations

• CatCrypt.Prob.XorBij.xorEquiv op hInvol x = { toFun := fun (k : α) => op k x, invFun := fun (r : α) => op r x, left_inv := ⋯, right_inv := ⋯ }

Bool XOR Bijection

def CatCrypt.Prob.XorBij.boolXorBij (x : Bool) : Bool ≃ Bool

XOR with a fixed Bool is a bijection.

This is the fundamental property used in OTP, PRF, MAC, PRG, and many other cryptographic proofs; it is shared here rather than duplicated per file.

Equations

• CatCrypt.Prob.XorBij.boolXorBij x = { toFun := fun (k : Bool) => k ^^ x, invFun := fun (r : Bool) => r ^^ x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CatCrypt.Prob.XorBij.boolXorBij_apply (x k : Bool) : (boolXorBij x) k = (k ^^ x)

@[simp]

theorem CatCrypt.Prob.XorBij.boolXorBij_symm (x : Bool) : (boolXorBij x).symm = boolXorBij x

Product XOR Bijection

def CatCrypt.Prob.XorBij.prodBoolXorBij (c : Bool × Bool) : Bool × Bool ≃ Bool × Bool

XOR bijection on Bool × Bool (component-wise).

Used in PRPCCA for ciphertext-space bijections.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CatCrypt.Prob.XorBij.prodBoolXorBij_apply (c k : Bool × Bool) : (prodBoolXorBij c) k = (k.1 ^^ c.1, k.2 ^^ c.2)

Coupling Lemma

The key theorem: sampling a key uniformly and applying XOR with a fixed message is indistinguishable from sampling uniformly.

This eliminates the ~15-line coupling proof pattern repeated across ~10 files.

theorem CatCrypt.Prob.XorBij.rHoare_sample_bij {α : Type} [Fintype α] [Nonempty α] (f : α ≃ α) : Relational.rHoare Relational.eqPre (do let k ← Core.SPComp.sample α Core.SPComp.pure (f k)) (Core.SPComp.sample α) Relational.eqPost

Core coupling: for any bijection family, sampling a key and applying the bijection is coupled with uniform sampling via eqPost.

This is the general pattern:

• Real: k ← sample α; pure (f k)
• Ideal: sample α
• Coupled via bijection f : α ≃ α

theorem CatCrypt.Prob.XorBij.rHoare_sample_xor (m : Bool) : Relational.rHoare Relational.eqPre (do let k ← Core.SPComp.sample Bool Core.SPComp.pure (k ^^ m)) (Core.SPComp.sample Bool) Relational.eqPost

Coupling for Bool XOR: sampling a key and XORing with a message has the same distribution as sampling directly.

Real game: k ← sample Bool; pure (xor k m) Ideal game: sample Bool

This is the single most commonly needed coupling in CatCrypt examples.

theorem CatCrypt.Prob.XorBij.rHoare_sample_prod_xor (c : Bool × Bool) : Relational.rHoare Relational.eqPre (do let k ← Core.SPComp.sample (Bool × Bool) Core.SPComp.pure (k.1 ^^ c.1, k.2 ^^ c.2)) (Core.SPComp.sample (Bool × Bool)) Relational.eqPost

Coupling for product Bool XOR.

Zero Advantage Corollaries

theorem CatCrypt.Prob.XorBij.advantage_zero_of_bij {α : Type} [Fintype α] [Nonempty α] (f : α ≃ α) (A : α → Core.SPComp Bool) : Crypto.AdvantageA (do let k ← Core.SPComp.sample α Core.SPComp.pure (f k)) (Core.SPComp.sample α) A = 0

If real game is sample key >> apply bijection and ideal game is sample, then every adversary has zero advantage.

theorem CatCrypt.Prob.XorBij.advantage_zero_of_xor (m : Bool) (A : Bool → Core.SPComp Bool) : Crypto.AdvantageA (do let k ← Core.SPComp.sample Bool Core.SPComp.pure (k ^^ m)) (Core.SPComp.sample Bool) A = 0

Zero advantage for Bool XOR games.

XOR Algebraic Helpers

theorem CatCrypt.Prob.XorBij.xor_self_inverse (a b : Bool) : (a ^^ b ^^ b) = a

XOR is self-inverse: xor (xor a b) b = a

@[simp]

theorem CatCrypt.Prob.XorBij.xor_false_right (b : Bool) : (b ^^ false) = b

XOR with false is identity

@[simp]

theorem CatCrypt.Prob.XorBij.xor_true_right (b : Bool) : (b ^^ true) = !b

XOR with true is negation