Birthday Bound

This file provides the birthday bound: the probability that q uniform samples from a set of size N contain a collision is at most q(q-1)/(2N).

Structure

Layer 1 — Pure arithmetic: Gauss sum formula in ENNReal.

Layer 2 — Abstract composition: If the per-step collision probability at step i is at most i/N, the total collision probability is ≤ q(q-1)/(2N).

Layer 3 — Connection to security games: The birthday bound implies that advantage between random function and random permutation games is small.

Key Theorems

• gauss_sum_ennreal — ∑_{i<q} i/N = q(q-1)/2 / N in ENNReal
• birthday_bound_sum — If step_pr(i) ≤ i/N, then ∑ step_pr(i) ≤ q(q-1)/(2N)
• birthday_advantage — Compose per-step advantage bounds into birthday bound

References

• [Bellare & Rogaway, Introduction to Modern Cryptography]
• [Shoup, Sequences of Games]

Layer 1: Pure Arithmetic

theorem CatCrypt.Prob.BirthdayBound.gauss_sum_nat (q : ℕ) : ∑ i ∈ Finset.range q, i = q * (q - 1) / 2

Gauss sum formula in ℕ: ∑_{i<q} i = q*(q-1)/2

theorem CatCrypt.Prob.BirthdayBound.gauss_sum_mul_two (q : ℕ) : (∑ i ∈ Finset.range q, i) * 2 = q * (q - 1)

Gauss sum formula with factor of 2: 2 * ∑_{i<q} i = q*(q-1)

theorem CatCrypt.Prob.BirthdayBound.gauss_sum_ennreal (q : ℕ) (N : ENNReal) : ∑ i ∈ Finset.range q, ↑i / N = ↑(q * (q - 1) / 2) / N

Key arithmetic identity in ENNReal: ∑_{i<q} (i : ℝ≥0∞) / N = q*(q-1)/2 / N

This is the birthday bound formula expressed as a sum of per-step collision probabilities.

Layer 2: Abstract Composition

Given per-step collision probabilities bounded by i/N,
bound the total collision probability by q(q-1)/(2N).

theorem CatCrypt.Prob.BirthdayBound.birthday_bound_sum (q : ℕ) (N : ENNReal) (step_pr : ℕ → ENNReal) (hstep : ∀ i < q, step_pr i ≤ ↑i / N) : ∑ i ∈ Finset.range q, step_pr i ≤ ↑(q * (q - 1) / 2) / N

Birthday bound from per-step bounds: If the probability of a collision at step i (given no collision at steps < i) is at most i/N, then the total collision probability is at most q(q-1)/(2N).

The per-step bound i/N is the probability that a fresh uniform sample from a set of size N collides with any of the i previously seen values.

The composition uses the union bound (sum of per-step probabilities).

theorem CatCrypt.Prob.BirthdayBound.birthday_bound_sum_nat (q N : ℕ) (step_pr : ℕ → ENNReal) (hstep : ∀ i < q, step_pr i ≤ ↑i / ↑N) : ∑ i ∈ Finset.range q, step_pr i ≤ ↑(q * (q - 1) / 2) / ↑N

Birthday bound (natural number denominator): Specialization with N as a natural number.

Layer 3: Integration with Security Games

These lemmas connect the birthday bound to the advantage framework,
allowing it to be used directly in game-hopping security proofs.

theorem CatCrypt.Prob.BirthdayBound.birthday_advantage {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (q N : ℕ) (hstep : ∀ i < q, Crypto.AdvantageA (G i) (G (i + 1)) A ≤ ↑i / ↑N) : Crypto.AdvantageA (G 0) (G q) A ≤ ↑(q * (q - 1) / 2) / ↑N

Birthday bound for advantage: Given a sequence of hybrid games where step i→(i+1) has advantage ≤ i/N, the total advantage is at most q(q-1)/(2N).

This combines the birthday bound arithmetic with the hybrid argument.

theorem CatCrypt.Prob.BirthdayBound.birthday_advantage_bound {α : Type} (real ideal : Core.SPComp α) (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (q N : ℕ) (hleft : real = G 0) (hright : ideal = G q) (hstep : ∀ i < q, Crypto.AdvantageA (G i) (G (i + 1)) A ≤ ↑i / ↑N) : Crypto.AdvantageA real ideal A ≤ ↑(q * (q - 1) / 2) / ↑N

Birthday bound for advantage with boundary conditions: When real = G 0 and ideal = G q.

Birthday Bound: Small Cases

For small concrete cases, the birthday bound gives explicit values.

theorem CatCrypt.Prob.BirthdayBound.birthday_q2 (N : ℕ) (step_pr : ℕ → ENNReal) (hstep : ∀ i < 2, step_pr i ≤ ↑i / ↑N) : ∑ i ∈ Finset.range 2, step_pr i ≤ 1 / ↑N

Birthday bound for q=2, N: Pr[collision] ≤ 1/N

theorem CatCrypt.Prob.BirthdayBound.birthday_q0 (N : ℕ) (step_pr : ℕ → ENNReal) : ∑ i ∈ Finset.range 0, step_pr i ≤ 0 / ↑N

Birthday bound for q=0: trivially 0

theorem CatCrypt.Prob.BirthdayBound.birthday_q1 (N : ℕ) (step_pr : ℕ → ENNReal) (hstep : ∀ i < 1, step_pr i ≤ ↑i / ↑N) : ∑ i ∈ Finset.range 1, step_pr i = 0

Birthday bound for q=1: 0 (no collision possible with one sample)