Carter–Wegman polynomial evaluation

Over a finite field F, a message m = (a₁, …, a_v) of length at most ℓ is hashed with a key k ∈ F by evaluating a polynomial at k [WC81]:

• polyHash k m = k ^ v + a₁ k ^ (v - 1) + ⋯ + a_v, Boneh and Shoup's Hpoly ([BS23], Equation 7.3). It is ℓ / |F|-universal ([BS23], Lemma 7.2).
• xpolyHash k m = k * polyHash k m, their Hxpoly ([BS23], Equation 7.23). It is (ℓ + 1) / |F|-Δ-universal ([BS23], Lemma 7.8), which is what the Carter–Wegman MAC needs.

The leading k ^ v lets messages of different lengths be compared: the message polynomials are monic of degree v, so distinct messages give distinct polynomials, and the difference of two of them has at most ℓ roots. Both functions are computed by Horner's rule.

Main definitions

• Cslib.Probability.polyHash, Cslib.Probability.xpolyHash: polynomial evaluation hashes.

Main results

• Cslib.Probability.isUniversalHash_polyHash: polyHash is ℓ / |F|-universal.
• Cslib.Probability.isDeltaUniversalHash_xpolyHash: xpolyHash is (ℓ + 1) / |F|-Δ-universal.

References

• M. N. Wegman, J. L. Carter, New Hash Functions and Their Use in Authentication and Set Equality
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 7.2.1 and 7.4.

def Cslib.Probability.polyHash {F : Type u_1} [Field F] (k : F) (m : List F) : F

Boneh and Shoup's Hpoly ([BS23], Equation 7.3): hash the message (a₁, …, a_v) with the key k to k ^ v + a₁ k ^ (v - 1) + ⋯ + a_v, by Horner's rule.

def Cslib.Probability.xpolyHash {F : Type u_1} [Field F] (k : F) (m : List F) : F

Boneh and Shoup's Hxpoly ([BS23], Equation 7.23): k * polyHash k m.

theorem Cslib.Probability.isUniversalHash_polyHash {F : Type u_1} [Field F] [Fintype F] (ℓ : ℕ) : IsUniversalHash (PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => polyHash k ↑m) (↑ℓ / ↑(Fintype.card F))

Hpoly is ℓ / |F|-universal ([BS23], Lemma 7.2): two distinct messages of length at most ℓ collide only at the roots of the nonzero difference of their polynomials.

theorem Cslib.Probability.isDeltaUniversalHash_xpolyHash {F : Type u_1} [Field F] [Fintype F] (ℓ : ℕ) : IsDeltaUniversalHash (PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => xpolyHash k ↑m) ((↑ℓ + 1) / ↑(Fintype.card F))

Hxpoly is (ℓ + 1) / |F|-Δ-universal ([BS23], Lemma 7.8): a difference d of the hashes of two distinct messages occurs only at the roots of the nonzero polynomial X (f - g) - d of degree at most ℓ + 1.