Universal hashing and the leftover hash lemma

A two-universal hash family has collision probability at most 1 / |Output| on every pair of distinct inputs. The seed is independent of the source and remains part of the output. The leftover hash lemma compares this joint output to the same seed with an independent uniform value.

The statements allow any finite seed distribution satisfying the collision bound. They are information-theoretic results; efficient sampling and evaluation require separate certificates.

Main definitions

• Cslib.Probability.IsTwoUniversal: a pairwise collision bound for a sampled hash seed.
• Cslib.Probability.seededHash: reveal the independent hash seed and its digest together.

Main results

• Cslib.Probability.isTwoUniversal_iff_isUniversalHash: two-universality is 1 / |Output|-universality.
• Cslib.Probability.IsTwoUniversal.collision_with_set_le: isolation by a union bound.
• Cslib.Probability.IsTwoUniversal.leftover_hash: the strong leftover hash lemma.
• Cslib.Probability.IsTwoUniversal.leftover_hash_conditional: extraction with side information.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 3.3, Lemma 1. Its collision argument generalizes from field hashing and uniform seeds to any seed distribution satisfying the two-universality bound.
• I. Haitner, S. Vadhan, The Many Entropies in One-Way Functions, Section 2.4.1, Definition 4 and Lemma 8.

Adapted from Probability/UniversalHash.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the upstream finite-PMF distance.

def Cslib.Probability.IsTwoUniversal {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] (seed : PMF Seed) (hash : Seed → Input → Output) : Prop

Distinct inputs collide with probability at most the reciprocal output-space size.

theorem Cslib.Probability.isTwoUniversal_iff_isUniversalHash {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [Nonempty Output] {seed : PMF Seed} {hash : Seed → Input → Output} : IsTwoUniversal seed hash ↔ IsUniversalHash seed hash (↑(Fintype.card Output))⁻¹

Two-universality is 1 / |Output|-universality in the sense of Cslib.Probability.IsUniversalHash.

theorem Cslib.Probability.IsTwoUniversal.precompose {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] {Input' : Type u_4} {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) {encode : Input' → Input} (hinjective : Function.Injective encode) : IsTwoUniversal seed fun (key : Seed) (value : Input') => hash key (encode value)

An injective input representation preserves two-universality.

noncomputable def Cslib.Probability.seededHash {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} (seed : PMF Seed) (source : PMF Input) (hash : Seed → Input → Output) : PMF (Seed × Output)

Hash a source using an independent seed and reveal both the seed and the hash value.

theorem Cslib.Probability.seededHash_eq_bind {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} (seed : PMF Seed) (source : PMF Input) (hash : Seed → Input → Output) : seededHash seed source hash = source.bind fun (x : Input) => PMF.map (fun (s : Seed) => (s, hash s x)) seed

The independent source and public seed can be sampled in either order.

theorem Cslib.Probability.dist_seededHash_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [Fintype Input] (seed : PMF Seed) (p q : PMF Input) (hash : Seed → Input → Output) : dist (seededHash seed p hash) (seededHash seed q hash) ≤ dist p q

Applying a shared public hash seed cannot increase distance between source distributions.

theorem Cslib.Probability.seededHash_eq_uniform_of_subsingleton {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Output] [Subsingleton Output] [Nonempty Output] (seed : PMF Seed) (source : PMF Input) (hash : Seed → Input → Output) : seededHash seed source hash = seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output)

An empty digest is already uniform. This exact case avoids charging an extraction error when the source has too little entropy to supply even one prefix bit.

theorem Cslib.Probability.IsTwoUniversal.precompose_seed {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] {Seed' : Type u_4} [Fintype Seed'] (seed : PMF Seed') (prepare : Seed' → Seed) {hash : Seed → Input → Output} (hhash : IsTwoUniversal (PMF.map prepare seed) hash) : IsTwoUniversal seed fun (s : Seed') => hash (prepare s)

Re-encoding a seed preserves universality when its distribution is pushed forward.

theorem Cslib.Probability.IsTwoUniversal.collision_with_set_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (candidates : Finset Input) (x : Input) : (∑ s : Seed, if ∃ y ∈ candidates, y ≠ x ∧ hash s y = hash s x then (seed s).toReal else 0) ≤ ↑(candidates.erase x).card / ↑(Fintype.card Output)

A hash fails to isolate a fixed input from a candidate set only if one of the other candidates collides with it. Two-universality and the union bound control this probability.

theorem Cslib.Probability.IsTwoUniversal.collisionProbability_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (source : PMF Input) : ∑ s : Seed, (seed s).toReal * PMF.collisionProbability (PMF.map (hash s) source) ≤ PMF.collisionProbability source + (↑(Fintype.card Output))⁻¹

Two-universality bounds the average collision probability of the hashed source.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_sq {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] [Nonempty Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (source : PMF Input) : 4 * dist (seededHash seed source hash) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output)) ^ 2 ≤ ↑(Fintype.card Output) * PMF.collisionProbability source

The strong leftover hash lemma, in squared form without logarithms or square roots.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] [Nonempty Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (source : PMF Input) : dist (seededHash seed source hash) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output)) ≤ √(↑(Fintype.card Output) * PMF.collisionProbability source) / 2

The strong leftover hash lemma: the seed stays public and independent uniform bits replace the hash value, with error at most half the square root of output size times source collision.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_of_mass_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] [Nonempty Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (source : PMF Input) {mass : ℝ} (hmass : ∀ (x : Input), (source x).toReal ≤ mass) : dist (seededHash seed source hash) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output)) ≤ √(↑(Fintype.card Output) * mass) / 2

A pointwise probability bound is sufficient for the leftover hash lemma. This is the min-entropy form: use mass = 2⁻ᵏ for a source with at least k bits of min-entropy.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_conditional_sq {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] [Nonempty Output] {Side : Type u_4} [Fintype Side] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (side : PMF Side) (source : Side → PMF Input) : 4 * dist (side.bind fun (info : Side) => PMF.map (fun (x : Seed × Output) => (info, x)) (seededHash seed (source info) hash)) (side.bind fun (info : Side) => PMF.map (fun (x : Seed × Output) => (info, x)) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output))) ^ 2 ≤ ↑(Fintype.card Output) * ∑ info : Side, (side info).toReal * PMF.collisionProbability (source info)

Revealing side information costs the average collision probability of the conditional sources. The hash seed is sampled independently of both the side information and the source.

theorem Cslib.Probability.IsTwoUniversal.leftover_hash_conditional {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] [Fintype Output] [Nonempty Output] {Side : Type u_4} [Fintype Side] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (side : PMF Side) (source : Side → PMF Input) : dist (side.bind fun (info : Side) => PMF.map (fun (x : Seed × Output) => (info, x)) (seededHash seed (source info) hash)) (side.bind fun (info : Side) => PMF.map (fun (x : Seed × Output) => (info, x)) (seed.bind fun (s : Seed) => PMF.map (fun (x : Output) => (s, x)) (PMF.uniformOfFintype Output))) ≤ √(↑(Fintype.card Output) * ∑ info : Side, (side info).toReal * PMF.collisionProbability (source info)) / 2

Conditional leftover hashing in its usual square-root form.