ε-Almost Δ-Universal hashing

ε-almost-Δ-universal₂ (ε-A∆U₂), due to [BKST15], Definition 1.1, generalises ε-AU₂ by bounding all difference probabilities, not just the zero-difference (collision) probability. It requires [AddCommGroup Output] to express H s x − H s y.

Special cases of this definition are known by several names in the literature. In particular, if G is the group of length-l strings of bits under element-wise XOR operation, this case has been called -"ε-otp secure" (e.g. Krawczyk94, 10.5555/1755009.1755041)

• ε-almost XOR universal (e.g. Rogaway99, Rogaway1999)

The chain of implications is:

almostStronglyUniversal2 ε → almostDeltaUniversal2 ε → almostUniversal2 ε

The left implication sums the joint bound over all a : Output to bound each difference. The right implication specialises b = 0 (since H s x − H s y = 0 ↔ H s x = H s y).

• HashFamily.almostDeltaUniversal2 ε H (defined in UniversalHashing.Basic): H is ε-A∆U₂ if for all distinct x ≠ y and every b : Output: Pr_{s}[H s x − H s y = b] ≤ ε. [BKST15], Definition 1.1
• HashFamily.almostDeltaUniversal2_mono: ε-A∆U₂ is monotone in ε.
• HashFamily.almostUniversal2_of_almostDeltaUniversal2: A∆U₂ implies AU₂.
• HashFamily.almostDeltaUniversal2_of_almostStronglyUniversal2: ASU₂ implies A∆U₂.

theorem HashFamily.almostDeltaUniversal2_of_deltaUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [AddCommGroup Output] (H : HashFamily Seed Input Output) (h : H.deltaUniversal2) : almostDeltaUniversal2 (1 / ↑(Fintype.card Output)) H

A perfectly Δ-universal family is (1 / |Output|)-A∆U₂ — with the optimal parameter, since for fixed x ≠ y the probabilities Pr[H s x − H s y = b] sum to 1 over b.

theorem HashFamily.almostDeltaUniversal2_mono {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [DecidableEq Output] [AddCommGroup Output] {ε₁ ε₂ : ℚ} (hε : ε₁ ≤ ε₂) (H : HashFamily Seed Input Output) (h : almostDeltaUniversal2 ε₁ H) : almostDeltaUniversal2 ε₂ H

ε-A∆U₂ is monotone in ε: if H is ε₁-A∆U₂ and ε₁ ≤ ε₂, then H is ε₂-A∆U₂.

theorem HashFamily.almostUniversal2_of_almostDeltaUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [DecidableEq Output] [AddCommGroup Output] {ε : ℚ} (H : HashFamily Seed Input Output) (h : almostDeltaUniversal2 ε H) : almostUniversal2 ε H

almostDeltaUniversal2 ε implies almostUniversal2 ε: specialise b = 0, since H s x − H s y = 0 ↔ H s x = H s y.

[BKST15], Definition 1.1, remark

theorem HashFamily.almostDeltaUniversal2_of_almostStronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [AddCommGroup Output] [Nonempty Seed] {ε : ℚ} (H : HashFamily Seed Input Output) (h : almostStronglyUniversal2 ε H) : almostDeltaUniversal2 ε H

almostStronglyUniversal2 ε implies almostDeltaUniversal2 ε: summing the joint bound Pr[H s x = a ∧ H s y = a − b] ≤ ε / |Output| over all a gives Pr[H s x − H s y = b] ≤ ε.

This makes the full implication chain almostStronglyUniversal2 ε → almostDeltaUniversal2 ε → almostUniversal2 ε explicit.

[BKST15], Definition 1.1; implicit in the paper's discussion

theorem HashFamily.almostStronglyUniversal2_of_almostDeltaUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [AddCommGroup Output] {ε : ℚ} (H : HashFamily Seed Input Output) (h : almostDeltaUniversal2 ε H) : almostStronglyUniversal2 (ε * ↑(Fintype.card Output)) H

ε-A∆U₂ implies (ε · |Output|)-ASU₂: each joint probability Pr[H s x = a ∧ H s y = b] equals Pr[H s x − H s y = a − b] (same event after fixing one marginal), which is at most ε by A∆U₂. The ASU₂ bound (ε · |Output|) / |Output| = ε then follows.