MAC (Message Authentication Code) EUF-CMA Security

This file defines the EUF-CMA security notion for MAC schemes at the abstract CryptoWord W level.

MAC Games

The MAC security game captures the difficulty of forging a valid tag:

• Real: tag is computed using the secret MAC key
• Ideal: tag is a random value (unforgeable)

For game-hopping proofs (SSH, Kerberos), we use an indistinguishability formulation rather than existential forgery, which is equivalent up to a factor of 1/|W| for single-query adversaries.

Cross-Validation

Property	This file	Textbook
Game structure	MAC_Game_Real/Ideal	Boneh-Shoup Def. 6.1 (PRF)
Advantage	Advantage(Real, Ideal)	|Pr[W₀] - Pr[W₁]|
Formulation	Indistinguishability (real vs random tag)	Equiv. to SUF-CMA for single query

Note: This uses an indistinguishability formulation rather than EUF-CMA (existential unforgeability). The two are equivalent up to a factor of 1/|W| for single-query adversaries. The indistinguishability formulation composes better with game-hopping.

Equivalent formalizations:

• CryptoVerif: SUF-CMA(mac, verify, key) macro

References

• Bellare, Kilian, Rogaway. The Security of the Cipher Block Chaining Message Authentication Code. JCSS 2000.
• Boneh & Shoup, A Graduate Course in Applied Cryptography, §6.3
• Cade, Blanchet. From Computationally-Proved Protocol Specifications to Implementations. JCS 2015.

MAC Definition

structure CatCrypt.Crypto.Assumptions.MACDef (W : Type) [SampleableType W] : Type

Abstract MAC scheme definition, parametric over SampleableType W.

• mac key message → tag
• verify key message tag → Bool

• mac : W → W → W

  MAC computation: (key, message) → tag

• verify : W → W → W → Bool

  MAC verification: (key, message, tag) → Bool

MAC Games

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.MAC_Adversary (W : Type) : Type

Type of MAC adversary: receives a (message, tag) pair and must distinguish real MAC from random tag.

Equations

• CatCrypt.Crypto.Assumptions.MAC_Adversary W = (W → CatCrypt.Core.SPComp Bool)

noncomputable def CatCrypt.Crypto.Assumptions.MAC_Game_Real {W : Type} [SampleableType W] (D : MACDef W) (msg : W) (A : MAC_Adversary W) : Core.SPComp Bool

MAC real game: sample random key, compute tag on adversary's message.

Equations

• CatCrypt.Crypto.Assumptions.MAC_Game_Real D msg A = do let key ← CatCrypt.Core.SPComp.sample W have tag : W := D.mac key msg A tag

noncomputable def CatCrypt.Crypto.Assumptions.MAC_Game_Ideal {W : Type} [SampleableType W] (A : MAC_Adversary W) : Core.SPComp Bool

MAC ideal game: adversary receives a random tag.

Equations

• CatCrypt.Crypto.Assumptions.MAC_Game_Ideal A = do let tag ← CatCrypt.Core.SPComp.sample W A tag

noncomputable def CatCrypt.Crypto.Assumptions.MAC_Advantage {W : Type} [SampleableType W] (D : MACDef W) (msg : W) (A : MAC_Adversary W) : ENNReal

MAC advantage: ability to distinguish real tag from random.

Equations

• CatCrypt.Crypto.Assumptions.MAC_Advantage D msg A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.Assumptions.MAC_Game_Real D msg A) (CatCrypt.Crypto.Assumptions.MAC_Game_Ideal A)

IsPure Proofs

theorem CatCrypt.Crypto.Assumptions.MAC_Game_Real_isPure {W : Type} [SampleableType W] (D : MACDef W) (msg : W) (A : MAC_Adversary W) (hA : ∀ (x : W), (A x).IsPure) : (MAC_Game_Real D msg A).IsPure

theorem CatCrypt.Crypto.Assumptions.MAC_Game_Ideal_isPure {W : Type} [SampleableType W] (A : MAC_Adversary W) (hA : ∀ (x : W), (A x).IsPure) : (MAC_Game_Ideal A).IsPure

Keyed MAC Games (KDM + Key Leakage)

Non-Standard Assumption

MAC_Keyed_Advantage combines key-dependent messages (msg : W → W) with key leakage (outputs (tag, key) as a pair). Same KDM + leakage pattern as AEAD_Keyed_Advantage.

Literature

Same as AEAD_Keyed_Advantage: Black-Rogaway-Shrimpton 2003, Applebaum et al. 2014, Dodis et al. 2010.

Usage

Used by SSH and Kerberos hybrid arguments.

noncomputable def CatCrypt.Crypto.Assumptions.mac_keyed_real {W : Type} [SampleableType W] (D : MACDef W) (msg : W → W) : Core.SPComp (W × W)

MAC keyed real game: sample key, output (tag, key) pair.

Equations

• CatCrypt.Crypto.Assumptions.mac_keyed_real D msg = (CatCrypt.Core.SPComp.sample W).bind fun (key : W) => CatCrypt.Core.SPComp.pure (D.mac key (msg key), key)

noncomputable def CatCrypt.Crypto.Assumptions.mac_keyed_ideal {W : Type} [SampleableType W] : Core.SPComp (W × W)

MAC keyed ideal game: sample independent random pair.

Equations

• CatCrypt.Crypto.Assumptions.mac_keyed_ideal = CatCrypt.Core.SPComp.sample (W × W)

noncomputable def CatCrypt.Crypto.Assumptions.MAC_Keyed_Advantage {W : Type} [SampleableType W] (D : MACDef W) (msg : W → W) (A : W × W → Core.SPComp Bool) : ENNReal

MAC keyed advantage.

Equations

• CatCrypt.Crypto.Assumptions.MAC_Keyed_Advantage D msg A = CatCrypt.Crypto.AdvantageA (CatCrypt.Crypto.Assumptions.mac_keyed_real D msg) CatCrypt.Crypto.Assumptions.mac_keyed_ideal A

theorem CatCrypt.Crypto.Assumptions.mac_keyed_real_isPure {W : Type} [SampleableType W] (D : MACDef W) (msg : W → W) : (mac_keyed_real D msg).IsPure

theorem CatCrypt.Crypto.Assumptions.mac_keyed_ideal_isPure {W : Type} [SampleableType W] : mac_keyed_ideal.IsPure