ε-Almost Universal Hashing

This file defines the notions

• ε-almost-universal₂ (ε-AU₂)
• ε-almost-strongly-universal₂ (ε-ASU₂)

These are relaxations of HashFamily.universal2 and HashFamily.stronglyUniversal2 where equality/bounds are replaced by ε.

Main definitions

• HashFamily.almostUniversal2 ε H: H is ε-almost-universal₂ (ε-AU₂) if for all distinct x ≠ y: Pr_{s}[H s x = H s y] ≤ ε.

• HashFamily.uniform H: H is uniform if for all hash inputs x and outputs a, Pr_{s}[H s x = a] = 1 / |Output|.

• HashFamily.almostStronglyUniversal2 ε H: H is ε-almost-strongly-universal₂ (ε-ASU₂) if for all distinct inputs x ≠ y and all outputs a b: Pr_{s}[H s x = a ∧ H s y = b] ≤ ε / |Output|. See ([BKST15] Definition 1.1). Note: some papers use a different definition which furthermore requires uniformity, e.g., [S94]. We do not.

Main results

• HashFamily.universal2_iff_probUniform (in Basic): universal2 ↔ almostUniversal2 (1 / |Output|).
• HashFamily.almostUniversal2_mono: ε-AU₂ is monotone in ε.
• HashFamily.almostStronglyUniversal2_mono: ε-ASU₂ is monotone in ε.
• HashFamily.almostUniversal2_of_almostStronglyUniversal2: almostStronglyUniversal2 ε implies almostUniversal2 ε.
• HashFamily.stronglyUniversal2_iff_almostStronglyUniversal2: stronglyUniversal2 ↔ almostStronglyUniversal2 (1 / |Output|).
• HashFamily.almostStronglyUniversal2_of_stronglyUniversal2: stronglyUniversal2 implies almostStronglyUniversal2 (1 / |Output|).
• HashFamily.uniform_of_stronglyUniversal2: stronglyUniversal2 implies uniform.
• HashFamily.almostStronglyUniversal2_eps_lower_bound: almostStronglyUniversal2 ε implies 1 / |Output| ≤ ε.

References

• [BKST15] @misc{cryptoeprint:2015/1187, author = {Khodakhast Bibak and Bruce M. Kapron and Venkatesh Srinivasan and László Tóth}, title = {On an almost-universal hash function family with applications to authentication and secrecy codes}, howpublished = {Cryptology {ePrint} Archive, Paper 2015/1187}, year = {2015}, url = {https://eprint.iacr.org/2015/1187} }

• [S94] @Article{Stinson1994, author={Stinson, D. R.}, title={Universal hashing and authentication codes}, journal={Designs, Codes and Cryptography}, year={1994}, month={Jul}, day={01}, volume={4}, number={3}, pages={369-380}, issn={1573-7586}, doi={10.1007/BF01388651}, url={https://doi.org/10.1007/BF01388651} }

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

[S94] 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|

[S94] 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)

theorem HashFamily.almostUniversal2_mono {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [DecidableEq Output] {ε₁ ε₂ : ℚ} (hε : ε₁ ≤ ε₂) (H : HashFamily Seed Input Output) (h : almostUniversal2 ε₁ H) : almostUniversal2 ε₂ H

theorem HashFamily.almostStronglyUniversal2_mono {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] {ε₁ ε₂ : ℚ} (hε : ε₁ ≤ ε₂) (H : HashFamily Seed Input Output) (h : almostStronglyUniversal2 ε₁ H) : almostStronglyUniversal2 ε₂ H

theorem HashFamily.almostUniversal2_of_almostStronglyUniversal2 {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 : almostStronglyUniversal2 ε H) : almostUniversal2 ε H

theorem HashFamily.almostStronglyUniversal2_of_stronglyUniversal2 {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) (hsu : H.stronglyUniversal2) : almostStronglyUniversal2 (1 / ↑(Fintype.card Output)) H

theorem HashFamily.stronglyUniversal2_iff_almostStronglyUniversal2 {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 ↔ almostStronglyUniversal2 (1 / ↑(Fintype.card Output)) H

stronglyUniversal2 is equivalent to almostStronglyUniversal2 (1 / |Output|). Since 1 / |Output| is the minimum possible ε for any ε-ASU₂ family (see almostStronglyUniversal2_eps_lower_bound), this characterizes strongly universal families as exactly those achieving the tightest possible near-independence bound.

theorem HashFamily.uniform_of_stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] [Nontrivial Input] (H : HashFamily Seed Input Output) (hsu : H.stronglyUniversal2) : H.uniform

theorem HashFamily.almostStronglyUniversal2_eps_lower_bound {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] [Nontrivial Input] {ε : ℚ} (H : HashFamily Seed Input Output) (h : almostStronglyUniversal2 ε H) : 1 / ↑(Fintype.card Output) ≤ ε