This module defines notions of universality for families of hash functions.

A hash family is a family of functions Input → Output. Rather than define it as a set of functions, we put the choice of function into a type Seed.

Universal-2

A function hash : Seed → Input → Output is Universal-2 if for any distinct inputs x and y, the probability over a uniform random seed that hash s x = hash s y is at most 1 / |Output|.

This is formalized as (number of seeds causing collision) * |Output| ≤ |Seed|.

We also give an alternative definition, proven equivalent, which the AIs seem to like more. Let's see which we keep in the end...

Strongly-universal-n

A family H is strongly universal (also known as "pairwise independent") if for all x ≠ y and all a b : Output, \Pr_i [h_i(x) = a ∧ h_i(y) = b] = 1 / |Output|^2

@[reducible, inline]

abbrev HashFamily (Seed : Type u_1) (Input : Type u_2) (Output : Type u_3) : Type (max (max u_1 u_2) u_3)

A hash family is a family of functions Input → Output. Rather than define it as a set of functions, we put the choice of function into a type Seed.

Equations

• HashFamily Seed Input Output = (Seed → Input → Output)

def HashFamily.universal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (hash : HashFamily Seed Input Output) : Prop

A hash function taking a seed and an input is universal-2 if for any distinct inputs x and y, the probability (over the seed) of a collision is at most 1/|Output|.

This is expressed as: (number of seeds causing collision) * |Output| ≤ |Seed|.

Equations

• hash.universal2 = ∀ ⦃x y : Input⦄, x ≠ y → Fintype.card ↑{s : Seed | hash s x = hash s y} * Fintype.card Output ≤ Fintype.card Seed

theorem HashFamily.universal2_of_seed_empty {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (hash : HashFamily Seed Input Output) [IsEmpty Seed] : hash.universal2

def probUniform {Seed : Type u_1} [Fintype Seed] (p : Seed → Prop) [DecidablePred p] : ℚ

The uniform probability of a predicate on Seed, modeled by counting.

Equations

• probUniform p = ↑(Fintype.card { i : Seed // p i }) / ↑(Fintype.card Seed)

theorem probUniform_congr {Seed : Type u_1} [Fintype Seed] {p q : Seed → Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (s : Seed), p s ↔ q s) : probUniform p = probUniform q

probUniform respects pointwise-equivalent predicates.

theorem probUniform_eq_of_additive_surjective {Seed : Type u_4} {Output : Type u_5} [Fintype Seed] [Fintype Output] [DecidableEq Output] [AddCommGroup Seed] [AddCommGroup Output] {f : Seed → Output} (hadd : ∀ (s t : Seed), f (s + t) = f s + f t) (hsurj : Function.Surjective f) (b : Output) : (probUniform fun (s : Seed) => f s = b) = 1 / ↑(Fintype.card Output)

Fibers of an additive surjection between finite additive groups are equiprobable: each value is hit with probability exactly 1 / |Output|.

This is the counting core behind perfect Δ-universality of linear hash families (all fibers are cosets of the kernel, hence equinumerous).

theorem probUniform_comp_equiv {Seed : Type u_1} [Fintype Seed] {Seed2 : Type u_4} [Fintype Seed2] (e : Seed2 ≃ Seed) (p : Seed → Prop) [DecidablePred p] : (probUniform fun (s : Seed2) => p (e s)) = probUniform p

probUniform is invariant under reindexing the seed space by an equivalence.

theorem probUniform_prod {S₁ : Type u_4} {S₂ : Type u_5} [Fintype S₁] [Fintype S₂] (P : S₁ → S₂ → Prop) [(s₁ : S₁) → (s₂ : S₂) → Decidable (P s₁ s₂)] : ↑(Fintype.card { s : S₁ × S₂ // P s.1 s.2 }) / ↑(Fintype.card (S₁ × S₂)) = (∑ s₁ : S₁, ↑(Fintype.card { s₂ : S₂ // P s₁ s₂ }) / ↑(Fintype.card S₂)) / ↑(Fintype.card S₁)

The probability of an event on a product seed space factors over the first coordinate: Pr_{s₁×s₂}[P] = (∑ s₁, Pr_{s₂}[P s₁]) / |S₁|.

theorem HashFamily.universal2_iff_probUniform {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) : H.universal2 ↔ ∀ ⦃x y : Input⦄, x ≠ y → (probUniform fun (i : Seed) => H i x = H i y) ≤ 1 / ↑(Fintype.card Output)

Alternative (equivalent) statement of universal-2 using probUniform.

A family H is universal2 if for all distinct x ≠ y, the collision probability is at most 1 / |Output|:

Pr_i [h_i(x) = h_i(y)] ≤ 1 / |Output|

def HashFamily.stronglyUniversal_n {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (n : ℕ) (H : HashFamily Seed Input Output) : Prop

A hash family is strongly-universal-n (also called "n-wise independent") if

• given n distinct inputs a₁, a₂, ...
• and n (not necessarily distinct) outputs b₁, b₂, ..., exactly |HashFamily|/(|Output|^n) functions take a₁ to b₁ a₂ to b₂, etc.

See [WC81]

Equations

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

def HashFamily.stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) : Prop

Special case: a family H is strongly-universal-2 (also known as just "strongly universal", or "pairwise independent") if for all x ≠ y and all a b : Output, \Pr_i [h_i(x) = a ∧ h_i(y) = b] = 1 / |Output|^2.

Equations

• H.stronglyUniversal2 = ∀ ⦃x y : Input⦄, x ≠ y → ∀ (a b : Output), ↑(Fintype.card { i : Seed // H i x = a ∧ H i y = b }) = ↑(Fintype.card Seed) / ↑(Fintype.card Output) ^ 2

ε-almost universality

Relaxations of HashFamily.universal2 and HashFamily.stronglyUniversal2 where equality/bounds are replaced by a parameter ε. Theorems about these notions live in UniversalHashing.AlmostUniversal and UniversalHashing.DeltaUniversal.

def HashFamily.almostUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [DecidableEq Output] (ε : ℚ) (H : HashFamily Seed Input Output) : Prop

A hash family is ε-almost-universal₂ (ε-AU₂) with parameter ε : ℚ if for any two distinct inputs x and y, the probability over a uniform random seed of a collision is at most ε:

Pr_{s}[H s x = H s y] ≤ ε

HashFamily.universal2 is the special case ε = 1 / |Output|; see HashFamily.universal2_iff_probUniform.

Definition 1.1 in [BKST15].

Equations

• HashFamily.almostUniversal2 ε H = ∀ ⦃x y : Input⦄, x ≠ y → (probUniform fun (s : Seed) => H s x = H s y) ≤ ε

def HashFamily.almostStronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (ε : ℚ) (H : HashFamily Seed Input Output) : Prop

A hash family is ε-almost-strongly-universal₂ (ε-ASU₂) with parameter ε : ℚ if for every pair of distinct inputs x ≠ y and all outputs a, b:

Pr_{s}[H s x = a ∧ H s y = b] ≤ ε / |Output|

HashFamily.stronglyUniversal2 is the special case ε = 1 / |Output| where the bound is tight; see HashFamily.stronglyUniversal2_iff_almostStronglyUniversal2.

Definition 1.1 in [BKST15]. This is the prevalent definition in modern literature.

Relationship to alternative definitions

[Sti94] additionally requires uniformity Pr_{s}[H s x = a] = 1 / |Output| (see HashFamily.uniform), i.e., the conjunction H.uniform ∧ H.almostStronglyUniversal2 ε.

The uniformity condition is motivated by Wegman–Carter MACs, where it ensures that observing a tag (m, t) reveals no information about the key. The two definitions coincide when ε = 1 / |Output| (the strongly-universal case): the joint bound then forces all marginals to equal 1 / |Output|, implying uniformity.

Equations

• HashFamily.almostStronglyUniversal2 ε H = ∀ ⦃x y : Input⦄, x ≠ y → ∀ (a b : Output), (probUniform fun (s : Seed) => H s x = a ∧ H s y = b) ≤ ε / ↑(Fintype.card Output)

def HashFamily.uniform {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) : Prop

A hash family is uniform if every input maps to every output with equal probability:

Pr_{s}[H s x = a] = 1 / |Output|

[Sti94] defines ε-ASU₂ as the conjunction H.uniform ∧ H.almostStronglyUniversal2 ε; see HashFamily.almostStronglyUniversal2 for a discussion of the two definitions and when they coincide.

Equations

• H.uniform = ∀ (x : Input) (a : Output), (probUniform fun (s : Seed) => H s x = a) = 1 / ↑(Fintype.card Output)

def HashFamily.almostDeltaUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [DecidableEq Output] [AddCommGroup Output] (ε : ℚ) (H : HashFamily Seed Input Output) : Prop

A hash family is ε-almost-Δ-universal₂ (ε-A∆U₂) with parameter ε : ℚ if for any two distinct inputs x and y and every group element b : Output:

Pr_{s}[H s x − H s y = b] ≤ ε

This is strictly stronger than almostUniversal2 (which only bounds the b = 0 case) and strictly weaker than almostStronglyUniversal2 (which bounds joint probabilities).

Definition 1.1 in [BKST15].

When Seed = Fin ℓ → ZMod 2, Input = Fin m → ZMod 2, Output = Fin n → ZMod 2, this is equivalent to Krawczyk's ε-otp-security (Definition 1 in [Kra95]) with uniform key distribution: for any distinct M ≠ M' and any target b, Pr_{k uniform}[H(k, M') − H(k, M) = b] ≤ ε.

Equations

• HashFamily.almostDeltaUniversal2 ε H = ∀ ⦃x y : Input⦄, x ≠ y → ∀ (b : Output), (probUniform fun (s : Seed) => H s x - H s y = b) ≤ ε

def HashFamily.deltaUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [AddCommGroup Output] (H : HashFamily Seed Input Output) : Prop

A hash family is Δ-universal₂ (perfectly Δ-universal) if for any two distinct inputs x and y, every difference value is attained with exactly the uniform probability:

Pr_{s}[H s x − H s y = b] = 1 / |Output|

This is almostDeltaUniversal2 with the smallest possible parameter ε = 1 / |Output|, attained with equality (see HashFamily.almostDeltaUniversal2_of_deltaUniversal2; no smaller ε is possible for any family, since for fixed x ≠ y the probabilities sum to 1 over b : Output).

Over the group Fin n → ZMod 2 (bit strings under XOR) this property is commonly called XOR-universality.

Equations

• H.deltaUniversal2 = ∀ ⦃x y : Input⦄, x ≠ y → ∀ (b : Output), (probUniform fun (s : Seed) => H s x - H s y = b) = 1 / ↑(Fintype.card Output)

def HashFamily.additive {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Add Input] [Add Output] (H : HashFamily Seed Input Output) : Prop

A hash family is additive (Krawczyk's "⊕-linear" over bit strings) if every member is an additive map: H s (x + y) = H s x + H s y.

Definition 2 in [Kra94].

Equations

• H.additive = ∀ (s : Seed) (x y : Input), H s (x + y) = H s x + H s y

def HashFamily.balanced {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [DecidableEq Output] [Zero Input] (ε : ℚ) (H : HashFamily Seed Input Output) : Prop

A hash family is ε-balanced if no nonzero input concentrates on any output value:

Pr_{s}[H s x = c] ≤ ε for all x ≠ 0 and all c.

For additive families this is equivalent to almostDeltaUniversal2 ε (HashFamily.additive_balanced_iff_almostDeltaUniversal2).

Definition 3 in [Kra94].

Equations

• HashFamily.balanced ε H = ∀ ⦃x : Input⦄, x ≠ 0 → ∀ (c : Output), (probUniform fun (s : Seed) => H s x = c) ≤ ε

def HashFamily.almostCollisionFlatUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (ε : ℚ) (H : HashFamily Seed Input Output) : Prop

A hash family is ε-almost collision-flat universal₂ (ε-ACFU₂) if it is uniform and no specific collision value is hit too often:

Pr_{s}[H s x = a ∧ H s y = a] ≤ ε / |Output| for all x ≠ y and all a.

Sits strictly between ε-ASU₂ (with uniformity) and ε-AU₂; see [Wiese, Boche 2024, Lemma 1.2] (ε-Almost Collision-Flat Universal Hash Functions and Mosaics of Designs).

Equations

• HashFamily.almostCollisionFlatUniversal2 ε H = (H.uniform ∧ ∀ ⦃x y : Input⦄, x ≠ y → ∀ (a : Output), (probUniform fun (s : Seed) => H s x = a ∧ H s y = a) ≤ ε / ↑(Fintype.card Output))

theorem HashFamily.stronglyUniversal2_iff_probUniform {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] (H : HashFamily Seed Input Output) : H.stronglyUniversal2 ↔ ∀ ⦃x y : Input⦄, x ≠ y → ∀ (a b : Output), (probUniform fun (i : Seed) => H i x = a ∧ H i y = b) = 1 / ↑(Fintype.card Output) ^ 2

Equivalent statement of strongly-universal-2 using probUniform.

A family H is stronglyUniversal2 if for all distinct x ≠ y, given two outputs a and b, the probability to map x ↦ a and y ↦ b is exactly 1 / (|Output|^2).

theorem HashFamily.stronglyUniversal2_stronglyUniversal_n_2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Inhabited Seed] (H : HashFamily Seed Input Output) : H.stronglyUniversal2 ↔ stronglyUniversal_n 2 H

stronglyUniversal2 is a special case of strongly_universal_n for n = 2.

theorem HashFamily.universal2_of_stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) : H.stronglyUniversal2 → H.universal2

stronglyUniversal2 implies universal2.

theorem stronglyUniversal_n_of_gt_card {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Fintype Input] (n : ℕ) (H : HashFamily Seed Input Output) (h : Fintype.card Input < n) : HashFamily.stronglyUniversal_n n H

If n is greater than the cardinality of the input space, then any hash family is strongly universal-n (vacuously).

theorem HashFamily.universal2_of_comp_injective_seed {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] (H : HashFamily Seed Input Output) {f : Seed → Seed} (hf : Function.Injective f) : H.universal2 ↔ universal2 (H ∘ f)

The composition of a universal2 function with an injective function is universal2.

theorem HashFamily.universal2_of_comp_bijective {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] {Seed2 : Type u_4} [Fintype Seed2] (H : HashFamily Seed Input Output) {f : Seed2 → Seed} (hf : Function.Bijective f) : H.universal2 ↔ universal2 (H ∘ f)