Bounds for ε-Almost Universal Hashing

Main results

• HashFamily.card_seed_lb_of_almostStronglyUniversal2: Every uniform ε-ASU₂ family (i.e. HashFamily.uniform H ∧ H.almostStronglyUniversal2 ε) satisfies |Seed| ≥ 1 + |Input| (|Output| − 1)² / (|Output| ε (|Input| − 1) + |Output| − |Input|). [S94, Theorem 4.3]
• HashFamily.card_seed_lb_of_stronglyUniversal2: Every strongly-universal₂ family satisfies |Seed| ≥ 1 + |Input| (|Output| − 1). [S94, Corollary 4.4]
• HashFamily.exists_collision_lb: For any hash family with |Input| > |Output|, some pair of distinct inputs has collision probability at least (|Input| − |Output|) / (|Output| (|Input| − 1)). [S94, Theorem 3.1]
• HashFamily.almostUniversal2_comp: Composing an ε₁-AU₂ family with an ε₂-AU₂ family yields an (ε₁ + ε₂)-AU₂ family. [S94, Theorem 5.4]

theorem HashFamily.card_seed_lb_of_almostStronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Input] [Fintype Output] [DecidableEq Output] [Nonempty Seed] [Nontrivial Input] {ε : ℚ} (H : HashFamily Seed Input Output) (h_unif : H.uniform) (hH : almostStronglyUniversal2 ε H) : 1 + ↑(Fintype.card Input) * (↑(Fintype.card Output) - 1) ^ 2 / (↑(Fintype.card Output) * ε * (↑(Fintype.card Input) - 1) + ↑(Fintype.card Output) - ↑(Fintype.card Input)) ≤ ↑(Fintype.card Seed)

Every uniform ε-ASU₂ hash family (i.e. HashFamily.uniform H ∧ H.almostStronglyUniversal2 ε) satisfies |Seed| ≥ 1 + |Input|·(|Output|−1)² / (|Output|·ε·(|Input|−1) + |Output| − |Input|).

[S94, Theorem 4.3]

theorem HashFamily.card_seed_lb_of_stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Input] [Fintype Output] [DecidableEq Output] [Nonempty Seed] [Nontrivial Input] (H : HashFamily Seed Input Output) (hH : H.stronglyUniversal2) : 1 + Fintype.card Input * (Fintype.card Output - 1) ≤ Fintype.card Seed

Every strongly-universal₂ hash family satisfies |Seed| ≥ 1 + |Input| · (|Output| − 1).

[S94, Corollary 4.4]

theorem HashFamily.exists_collision_lb {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Input] [Fintype Output] [DecidableEq Output] [Nonempty Seed] (H : HashFamily Seed Input Output) (hlt : Fintype.card Output < Fintype.card Input) : ∃ (x : Input) (y : Input), x ≠ y ∧ (↑(Fintype.card Input) - ↑(Fintype.card Output)) / (↑(Fintype.card Output) * (↑(Fintype.card Input) - 1)) ≤ probUniform fun (s : Seed) => H s x = H s y

For any hash family, when |Input| > |Output|, some pair of distinct inputs has collision probability at least (|Input| − |Output|) / (|Output| · (|Input| − 1)).

This gives the optimality threshold: no family can be ε-AU for ε below this value.

[S94, Theorem 3.1]

theorem HashFamily.almostUniversal2_comp {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {Seed₁ : Type u_3} {Seed₂ : Type u_4} {Middle : Type u_5} [Fintype Seed₁] [Fintype Seed₂] [DecidableEq Middle] {ε₁ ε₂ : ℚ} (hε₂ : 0 ≤ ε₂) {H₁ : HashFamily Seed₁ Input Middle} {H₂ : HashFamily Seed₂ Middle Output} (h₁ : almostUniversal2 ε₁ H₁) (h₂ : almostUniversal2 ε₂ H₂) : almostUniversal2 (ε₁ + ε₂) fun (s : Seed₁ × Seed₂) (x : Input) => H₂ s.2 (H₁ s.1 x)

Composing an ε₁-AU family with an ε₂-AU family yields an (ε₁ + ε₂)-AU family.

Given H₁ : Seed₁ → Input → Middle and H₂ : Seed₂ → Middle → Output, the family fun (s₁, s₂) x ↦ H₂ s₂ (H₁ s₁ x) is (ε₁ + ε₂)-AU.

[S94, Theorem 5.4]