### Abstract

A k-universal hash family is a probability space of functions, which have uniform distribution and form k-wise independent random variables. They can often be used in place of classic (or cryptographic) hash functions and allow the rigorous analysis of the performance of randomized algorithms and data structures that rely on hash functions. In 1981 Wegman and Carter introduced a generic construction for such families with arbitrary k using polynomials over a finite field. This entry contains a formalization of them and establishes the property of k-universality. To be useful the formalization also provides an explicit construction of finite fields using the factor ring of integers modulo a prime. Additionally, some generic results about independent families are shown that might be of independent interest.

### License

BSD License

### Topics

- Computer science/Algorithms/Randomized

### Session Universal_Hash_Families

- Universal_Hash_Families
- Universal_Hash_Families_More_Independent_Families
- Carter_Wegman_Hash_Family
- Universal_Hash_Families_More_Finite_Fields

### Depends on

- Finite Fields
- Interpolation Polynomials (in HOL-Algebra)

### Used by

- Schönhage-Strassen Multiplication
- Formalization of Randomized Approximation Algorithms for Frequency Moments
- Median Method

### Auto-related entries

- Perfect Fields
- Lehmer’s Theorem

## Cite

×

Universal_Hash_Families-AFP

    @article{Universal_Hash_Families-AFP,
      author  = {Emin Karayel},
      title   = {Universal Hash Families},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Universal_Hash_Families.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 21, 2022 : Isabelle2021-1