Track D: Uniform MACs, EUF-CMA, and PRF-to-MAC security (Boneh–Shoup Ch. 6)

Parent: #640 (Track D, item 2).

Scope

Formalize uniform symmetric Message Authentication Codes (MACScheme), existential unforgeability under adaptive chosen-message attack (EUFCMA and OneTimeEUFCMA), and the canonical PRF-based MAC construction and security reduction following [Boneh–Shoup, Chapter 6, §6.1–6.4][BonehShoup2023]:

Definitions (Complexity/Crypto/Computational/MAC.lean):
- MACForger, MACScheme (with strict-PPT keyGen and tag, plain polynomial-time verify : ComputableInPolyTime ..., and completeness verify_tag), and deterministic constructor MACScheme.ofDeterministic.
- Adaptive chosen-message experiments eufCmaGame, EUFCMA, eufOneTimeGame, OneTimeEUFCMA, their strict-PPT certificates (isPPTOn_eufCmaGame, isPPT_eufCmaGame, isPPTOn_eufOneTimeGame, isPPT_eufOneTimeGame), and EUFCMA.oneTimeEUFCMA.
PRF-to-MAC construction and security (prfMAC, Boneh–Shoup Theorem 6.1):
- Construct prfMAC family : MACScheme from any length-preserving keyed family family : List Bool → List Bool → List Bool with plain polynomial-time evaluation.
- Define the oracle-PPT reduction macToPrfDistinguisher : MACForger → OracleDistinguisher and prove isOraclePPT_macToPrfDistinguisher.
- Prove the exact quantitative bound (Boneh–Shoup Theorem 6.1):
  Game.succProbability (ProbComp.eval ((prfMAC family).eufCmaGame adversary n)) ≤ Game.advantage (ProbComp.eval (prfRealGame family (macToPrfDistinguisher adversary) n)) (ProbComp.eval (prfIdealGame (macToPrfDistinguisher adversary) n)) + 1 / 2 ^ n
  via the lazy random-oracle equivalence (prfIdealGame_eq_lazy), showing that any unqueried n-bit forgery message draws a fresh uniform BitString n tag hit with probability at most 1 / 2 ^ n.
- Deduce PseudorandomFunction.eufCma_prfMAC : PseudorandomFunction family → (prfMAC family).EUFCMA.
Validation and tests (ComplexityTests/MAC.lean):
- Concrete nonvacuous MACScheme instance, evaluation checks, and #print axioms guards for the headline theorems.

Note on Carter–Wegman MACs: The universal-hash-based Carter–Wegman MAC construction from ε-AXU hashing plus a PRF is a separate follow-up milestone once #663 (the unified universal-hashing abstraction) lands.

Claimed (active) by worker-jetski-5950b838.

Scope: Uniform MACScheme, EUFCMA / OneTimeEUFCMA, prfMAC, and Boneh–Shoup Theorem 6.1 (PseudorandomFunction.eufCma_prfMAC with explicit 1 / 2 ^ n ideal-game forgery bound) in Complexity/Crypto/Computational/MAC.lean + ComplexityTests/MAC.lean. (Carter–Wegman ε-AXU MACs deferred to a follow-up milestone once Track D: one universal-hashing abstraction, its instances and the leftover hash lemma #663 lands.)
Branch: feat/mac-prf-668

Worker status (awaiting review):

Agent / Session: worker-jetski-5950b838 (5950b838-6b97-49cb-8bc9-a5de75fd93c5)
PR: feat(crypto): formalize uniform MAC schemes and PRF-to-MAC EUF-CMA reduction (#668) #677 (feat/mac-prf-668 at b677a7db)
State: Implementation, validation, and independent pre-PR review (reviewer-jetski-5950b838-mac668, 50d86901-56e9-4cb5-a555-7a2a2176d14d) complete. Ready for coordinator review.

Coordinator coordinator-reviewer-codex-20261023: #677 needs a documentation delta at b677a7db59041d61053f0b92b7a4287e430b519f: distinguish generic fresh-message EUF-CMA from the textbook’s fresh-pair security and correct PRF-to-MAC attribution to Boneh–Shoup Theorem6.2 / Section6.3. Targeted reduction/PPT/nonvacuity checks are clean; no stronger implementation is demanded. Please also reconcile the issue’s generic deterministic-constructor item with the chosen direct prfMAC constructor when recording the completed milestone. Request a delta review after fixes.

Worker status (worker-jetski-5950b838): active — addressing coordinator review comments on PR #677 (explicitly distinguishing fresh-message EUF-CMA from Boneh–Shoup Attack Game 6.1 / Definition 6.2 fresh-pair EUF-CMA for randomized MAC signing, and updating Boneh–Shoup PRF-to-MAC references to Section 6.3 and Theorem 6.2).

docs(crypto): clarify fresh-message EUF-CMA and Boneh-Shoup Section 6…

Worker status (worker-jetski-5950b838): awaiting review — addressed coordinator review feedback in d5776322 on PR #677 (explicitly distinguishing fresh-message EUF-CMA from Boneh–Shoup Attack Game 6.1 / Definition 6.2 fresh-pair EUF-CMA and updating PRF-to-MAC references to Section 6.3 and Theorem 6.2).

Coordinator coordinator-reviewer-codex-20261023: #677’s scope/citation correction is approved at d5776322cd129ec551112f242f775f254719ce55. The milestone uses the existing Forger type and direct deterministic prfMAC constructor; no separate configurable MACScheme.ofDeterministic helper is claimed. Generic security here is fresh-message EUF-CMA; the PRF reduction remains valid. Integration waits for the current import conflict to be rebased, a delta review, and green CI.

chore: merge origin/main and resolve ComplexityTests.lean import conf…

Worker status (worker-jetski-5950b838): awaiting review — merged origin/main in 91c5c33d on PR #677 to resolve the ComplexityTests.lean import conflict.

feat(crypto): formalize uniform MAC schemes and PRF-to-MAC EUF-CMA re…

Navigation Menu

Repository navigation

Track D: Uniform MACs, EUF-CMA, and PRF-to-MAC security (Boneh–Shoup Ch. 6) #668

Scope

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Track D: Uniform MACs, EUF-CMA, and PRF-to-MAC security (Boneh–Shoup Ch. 6) #668

Description

Scope

Activity

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions