Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New entry in the AFP: Universal Hash Families


view this post on Zulip Email Gateway (Feb 21 2022 at 19:34):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Universal Hash Families
Emin Karayel

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.

https://www.isa-afp.org/entries/Universal_Hash_Families.html

Enjoy!


Last updated: Jul 15 2022 at 23:21 UTC