Universal Hashing and Carter-Wegman MAC

This file formalizes universal hash families and the Carter-Wegman one-time MAC construction from Chapter 12 of "The Joy of Cryptography".

Main definitions

• UHFamily — universal hash family structure
• boolPairwiseHash — pairwise-independent hash over Bool: H(k₁,k₂)(m) = (k₁∧m) ⊕ k₂
• uh_forge_real, uh_forge_ideal — forgery games
• IsUniversal — universality property

Main results

• boolHash_forge_advantage — forgery advantage ≤ 1/2 for Bool hash
• boolPairwiseHash_is_universal — Bool hash is 1/2-universal

References

• [Rosulek, The Joy of Cryptography, Chapter 12]
• [Carter & Wegman, Universal Classes of Hash Functions, 1979]

Universal Hash Family

structure CatCryptCore.Examples.UniversalHash.UHFamily : Type 1

A universal hash family with collision bound ε.

• KeyType : Type
• MsgType : Type
• TagType : Type
• finKey : Fintype self.KeyType
• neKey : Nonempty self.KeyType
• decEqTag : DecidableEq self.TagType
• hash : self.KeyType → self.MsgType → self.TagType
• epsilon : ENNReal

noncomputable def CatCryptCore.Examples.UniversalHash.boolPairwiseHash : UHFamily

Pairwise-independent hash over Bool.

Equations

• One or more equations did not get rendered due to their size.

Forgery Games

noncomputable def CatCryptCore.Examples.UniversalHash.uh_forge_real (H : UHFamily) (_m m_star : H.MsgType) (t_star : H.TagType) : CatCrypt.Core.SPComp Bool

Real forgery game: sample key, check if adversary's guess matches hash on new message.

Equations

• CatCryptCore.Examples.UniversalHash.uh_forge_real H _m m_star t_star = do let k ← CatCrypt.Core.SPComp.sample H.KeyType CatCrypt.Core.SPComp.pure (t_star == H.hash k m_star)

noncomputable def CatCryptCore.Examples.UniversalHash.uh_forge_ideal : CatCrypt.Core.SPComp Bool

Ideal forgery game: forgery always fails.

Equations

• CatCryptCore.Examples.UniversalHash.uh_forge_ideal = CatCrypt.Core.SPComp.pure false

noncomputable def CatCryptCore.Examples.UniversalHash.UH_Forgery_Advantage (H : UHFamily) (m m_star : H.MsgType) (t_star : H.TagType) (A : Bool → CatCrypt.Core.SPComp Bool) : ENNReal

Forgery advantage.

Equations

• One or more equations did not get rendered due to their size.

IsPure Proofs

theorem CatCryptCore.Examples.UniversalHash.uh_forge_real_isPure (H : UHFamily) (m m_star : H.MsgType) (t_star : H.TagType) : (uh_forge_real H m m_star t_star).IsPure

theorem CatCryptCore.Examples.UniversalHash.uh_forge_ideal_isPure : uh_forge_ideal.IsPure

Arithmetic Helpers

theorem CatCryptCore.Examples.UniversalHash.two_mul_four_inv : 2 * 4⁻¹ = 2⁻¹

2 × 4⁻¹ = 2⁻¹ in ENNReal.

theorem CatCryptCore.Examples.UniversalHash.four_inv_add : 4⁻¹ + 4⁻¹ = 2⁻¹

4⁻¹ + 4⁻¹ = 2⁻¹ in ENNReal.

theorem CatCryptCore.Examples.UniversalHash.four_inv_double (x : ENNReal) : 4⁻¹ * x + 4⁻¹ * x = 2⁻¹ * x

Doubling a quarter gives a half: 4⁻¹x + 4⁻¹x = 2⁻¹*x in ENNReal.

Core prTrue Equality

theorem CatCryptCore.Examples.UniversalHash.forge_prTrue_eq (m m_star t_star : Bool) (h_diff : m_star ≠ m) (A : Bool → CatCrypt.Core.SPComp Bool) (h₀ : CatCrypt.Core.Heap) : CatCrypt.Crypto.prTrue ((uh_forge_real boolPairwiseHash m m_star t_star).bind A) h₀ = CatCrypt.Crypto.prTrue ((CatCrypt.Core.SPComp.sample Bool).bind A) h₀

For the Bool pairwise hash forgery game with m_star ≠ m, the prTrue distribution equals that of uniform Bool sampling.

The proof expands the sums over Bool × Bool, computes the hash values, and uses arithmetic to show the 4-element sum equals the 2-element sum.

Main Security Theorem

theorem CatCryptCore.Examples.UniversalHash.boolHash_forge_advantage (m m_star t_star : Bool) (h_diff : m_star ≠ m) (A : Bool → CatCrypt.Core.SPComp Bool) : UH_Forgery_Advantage boolPairwiseHash m m_star t_star A ≤ 2⁻¹

For the Bool hash, forgery advantage ≤ 1/2. Uses forge_prTrue_eq to show the advantage equals that of sample Bool vs pure false.

theorem CatCryptCore.Examples.UniversalHash.boolPairwiseHash_mac_security (m m_star t_star : Bool) (h_diff : m_star ≠ m) (A : Bool → CatCrypt.Core.SPComp Bool) : UH_Forgery_Advantage boolPairwiseHash m m_star t_star A ≤ boolPairwiseHash.epsilon

Concrete instance: Bool hash MAC security bound.

Collision Game and Universality

noncomputable def CatCryptCore.Examples.UniversalHash.collision_game (H : UHFamily) (m₁ m₂ : H.MsgType) : CatCrypt.Core.SPComp Bool

Collision probability game.

Equations

• CatCryptCore.Examples.UniversalHash.collision_game H m₁ m₂ = do let k ← CatCrypt.Core.SPComp.sample H.KeyType CatCrypt.Core.SPComp.pure (H.hash k m₁ == H.hash k m₂)

def CatCryptCore.Examples.UniversalHash.IsUniversal (H : UHFamily) : Prop

A hash family is ε-universal.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCryptCore.Examples.UniversalHash.collision_prTrue_eq (m₁ m₂ : Bool) (h_ne : m₁ ≠ m₂) (A : Bool → CatCrypt.Core.SPComp Bool) (h₀ : CatCrypt.Core.Heap) : CatCrypt.Crypto.prTrue ((collision_game boolPairwiseHash m₁ m₂).bind A) h₀ = CatCrypt.Crypto.prTrue ((CatCrypt.Core.SPComp.sample Bool).bind A) h₀

Collision prTrue equals uniform Bool prTrue (same argument as forge).

theorem CatCryptCore.Examples.UniversalHash.boolPairwiseHash_is_universal : IsUniversal boolPairwiseHash

The Bool pairwise hash is 1/2-universal.