Universal and Δ-universal hash families

A keyed hash family is a function h : ι → X → Y together with a law seed : PMF ι of its key, or seed. Two collision properties of such families are defined here, for an arbitrary seed law:

• IsUniversalHash seed h ε: distinct inputs collide with probability at most ε. This is an ε-bounded universal hash function, or ε-UHF ([BS23], Definition 7.2); for ε = 1 / |Y| it is the universal family of Carter and Wegman [CW79] (Cslib.Probability.IsTwoUniversal).
• IsDeltaUniversalHash seed h ε, for an additive group Y: for distinct inputs, every difference of their hashes has probability at most ε. This is an ε-almost-Δ-universal family; it is ε-almost-XOR-universal (ε-AXU) when Y is a space of bit strings, and an ε-bounded difference unpredictable function, or ε-DUF ([BS23], Definition 7.5).

A Δ-universal family is universal, taking the difference 0 (IsDeltaUniversalHash.isUniversalHash). Strongly universal, that is pairwise independent, families with uniform seeds are Cslib.Probability.IsPairwiseIndependentHash; they are universal and Δ-universal with ε = 1 / |Y| (Complexity.Probability.PairwiseIndependentHash.Universal). A uniformly distributed difference gives the optimal ε = 1 / |Y| (IsDeltaUniversalHash.of_map_sub_eq_uniform). Further families are Carter–Wegman polynomial evaluation (Complexity.Probability.HashFamily.Polynomial) and multiply-shift hashing (Complexity.Probability.HashFamily.MultiplyShift).

Probabilities are taken with PMF.toOuterMeasure and bounds are extended nonnegative reals. These are information-theoretic properties; efficient evaluation is a separate matter.

Main definitions

• Cslib.Probability.IsUniversalHash: ε-universal families.
• Cslib.Probability.IsDeltaUniversalHash: ε-almost-Δ-universal families.

Main results

• Cslib.Probability.IsDeltaUniversalHash.isUniversalHash: Δ-universal families are universal.
• Cslib.Probability.IsUniversalHash.precompose, Cslib.Probability.IsUniversalHash.precompose_seed: injective input encodings and pushed-forward seeds.
• Cslib.Probability.IsUniversalHash.sum_ite_toReal_le: the collision bound as a finite sum.
• Cslib.Probability.IsDeltaUniversalHash.of_map_sub_eq_uniform: uniform differences.
• Cslib.Probability.IsUniversalHash.of_card_le, Cslib.Probability.IsDeltaUniversalHash.of_card_le: counting bad seeds of a uniform seed.

References

• J. L. Carter, M. N. Wegman, Universal Classes of Hash Functions
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 7.1 and 7.4.

def Cslib.Probability.IsUniversalHash {ι : Type u_1} {X : Type u_3} {Y : Type u_5} (seed : PMF ι) (hash : ι → X → Y) (ε : ENNReal) : Prop

An ε-universal hash family ([BS23], Definition 7.2): for distinct inputs x and x', the seed i gives hash i x = hash i x' with probability at most ε.

def Cslib.Probability.IsDeltaUniversalHash {ι : Type u_1} {X : Type u_3} {Y : Type u_5} [AddGroup Y] (seed : PMF ι) (hash : ι → X → Y) (ε : ENNReal) : Prop

An ε-almost-Δ-universal hash family ([BS23], Definition 7.5, where it is called an ε-DUF; ε-AXU when the difference is XOR): for distinct inputs x and x' and every d, the seed i gives hash i x - hash i x' = d with probability at most ε.

theorem Cslib.Probability.IsUniversalHash.mono {ι : Type u_1} {X : Type u_3} {Y : Type u_5} {seed : PMF ι} {hash : ι → X → Y} {ε ε' : ENNReal} (hh : IsUniversalHash seed hash ε) (hε : ε ≤ ε') : IsUniversalHash seed hash ε'

A family that is ε-universal is ε'-universal for every ε' ≥ ε.

theorem Cslib.Probability.IsUniversalHash.precompose {ι : Type u_1} {X : Type u_3} {X' : Type u_4} {Y : Type u_5} {seed : PMF ι} {hash : ι → X → Y} {ε : ENNReal} (hh : IsUniversalHash seed hash ε) {encode : X' → X} (hencode : Function.Injective encode) : IsUniversalHash seed (fun (i : ι) (x : X') => hash i (encode x)) ε

An injective input encoding preserves universality.

theorem Cslib.Probability.IsUniversalHash.precompose_seed {ι : Type u_1} {ι' : Type u_2} {X : Type u_3} {Y : Type u_5} {hash : ι → X → Y} {ε : ENNReal} (seed : PMF ι') (prepare : ι' → ι) (hh : IsUniversalHash (PMF.map prepare seed) hash ε) : IsUniversalHash seed (fun (i : ι') => hash (prepare i)) ε

Universality for a pushed-forward seed law is universality of the precomposed family.

theorem Cslib.Probability.IsUniversalHash.sum_ite_toReal_le {ι : Type u_1} {X : Type u_3} {Y : Type u_5} {seed : PMF ι} {hash : ι → X → Y} {ε : ENNReal} [Fintype ι] (hh : IsUniversalHash seed hash ε) (hε : ε ≠ ⊤) {x x' : X} (hx : x ≠ x') : (∑ i : ι, if hash i x = hash i x' then (seed i).toReal else 0) ≤ ε.toReal

On a finite seed space, the collision probability of distinct inputs is a sum of seed masses bounded by ε.

theorem Cslib.Probability.IsUniversalHash.of_sum_ite_toReal_le {ι : Type u_1} {X : Type u_3} {Y : Type u_5} {seed : PMF ι} {hash : ι → X → Y} [Fintype ι] {ε : ℝ} (hh : ∀ (x x' : X), x ≠ x' → (∑ i : ι, if hash i x = hash i x' then (seed i).toReal else 0) ≤ ε) : IsUniversalHash seed hash (ENNReal.ofReal ε)

A collision bound stated as a finite sum of seed masses gives universality.

theorem Cslib.Probability.IsUniversalHash.of_card_le {ι : Type u_1} {X : Type u_3} {Y : Type u_5} {hash : ι → X → Y} [Fintype ι] [Nonempty ι] [DecidableEq Y] {c : ℕ} (hc : ∀ (x x' : X), x ≠ x' → {i : ι | hash i x = hash i x'}.card ≤ c) : IsUniversalHash (PMF.uniformOfFintype ι) hash (↑c / ↑(Fintype.card ι))

With a uniform seed, a bound c on the number of seeds on which two distinct inputs collide gives c / |ι|-universality.

theorem Cslib.Probability.IsDeltaUniversalHash.isUniversalHash {ι : Type u_1} {X : Type u_3} {Y : Type u_5} [AddGroup Y] {seed : PMF ι} {hash : ι → X → Y} {ε : ENNReal} (hh : IsDeltaUniversalHash seed hash ε) : IsUniversalHash seed hash ε

A Δ-universal family is universal with the same bound: take the difference 0.

theorem Cslib.Probability.IsDeltaUniversalHash.mono {ι : Type u_1} {X : Type u_3} {Y : Type u_5} [AddGroup Y] {seed : PMF ι} {hash : ι → X → Y} {ε ε' : ENNReal} (hh : IsDeltaUniversalHash seed hash ε) (hε : ε ≤ ε') : IsDeltaUniversalHash seed hash ε'

A family that is ε-Δ-universal is ε'-Δ-universal for every ε' ≥ ε.

theorem Cslib.Probability.IsDeltaUniversalHash.precompose {ι : Type u_1} {X : Type u_3} {X' : Type u_4} {Y : Type u_5} [AddGroup Y] {seed : PMF ι} {hash : ι → X → Y} {ε : ENNReal} (hh : IsDeltaUniversalHash seed hash ε) {encode : X' → X} (hencode : Function.Injective encode) : IsDeltaUniversalHash seed (fun (i : ι) (x : X') => hash i (encode x)) ε

An injective input encoding preserves Δ-universality.

theorem Cslib.Probability.IsDeltaUniversalHash.precompose_seed {ι : Type u_1} {ι' : Type u_2} {X : Type u_3} {Y : Type u_5} [AddGroup Y] {hash : ι → X → Y} {ε : ENNReal} (seed : PMF ι') (prepare : ι' → ι) (hh : IsDeltaUniversalHash (PMF.map prepare seed) hash ε) : IsDeltaUniversalHash seed (fun (i : ι') => hash (prepare i)) ε

Δ-universality for a pushed-forward seed law is Δ-universality of the precomposed family.

theorem Cslib.Probability.IsDeltaUniversalHash.of_map_sub_eq_uniform {ι : Type u_1} {X : Type u_3} {Y : Type u_5} [AddGroup Y] {seed : PMF ι} {hash : ι → X → Y} [Fintype Y] [Nonempty Y] (hh : ∀ (x x' : X), x ≠ x' → PMF.map (fun (i : ι) => hash i x - hash i x') seed = PMF.uniformOfFintype Y) : IsDeltaUniversalHash seed hash (↑(Fintype.card Y))⁻¹

If distinct inputs always have a uniformly distributed difference of hashes, the family is 1 / |Y|-Δ-universal, the least possible bound.

theorem Cslib.Probability.IsDeltaUniversalHash.of_card_le {ι : Type u_1} {X : Type u_3} {Y : Type u_5} [AddGroup Y] {hash : ι → X → Y} [Fintype ι] [Nonempty ι] [DecidableEq Y] {c : ℕ} (hc : ∀ (x x' : X), x ≠ x' → ∀ (d : Y), {i : ι | hash i x - hash i x' = d}.card ≤ c) : IsDeltaUniversalHash (PMF.uniformOfFintype ι) hash (↑c / ↑(Fintype.card ι))

With a uniform seed, a bound c on the number of seeds giving any one difference of the hashes of two distinct inputs gives c / |ι|-Δ-universality.