Deterministic MAC from a PRF

The standard construction of a message authentication code from a pseudorandom function (Boneh-Shoup v0.6, §6.3; Katz-Lindell, Construction 4.3):

• tag k m := pure (prf.eval k m)
• verify k m t := pure (t == prf.eval k m)

Main Definitions

• PRFScheme.toMacAlg — the derived MAC from a PRF.
• PRFScheme.toMacAlg_perfectlyComplete — honest tags always verify.

Security (Boneh-Shoup Theorem 6.2)

• PRFScheme.macToPRFReduction — the PRF distinguisher constructed from a UF-CMA forger.
• PRFScheme.prf_implies_uf_cma — PRF security implies UF-CMA security: UF_CMA_Advantage(A) ≤ prfAdvantage(prf, B) + 1/|R|.

References

• [Boneh, Shoup, A Graduate Course in Applied Cryptography, v0.6, §6.3] (https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf)

Construction

def PRFScheme.toMacAlg {K D R : Type} [DecidableEq R] (prf : PRFScheme K D R) : MacAlg ProbComp D K R

The deterministic MAC derived from a PRF: tagging is PRF evaluation, verification recomputes and compares.

theorem PRFScheme.toMacAlg_perfectlyComplete {K D R : Type} [DecidableEq R] (prf : PRFScheme K D R) : prf.toMacAlg.PerfectlyComplete ProbCompRuntime.probComp

The derived MAC is perfectly complete: an honestly generated tag always verifies.

Security Reduction (Boneh-Shoup Theorem 6.2)

Given a UF-CMA forger A against prf.toMacAlg, we construct a PRF distinguisher B (macToPRFReduction A) and prove:

UF_CMA_Advantage(A) ≤ prfAdvantage(prf, B) + 1/|R|

The reduction forwards A's tagging queries to its own PRF/random-function oracle while logging them, then checks the forgery condition.

Strong vs weak UF-CMA. Boneh-Shoup's Attack Game 6.1 checks that the forgery pair (m, t) is fresh (strong UF-CMA). VCVio's MacAlg.UF_CMA_Exp checks only message freshness (!log.wasQueried msg). For the deterministic MAC prf.toMacAlg, each message has exactly one valid tag, so the two notions coincide.

noncomputable def PRFScheme.macToPRFQueryImpl {D R : Type} : QueryImpl (unifSpec + OracleSpec.ofFn fun (x : D) => R) (WriterT (OracleSpec.ofFn fun (x : D) => R).QueryLog (OracleComp (unifSpec + OracleSpec.ofFn fun (x : D) => R)))

Oracle implementation for the reduction: forwards unifSpec queries transparently and forwards (D →ₒ R) queries to the ambient oracle while logging them.

noncomputable def PRFScheme.macToPRFReduction {K D R : Type} [DecidableEq D] [DecidableEq R] (prf : PRFScheme K D R) (adversary : prf.toMacAlg.UF_CMA_Adversary) : PRFAdversary D R

The PRF distinguisher constructed from a UF-CMA forger. Runs the forger with logged-and-forwarded oracles, then verifies the forgery via one additional oracle query. If the forger makes Q tagging queries, the reduction makes Q + 1 oracle queries total; this can be tracked separately via IsTotalQueryBound.

theorem PRFScheme.prfRealExp_macToPRFReduction_eq_UF_CMA_Exp {K D R : Type} [DecidableEq D] [DecidableEq R] (prf : PRFScheme K D R) (adversary : prf.toMacAlg.UF_CMA_Adversary) : Pr[= true | prf.prfRealExp (prf.macToPRFReduction adversary)] = MacAlg.UF_CMA_Advantage ProbCompRuntime.probComp adversary

In the real PRF experiment, the reduction reproduces exactly the UF-CMA game.

theorem PRFScheme.prfIdealExp_macToPRFReduction_le {K D R : Type} [DecidableEq D] [DecidableEq R] [Nonempty R] [SampleableType R] [Fintype R] (prf : PRFScheme K D R) (adversary : prf.toMacAlg.UF_CMA_Adversary) : Pr[= true | prfIdealExp (prf.macToPRFReduction adversary)].toReal ≤ (↑(Fintype.card R))⁻¹

In the ideal PRF experiment (random oracle), the reduction succeeds with probability at most 1/|R| — a fresh random oracle query is independent of the forger's output.

Proof idea: The reduction outputs true only when !wasQueried log msg ∧ τ = t, where t is the random oracle's response on msg. If msg was queried before (wasQueried = true), the output is false. If msg is fresh, the random oracle returns a uniform t ← $ᵗ R independent of τ, so Pr[τ = t] = 1/|R|.

theorem PRFScheme.prf_implies_uf_cma {K D R : Type} [DecidableEq D] [DecidableEq R] [Nonempty R] [SampleableType R] [Fintype R] (prf : PRFScheme K D R) (adversary : prf.toMacAlg.UF_CMA_Adversary) : (MacAlg.UF_CMA_Advantage ProbCompRuntime.probComp adversary).toReal ≤ prf.prfAdvantage (prf.macToPRFReduction adversary) + (↑(Fintype.card R))⁻¹

Boneh-Shoup Theorem 6.2. PRF security implies UF-CMA security for the derived MAC: for any forger A, the constructed distinguisher macToPRFReduction prf A satisfies UF_CMA_Advantage(A) ≤ prfAdvantage(prf, B) + 1/|R|.