MAC from PRF Construction

This file formalizes Claim 10.4 of "The Joy of Cryptography" (online edition, Chapter 10, Message Authentication Codes): constructing a secure MAC (Message Authentication Code) from a PRF (Pseudorandom Function).

Overview

The construction is simple:

• Given a PRF F_k: M → T, define:
  • GetTag(m) = F_k(m)
  • CheckTag(m, t) = (F_k(m) == t)

Security Proof via Game Hopping

The security proof uses a sequence of game hops:

1. TAG_real (Real MAC game):

   • GetTag(m) = PRF(k, m) and CheckTag(m, t) = (PRF(k, m) == t)

2. TAG_EVAL_tt ∘ EVAL_real (Link with PRF real):

   • GetTag/CheckTag use the PRF lookup interface

3. TAG_EVAL_tt ∘ EVAL_ideal (Replace PRF with random):

   • Lookup returns random values (stored in table T)

4. TAG_GUESS_real (Intermediate via GUESS package):

   • CheckTag uses the GUESS interface

5. TAG_GUESS_ideal (Statistical gap):

   • GUESS returns based on stored table membership

6. TAG_EVAL_ff ∘ EVAL_ideal (Dual construction):

   • Uses set S to track (m, t) pairs

7. TAG_EVAL_ff ∘ EVAL_real (Back to PRF):

   • Statistical identical to TAG_ideal

8. TAG_ideal (Ideal MAC game):

   • GetTag stores (m, t) in set S, CheckTag checks membership

Main Result

Advantage(TAG) ≤ prf_epsilon_1 + statistical_gap + prf_epsilon_2

where:

• prf_epsilon_i is the PRF advantage for adversary A ∘ TAG_EVAL_pkg_i
• statistical_gap is the GUESS distinguishing probability (negligible)

References

• [Rosulek, The Joy of Cryptography, online edition, Chapter 10, Claim 10.4]
• SSProve PRFMAC.v

Type Definitions

Following the Rocq development, we parameterize by:

• n: the security parameter (not used explicitly for Bool, but mirrors the structure)
• Word: the type for messages, tags, and keys (Bool for simplicity)
• PRF: the pseudorandom function family

@[reducible, inline]

abbrev CatCrypt.Examples.PRFMAC.Word : Type

For simplicity, we use Bool as the word type (represents Z_{2^n} with n=1)

Equations

• CatCrypt.Examples.PRFMAC.Word = Bool

@[instance_reducible]

instance CatCrypt.Examples.PRFMAC.instFintypeWord : Fintype Word

Equations

• CatCrypt.Examples.PRFMAC.instFintypeWord = inferInstance

instance CatCrypt.Examples.PRFMAC.instNonemptyWord : Nonempty Word

@[instance_reducible]

instance CatCrypt.Examples.PRFMAC.instDecidableEqWord : DecidableEq Word

Equations

• CatCrypt.Examples.PRFMAC.instDecidableEqWord = inferInstance

PRF Function

We abstract over the PRF function. In the Rocq version, this is a parameter. For our Bool instantiation, we use XOR (same as in PRF.lean and MAC.lean).

def CatCrypt.Examples.PRFMAC.prf (k m : Word) : Word

The PRF function: key → message → tag. For Bool, we use XOR which is a bijection.

Equations

• CatCrypt.Examples.PRFMAC.prf k m = (k ^^ m)

Memory Locations

The proof uses several memory locations for state:

• k_loc: the PRF key (Option Word, None means not yet sampled)
• T_loc: random function table (Map Word Word)
• S_loc: set of (message, tag) pairs that have been issued

In Lean, we model these using the Heap abstraction from CatCrypt.Core. For this example, we use simplified in-line state rather than explicit locations.

Operation Identifiers

def CatCrypt.Examples.PRFMAC.LOOKUP : ℕ

Equations

• CatCrypt.Examples.PRFMAC.LOOKUP = 3

def CatCrypt.Examples.PRFMAC.GETTAG : ℕ

Equations

• CatCrypt.Examples.PRFMAC.GETTAG = 5

def CatCrypt.Examples.PRFMAC.CHECKTAG : ℕ

Equations

• CatCrypt.Examples.PRFMAC.CHECKTAG = 6

def CatCrypt.Examples.PRFMAC.GUESS : ℕ

Equations

• CatCrypt.Examples.PRFMAC.GUESS = 7

EVAL Package (PRF/Random Function)

The EVAL package provides a lookup interface that can be either:

• EVAL_real: Uses the PRF with a sampled key
• EVAL_ideal: Uses a truly random function (lazy-sampled table)

noncomputable def CatCrypt.Examples.PRFMAC.EVAL_real (m : Word) : Core.SPComp Word

EVAL_real: lookup returns PRF(k, m) for a lazily-sampled key k.

First call samples the key, subsequent calls use the same key. Models: lookup(m) = F_k(m)

Equations

• CatCrypt.Examples.PRFMAC.EVAL_real m = do let k ← CatCrypt.Core.SPComp.sample CatCrypt.Examples.PRFMAC.Word CatCrypt.Core.SPComp.pure (CatCrypt.Examples.PRFMAC.prf k m)

noncomputable def CatCrypt.Examples.PRFMAC.EVAL_ideal (T : Word → Option Word) (m : Word) : Core.SPComp (Word × (Word → Option Word))

EVAL_ideal: lookup returns a random value, maintaining consistency via table T.

If T[m] exists, return it; otherwise sample fresh, store in T, return. Models a truly random function.

Equations

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

GUESS Package

The GUESS package is an intermediate abstraction that helps with the game hopping.

• GUESS_real: guess(m, t) checks if t equals the value in table T
• GUESS_ideal: guess(m, t) checks if t was previously returned by lookup(m)

The key insight is that these are statistically close when T is random.

noncomputable def CatCrypt.Examples.PRFMAC.GUESS_real (T : Word → Option Word) (m t : Word) : Core.SPComp (Bool × (Word → Option Word))

GUESS_real: checks if guessed tag matches the random table value. Returns (t == T[m]) where T[m] is lazily sampled if needed.

Equations

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

noncomputable def CatCrypt.Examples.PRFMAC.GUESS_ideal (T : Word → Option Word) (m t : Word) : Core.SPComp Bool

GUESS_ideal: checks if (m, t) was previously issued. Returns true iff some T[m] = t (i.e., t was the lookup result).

Equations

• CatCrypt.Examples.PRFMAC.GUESS_ideal T m t = CatCrypt.Core.SPComp.pure (T m == some t)

TAG Package (MAC Interface)

The TAG package is the MAC construction we're proving secure.

• TAG_real: Uses PRF directly
• TAG_ideal: Uses a set S to track issued tags; CheckTag only succeeds for issued pairs

noncomputable def CatCrypt.Examples.PRFMAC.TAG_real_gettag (m : Word) : Core.SPComp Word

TAG_real: The real MAC game.

• GetTag(m) = PRF(k, m)
• CheckTag(m, t) = (t == PRF(k, m))

Note: Key k is sampled lazily on first use.

Equations

• CatCrypt.Examples.PRFMAC.TAG_real_gettag m = do let k ← CatCrypt.Core.SPComp.sample CatCrypt.Examples.PRFMAC.Word CatCrypt.Core.SPComp.pure (CatCrypt.Examples.PRFMAC.prf k m)

noncomputable def CatCrypt.Examples.PRFMAC.TAG_real_checktag (m t : Word) : Core.SPComp Bool

Equations

• CatCrypt.Examples.PRFMAC.TAG_real_checktag m t = do let k ← CatCrypt.Core.SPComp.sample CatCrypt.Examples.PRFMAC.Word CatCrypt.Core.SPComp.pure (t == CatCrypt.Examples.PRFMAC.prf k m)

noncomputable def CatCrypt.Examples.PRFMAC.TAG_ideal_gettag (S : Word × Word → Bool) (m : Word) : Core.SPComp (Word × (Word × Word → Bool))

TAG_ideal: The ideal MAC game with perfect unforgeability.

• GetTag(m): computes t = PRF(k, m), stores (m, t) in set S, returns t
• CheckTag(m, t): returns (m, t) ∈ S

The adversary can only succeed on CheckTag for tags they've received.

Equations

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

noncomputable def CatCrypt.Examples.PRFMAC.TAG_ideal_checktag (S : Word × Word → Bool) (m t : Word) : Core.SPComp Bool

Equations

• CatCrypt.Examples.PRFMAC.TAG_ideal_checktag S m t = CatCrypt.Core.SPComp.pure (S (m, t))

Simplified Game Definitions

For the security proof, we define the games as SPComp computations. We use a simplified model where state is threaded explicitly through the computations.

noncomputable def CatCrypt.Examples.PRFMAC.macReal (m m_check t_guess : Word) : Core.SPComp Bool

Real MAC game: given message m, return (tag, verification_result). Models the real-world behavior where CheckTag uses the actual PRF.

Equations

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

noncomputable def CatCrypt.Examples.PRFMAC.macIdeal (m m_check t_guess : Word) : Core.SPComp Bool

Ideal MAC game: CheckTag only succeeds for previously issued tags. When m_check ≠ m (different message), forgery always fails.

Equations

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

Game Hopping Lemmas

The security proof proceeds by a sequence of game hops, relating: TAG_real ≈ TAG_EVAL ∘ EVAL_real ≈ TAG_EVAL ∘ EVAL_ideal ≈ TAG_GUESS ∘ GUESS_real ≈ TAG_GUESS ∘ GUESS_ideal ≈ TAG_ideal

Each hop is either:

1. Perfect equivalence (code transformation)
2. Bounded by PRF advantage
3. Bounded by statistical gap (negligible)

Core Lemma: PRF output uniformity

When the key k is uniformly random, prf(k, m) = k XOR m is uniformly distributed. This is the key property enabling the security reduction.

theorem CatCrypt.Examples.PRFMAC.prf_uniform (m : Word) : Relational.rHoare Relational.eqPre (do let k ← Core.SPComp.sample Word Core.SPComp.pure (prf k m)) (Core.SPComp.sample Word) Relational.eqPost

Hop 1: TAG_real ≈ TAG_EVAL_tt ∘ EVAL_real

This is a perfect equivalence by construction: both compute PRF(k, m).

theorem CatCrypt.Examples.PRFMAC.hop1_equiv (m m_check t_guess : Word) : macReal m m_check t_guess = do let k ← Core.SPComp.sample Word have _t : Word := prf k m Core.SPComp.pure (t_guess == prf k m_check)

Statistical Gap Lemma

The key statistical insight: when T is a random function and (m, t) was not queried, the probability that t = T[m] is 1/|Word| = 1/2 for Bool.

For GUESS_real vs GUESS_ideal:

• GUESS_real: returns (t == T[m]) where T[m] is random
• GUESS_ideal: returns (T m == some t), which is true iff t was the lookup result

When the adversary hasn't queried lookup(m), GUESS_real returns true with prob 1/2, while GUESS_ideal returns false. This is the statistical gap.

For our simplified Bool case, we can show perfect security under certain conditions.

theorem CatCrypt.Examples.PRFMAC.forgery_diff_message_uniform (m m_check t_guess : Word) (hdiff : m_check ≠ m) : Relational.rHoare Relational.eqPre (macReal m m_check t_guess) (Core.SPComp.sample Bool) Relational.eqPost

When m_check ≠ m (forgery attempt on different message), the verification result is uniformly distributed in the real game.

Main Security Theorem

The MAC constructed from a PRF is secure. The advantage is bounded by:

• The PRF advantage (how distinguishable PRF is from random)
• The statistical gap (probability of successful guess on unqueried input)

For our simplified Bool model with XOR "PRF", both are zero, giving perfect security.

Perfect indistinguishability fails on an unqueried message

When m_check ≠ m, the real game returns a uniform Boolean (the guess is checked against the PRF output) and the ideal game returns false. The identity distinguisher separates them with advantage 1/2, so no equality coupling between the two games exists (not_rHoare_macReal_macIdeal_of_ne). The gap is the statistical term of the PRF-MAC bound: 1/2 over Bool, 1/2^n over {0,1}^n. The security statement is therefore an advantage bound (security_based_on_prf).

noncomputable def CatCrypt.Examples.PRFMAC.mac_forgery_advantage (m m_check t_guess : Word) (A : Bool → Core.SPComp Bool) : ENNReal

The advantage in distinguishing real vs ideal MAC for forgery attempts.

When m_check ≠ m, the distinguishing advantage equals the statistical gap:

• Real: Pr[t_guess == PRF(k, m_check)] = 1/2 for uniform k
• Ideal: Pr[false] = 0

An adversary that outputs "real" when verification succeeds and "ideal" when it fails has advantage |1/2 - 0| = 1/2 for Bool.

For the full security proof, this gap is bounded by 1/|Word| = 1/2^n, which is negligible for large n.

Equations

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

theorem CatCrypt.Examples.PRFMAC.mac_same_message_correct_tag (m k : Word) : (prf k m == prf k m) = true

When messages match (m_check = m), verification behaves identically in both games for the correct tag. This is the "no forgery needed" case.

theorem CatCrypt.Examples.PRFMAC.mac_same_message_coupling (m t_guess : Word) : Relational.rHoare Relational.eqPre (macReal m m t_guess) (macIdeal m m t_guess) Relational.eqPost

For same message, both games agree on correct tag verification.

macIdeal Simplification

theorem CatCrypt.Examples.PRFMAC.macIdeal_diff_eq_pure_false (m m_check t_guess : Word) (hdiff : m_check ≠ m) : macIdeal m m_check t_guess = Core.SPComp.pure false

When messages differ, the ideal MAC game always returns false. Since m_check ≠ m, the check m_check == m is false, making the entire conjunction false regardless of the key.

theorem CatCrypt.Examples.PRFMAC.prTrue_pure_empty (b : Bool) : Crypto.prTrue (Core.SPComp.pure b) Core.Heap.empty = if b = true then 1 else 0

prTrue of a constant Boolean computation from the empty heap.

theorem CatCrypt.Examples.PRFMAC.not_rHoare_macReal_macIdeal_of_ne (m m_check t_guess : Word) (hdiff : m_check ≠ m) : ¬Relational.rHoare Relational.eqPre (macReal m m_check t_guess) (macIdeal m m_check t_guess) Relational.eqPost

Refutation of perfect indistinguishability for a forgery on an unqueried message: for m_check ≠ m there is no equality coupling between macReal and macIdeal. The identity distinguisher has advantage 1/2, while an equality coupling forces advantage 0.

Security Statement

The full security theorem would state:

Advantage_MAC(A) ≤ Advantage_PRF(A ∘ Wrapper₁) +
                   Statistical_Gap(A) +
                   Advantage_PRF(A ∘ Wrapper₂)

For our simplified Bool model:

• The PRF advantage is 0 (XOR with random key is perfectly random)
• The statistical gap is 1/2 for a single guess on Bool

In a proper cryptographic setting with security parameter n:

• Word = {0,1}^n (2^n elements)
• Statistical gap = 1/2^n per query (negligible)
• PRF advantage is negligible by assumption

noncomputable def CatCrypt.Examples.PRFMAC.prf_epsilon (A : Word → Core.SPComp Bool) : ENNReal

The PRF epsilon: advantage in distinguishing PRF from random function. For our XOR construction over Bool, this is 0.

Equations

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

noncomputable def CatCrypt.Examples.PRFMAC.statistical_gap (_m _t : Word) : ENNReal

The statistical gap: advantage in the GUESS game. For Bool, this represents the probability of a lucky guess.

Equations

• CatCrypt.Examples.PRFMAC.statistical_gap _m _t = 1 / 2

theorem CatCrypt.Examples.PRFMAC.security_based_on_prf (m m_check t_guess : Word) (hdiff : m_check ≠ m) : mac_forgery_advantage m m_check t_guess ≤ fun (A : Word → Core.SPComp Bool) => prf_epsilon A + statistical_gap m t_guess + prf_epsilon A

Main security theorem: MAC forgery advantage is bounded.

The advantage of any adversary A against the MAC scheme is bounded by the sum of PRF advantages and the statistical gap:

mac_forgery_advantage ≤ prf_epsilon₁ + statistical_gap + prf_epsilon₂

For the Bool/XOR construction:

• PRF advantages are 0 (perfect PRF security)
• Statistical gap is 1/2 per query

In a proper crypto setting with security parameter n:

• Statistical gap is 1/2^n (negligible)
• PRF advantages are negligible by assumption

Proof Status: The individual game hop lemmas are proved:

• prf_uniform: PRF output is uniformly distributed (bijection coupling)
• mac_same_message_coupling: same-message case is perfectly coupled
• forgery_diff_message_uniform: different-message forgery is uniform

The full chaining requires package composition (link) and the advantage triangle inequality. The shallow RawPackage layer does not support linking (see RawPackage.link WARNING). Use the deep embedding layer (DeepPackage.link, runPkg_link) for the complete proof.

Discussion

Relation to Rocq SSProve

The Rocq development (PRFMAC.v) proves the full security theorem with:

1. Package Infrastructure: Packages with interfaces, locations, and composition
2. Game Hopping: Using ssprove triangle tactic for advantage bounds
3. Invariant Proofs: Relational invariants for state correspondence

This Lean port demonstrates:

• The core game definitions (TAG, EVAL, GUESS packages as SPComp)
• The key bijection coupling technique for PRF uniformity
• The structure of the security argument

What Would Complete the Port

1. Package Linking: Formal link operation for composing packages
2. Advantage Bounds: Triangle inequality for chaining game hops
3. Stateful Invariants: Formal invariants relating table T and set S
4. Package Validity: Proofs that adversary locations are disjoint from game state

The Statistical Gap

The statistical gap arises from the GUESS game:

• GUESS_real: Returns (t == T[m]) for random T[m]
• GUESS_ideal: Returns (m,t) ∈ issued_tags

When the adversary queries CheckTag(m*, t*) for a fresh message m*:

• Real: t* matches a random value with probability 1/|Word|
• Ideal: Returns false (m* wasn't in issued messages)

This gap is 1/|Word| = 1/2^n, which is negligible in n.

Comparison with Simple XOR MAC (MAC.lean)

MAC.lean shows that a simple XOR MAC is NOT secure: the adversary can compute k from t = k ⊕ m and forge arbitrary tags.

PRFMAC demonstrates that using a PRF prevents this attack because:

1. The adversary cannot distinguish PRF from random
2. Random functions don't reveal the key from outputs
3. Forging requires guessing PRF outputs, which has negligible probability