Universal hashing and the leftover hash lemma

A hash family whose seed is independent of the source and published with the digest turns a source with small collision probability into almost uniform bits: this is the leftover hash lemma. It is proved once, for ε-universal families (Cslib.Probability.IsUniversalHash): the joint law of the seed and the digest is within √(|Output| (CP + ε) - 1) / 2 of the seed with an independent uniform value, where CP is the collision probability of the source. Universal families in the sense of Carter and Wegman have ε = 1 / |Output| (Cslib.Probability.IsTwoUniversal), and then the bound is √(|Output| CP) / 2.

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: 1 / |Output|-universal families.
• Cslib.Probability.seededHash: reveal the independent hash seed and its digest together.

Main results

• Cslib.Probability.IsDeltaUniversalHash.isTwoUniversal: a 1 / |Output|-Δ-universal family is two-universal.
• Cslib.Probability.IsTwoUniversal.sum_ite_le, Cslib.Probability.isTwoUniversal_iff_sum_ite_le: real-valued pairwise collision bound (|Output| : ℝ)⁻¹.
• Cslib.Probability.isTwoUniversal_uniformOfFintype_iff, Cslib.Probability.IsTwoUniversal.expect_boole_le: two-universality under a uniform seed as a uniform expectation bound.
• Cslib.Probability.IsUniversalHash.collision_with_set_le: isolation by a union bound.
• Cslib.Probability.IsUniversalHash.leftover_hash_sq, Cslib.Probability.IsUniversalHash.leftover_hash: the strong leftover hash lemma for ε-universal families.
• Cslib.Probability.IsTwoUniversal.leftover_hash: its form for universal families.
• Cslib.Probability.IsTwoUniversal.leftover_hash_conditional: extraction with side information.

References

• J. L. Carter, M. N. Wegman, Universal Classes of Hash Functions
• 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 collision 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.

@[reducible, inline]

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

A universal hash family in the sense of Carter and Wegman [CW79]: distinct inputs collide with probability at most 1 / |Output|.

theorem Cslib.Probability.IsDeltaUniversalHash.isTwoUniversal {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Output] [AddGroup Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hh : IsDeltaUniversalHash seed hash (↑(Fintype.card Output))⁻¹) : IsTwoUniversal seed hash

A 1 / |Output|-Δ-universal hash family is two-universal.

theorem Cslib.Probability.IsTwoUniversal.sum_ite_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) {x y : Input} (hxy : x ≠ y) : (∑ s : Seed, if hash s x = hash s y then (seed s).toReal else 0) ≤ (↑(Fintype.card Output))⁻¹

For a universal hash family, distinct inputs collide with total seed probability at most (|Output| : ℝ)⁻¹.

theorem Cslib.Probability.isTwoUniversal_iff_sum_ite_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] {seed : PMF Seed} {hash : Seed → Input → Output} : IsTwoUniversal seed hash ↔ ∀ (x y : Input), x ≠ y → (∑ s : Seed, if hash s x = hash s y then (seed s).toReal else 0) ≤ (↑(Fintype.card Output))⁻¹

Two-universality is equivalent to the real-valued pairwise collision bound (|Output| : ℝ)⁻¹ on every pair of distinct inputs.

theorem Cslib.Probability.isTwoUniversal_uniformOfFintype_iff {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [Nonempty Seed] {hash : Seed → Input → Output} : IsTwoUniversal (PMF.uniformOfFintype Seed) hash ↔ ∀ (x y : Input), x ≠ y → (Finset.univ.expect fun (s : Seed) => if hash s x = hash s y then 1 else 0) ≤ (↑(Fintype.card Output))⁻¹

Under the uniform seed distribution, two-universality is equivalent to bounding the uniform expectation of the collision indicator of distinct inputs by 1 / |Output|.

theorem Cslib.Probability.IsTwoUniversal.expect_boole_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [Nonempty Seed] [DecidableEq Output] {hash : Seed → Input → Output} (hhash : IsTwoUniversal (PMF.uniformOfFintype Seed) hash) {x y : Input} (hxy : x ≠ y) : (Finset.univ.expect fun (s : Seed) => if hash s x = hash s y then 1 else 0) ≤ (↑(Fintype.card Output))⁻¹

Under the uniform seed distribution, two-universality bounds the uniform expectation of the collision indicator of distinct inputs by 1 / |Output|.

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.IsUniversalHash.collision_with_set_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] {seed : PMF Seed} {hash : Seed → Input → Output} {ε : ENNReal} (hhash : IsUniversalHash seed hash ε) (hε : ε ≠ ⊤) (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 * ε.toReal

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

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. For a universal family this has probability at most the number of other candidates divided by |Output|.

theorem Cslib.Probability.IsUniversalHash.collisionProbability_le {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Finite Input] {seed : PMF Seed} {hash : Seed → Input → Output} {ε : ENNReal} (hhash : IsUniversalHash seed hash ε) (hε : ε ≠ ⊤) (source : PMF Input) : ∑ s : Seed, (seed s).toReal * PMF.collisionProbability (PMF.map (hash s) source) ≤ PMF.collisionProbability source + ε.toReal

An ε-universal family bounds the average collision probability of the hashed source by the collision probability of the source plus ε.

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))⁻¹

A universal family bounds the average collision probability of the hashed source by the collision probability of the source plus 1 / |Output|.

theorem Cslib.Probability.IsUniversalHash.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} {ε : ENNReal} (hhash : IsUniversalHash seed hash ε) (hε : ε ≠ ⊤) (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 + ε.toReal) - 1

Leftover hash lemma for ε-universal families, in squared form: the seed stays public, and independent uniform bits replace the digest, at squared distance at most (|Output| (CP + ε) - 1) / 4, where CP is the collision probability of the source.

theorem Cslib.Probability.IsUniversalHash.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} {ε : ENNReal} (hhash : IsUniversalHash seed hash ε) (hε : ε ≠ ⊤) (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 + ε.toReal) - 1) / 2

Leftover hash lemma for ε-universal families: the seed stays public, and independent uniform bits replace the digest, with error at most √(|Output| (CP + ε) - 1) / 2.

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 for universal families, 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.