Toeplitz hashing

Over a finite field F, the maps x ↦ T x + v from F^n to F^m, for a uniformly random m × n Toeplitz matrix T (Matrix.toeplitz) and an independent uniformly random vector v, form a pairwise independent hash family (Cslib.Probability.isPairwiseIndependentHash_toeplitzHash) Katz and Lindell, Exercise 4.26. This is the affine family Cslib.Probability.affineHash restricted to Toeplitz matrices, with seeds of n + 2 m - 1 field elements instead of m n + m (Cslib.Probability.card_toeplitzHash_seed). The proof uses the shift criterion Cslib.Probability.isPairwiseIndependentHash_add_of_surjective: for every nonzero d : F^n, the Toeplitz matrices T reach every vector T d (Matrix.toeplitz_mulVec_surjective).

Main definitions

• Cslib.Probability.toeplitzHash: the map x ↦ T x + v with seed a Toeplitz matrix T and a vector v.

Main results

• Cslib.Probability.isPairwiseIndependentHash_toeplitzHash: the Toeplitz hash family over a finite field is pairwise independent.
• Cslib.Probability.card_toeplitzHash_seed: its seeds consist of n + 2 m - 1 field elements.

References

• J. Katz, Y. Lindell, Introduction to Modern Cryptography, Section 4.6

def Cslib.Probability.toeplitzHash {F : Type u_1} {m n : ℕ} [NonUnitalNonAssocSemiring F] (p : (Fin (m + n - 1) → F) × (Fin m → F)) (x : Fin n → F) : Fin m → F

The affine map x ↦ T x + v from F^n to F^m, with seed (a, v) where T is the Toeplitz matrix Matrix.toeplitz a with diagonals a [Katz and Lindell, Exercise 4.26] [KL20].

@[simp]

theorem Cslib.Probability.toeplitzHash_apply {F : Type u_1} {m n : ℕ} [NonUnitalNonAssocSemiring F] (a : Fin (m + n - 1) → F) (v : Fin m → F) (x : Fin n → F) : toeplitzHash (a, v) x = (Matrix.toeplitz a).mulVec x + v

The Toeplitz hash with seed (a, v) sends x to T x + v, where T = Matrix.toeplitz a.

theorem Cslib.Probability.toeplitzHash_eq_affineHash {F : Type u_1} {m n : ℕ} [NonUnitalNonAssocSemiring F] (p : (Fin (m + n - 1) → F) × (Fin m → F)) : toeplitzHash p = affineHash (Matrix.toeplitz p.1, p.2)

The Toeplitz hash is the affine hash Cslib.Probability.affineHash restricted to Toeplitz matrices.

theorem Cslib.Probability.isPairwiseIndependentHash_toeplitzHash {F : Type u_1} {m n : ℕ} [Field F] [Fintype F] [DecidableEq F] : IsPairwiseIndependentHash toeplitzHash

Toeplitz hashing is pairwise independent: over a finite field F, the maps x ↦ T x + v from F^n to F^m, for a uniformly random m × n Toeplitz matrix T and an independent uniformly random vector v, form a pairwise independent hash family Katz and Lindell, Exercise 4.26.

theorem Cslib.Probability.card_toeplitzHash_seed {F : Type u_1} {m n : ℕ} [Fintype F] : Fintype.card ((Fin (m + n - 1) → F) × (Fin m → F)) = Fintype.card F ^ (n + 2 * m - 1)

The seed length of Toeplitz hashing: the Toeplitz hash family from F^n to F^m has |F| ^ (n + 2 m - 1) seeds, m + n - 1 field elements for the matrix and m for the offset. The affine family Cslib.Probability.affineHash with the same domain and range has |F| ^ (m n + m) seeds, which is at least as many once m and n are positive, and strictly more once they both exceed 1.