Universal finite hash families #
Distinct inputs collide on at most a 1 / card Ω fraction of seeds. The
division-free cardinality condition is meaningful even for empty types;
probability bounds separately require nonempty sampling types. Universality
does not assert independence of the two hash outputs.
This is Definition 2 of Barak, Dodis, Krawczyk, Pereira, Pietrzak, Standaert, and Yu, Leftover Hash Lemma, Revisited (CRYPTO 2011), specialized to exact universality and arbitrary finite output types.
def
Algebraic.Cutwidth.Extractor.UniversalHashFamily
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype Seed]
[Fintype Ω]
(E : α → Seed → Ω)
:
Distinct inputs collide on at most the reciprocal output-cardinality fraction of the uniformly sampled seeds.
Equations
- Algebraic.Cutwidth.Extractor.UniversalHashFamily E = ∀ (x x' : α), x ≠ x' → {y : Seed | E x y = E x' y}.card * Fintype.card Ω ≤ Fintype.card Seed