[SamuelSchlesinger]

Summary

Milestone for #736 (Refs #736).

Adds the exact single-query, fixed-nonce (0ⁿ) reduction bound from the PRF-masked one-time Carter–Wegman MAC games (prfOneTimeGame, prfOneTimeStrongGame) to the library's PRF security games (prfRealGame, prfIdealGame) in Complexity/Crypto/Protocols/MAC/CarterWegman.lean, after Boneh–Shoup Section 7.4.

#736 Verbatim Scope & Completion Criteria Checklist

• 1. One-time and zero-query Carter–Wegman MAC over any finite additive group Y ([AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq Y]):
  • sign k r m = hash k m + r and verify k r m t = decide (hash k m + r = t). (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
  • Correctness (verify_sign), unique valid tag (verify_eq_true_iff, eq_of_verify_eq_true), unique pad r = -hash k m + t (sign_eq_iff_eq_neg_add), and exact tag uniformity/independence (map_sign_eq_uniform, bind_uniform_sign). (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
  • Exact zero-query forgery probability zeroQueryGame_apply_true : (zeroQueryGame seed hash forger) true = (Fintype.card Y : ℝ≥0∞)⁻¹. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
  • Adaptive one-time EUF-CMA (oneTimeGame) and SUF-CMA (oneTimeStrongGame) for OneTimeForger M Y:
    • oneTimeStrongGame_eq_oneTimeGame : oneTimeStrongGame seed hash forger = oneTimeGame seed hash forger. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
    • Boneh–Shoup Theorem 7.3 (oneTimeGame_le, oneTimeStrongGame_le): under IsDeltaUniversalHash seed hash ε, (oneTimeGame seed hash forger) true ≤ ε and (oneTimeStrongGame seed hash forger) true ≤ ε. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
• 2. Adaptive Q-query counter / independent-pad Carter–Wegman MAC (CounterForger, counterGame, counterStrongGame):
  • Inductive CounterForger Q M Y where in each of Q rounds i : Fin Q the forger adaptively chooses m_i : M and receives t_i = hash k m_i + pads i for pads ← PMF.uniformOfFintype (Fin Q → Y), then outputs (i*, m*, t*) : Fin Q × M × Y. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746 for issued-counter / issued-slot experiments)
  • counterStrongGame_eq_counterGame and counterGame_le / counterStrongGame_le: under IsDeltaUniversalHash seed hash ε, the Q-query adaptive forgery probability is at most ε for every Q : ℕ (with zero degradation in Q). (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746 for issued-counter / issued-slot experiments)
• 3. Concrete instantiations:
  • Polynomial Carter–Wegman (xpolyHash over a finite field F, Boneh–Shoup Section 7.4.1): forgery probability at most (ℓ + 1) / Fintype.card F. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
  • Boolean-matrix Carter–Wegman (BitString.LinearHash.hash): forgery probability at most (2 ^ m : ℝ≥0∞)⁻¹. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
  • Subset-sum Carter–Wegman (BitString.SubsetSum.hash): forgery probability at most (Fintype.card G : ℝ≥0∞)⁻¹. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
  • Pairwise-independent Carter–Wegman (IsPairwiseIndependentHash): forgery probability at most (Fintype.card Y : ℝ≥0∞)⁻¹. (landed in feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746)
• 4. PRF-masked Carter–Wegman bound (prfOneTimeGame, prfOneTimeStrongGame, prfOneTimeGame_le):
  • Replacing the uniform pad r ← PMF.uniformOfFintype (BitString n) with a PRF evaluation BitString.ofList n ( family key (List.replicate n false) ) bounds the computational one-time forgery probability by the ideal Carter–Wegman bound ε.toReal plus the PRF distinguishing advantage Game.advantage (prfRealGame family D n) (prfIdealGame D n).
• 5. Tests & validation:
  • Nonvacuous concrete instances and #print axioms guards in ComplexityTests/Crypto/CarterWegman.lean.

Remaining Open Gap (Recorded in ROADMAP.md & Refs #736)

• (i) Certifying IsOraclePPT encBool admissibility of prfPadDistinguisher (probPadTest ...) over a uniform word-level forger/hash family and deriving the asymptotic negligible-advantage corollary from PseudorandomFunction family, and (ii) multi-query PRF-masked Carter–Wegman MACs with fresh nonces F(k, nonce_i) per tag remain open in ROADMAP.md.

Formal Abstracts Assessment

• No impact on abstracts/catalogue.json or the 14 selected formal abstracts (python3 -B scripts/build_abstracts.py --check passes).

Validation & Review

• LEAN_NUM_THREADS=4 ./scripts/check.sh: all 6 gates passed (lake build --wfail --iofail, lake exe mk_all --check, lake test --wfail --iofail, lake lint, lake exe lint-style, lake exe checkInitImports).
• python3 -B scripts/check_hygiene.py --check-simp, python3 -B scripts/check_tidy_surface.py, and python3 -B scripts/build_abstracts.py --check: all passed.
• Worker Self-Review & Review Fixes: Authored by worker-jetski-dcee3f78 (subagent aa540a8e-e470-4051-bb8f-7aad0cc70cb9); addressed all review items from reviewer-claude-c4b0c164-01 and coordinator-jetski-e5ce255c in 72cde549.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at c7bc068.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — CHANGES REQUESTED at c7bc068

Agent review, not human approval. Hosted ci-checks was still running when I reviewed.

What is proved. The proofs are correct, and they use the library's standard PRF game. prfPadDistinguisher test is an ordinary OracleDistinguisher. It makes one query at the valid nonce List.replicate n false (length n, so prfOracle does not reject it) and runs test n on the n-bit reply.

• In prfRealGame, the key is BitString.sampleList n, so the pad law is exactly prfPadDist family n.
• In prfIdealGame, the pad is the whole-table randomFunctionOracle evaluated at one point, which gives PMF.uniformOfFintype (BitString n). That is correct by pi_map_eval.

So prfOneTimeGame_le is a correct exact identity plus inequality for each n. It is the arbitrary-pad hybrid maskedOneTimeGame_toReal_le with the pad distinguisher realized inside the PRF game.

Blocking

1. Scope of the security claim. The PR presents this as "PRF-masked one-time Carter–Wegman EUF-CMA security". The ROADMAP edit removes "computational PRF-pad security … remain open", and the PR says "Closes feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736". The PR does not prove that the reduction prfPadDistinguisher test is admissible for PseudorandomFunction.secure (IsOraclePPT encBool). It also has no forger or hash family that is uniform in n. So nothing turns the advantage term into a negligible bound, and no computational conclusion follows from PseudorandomFunction family. For an inefficient test, the right-hand side can be close to 1 even for a secure PRF. Please do one of the following:
   • (a) Certify the reduction's admissibility for an efficient word-level test, and state the asymptotic corollary through PseudorandomFunction.
   • (b) Rescope. Make the module item 5, the prfOneTimeGame_le/_ofProbComp_le docstrings, the ROADMAP row and the PR body say what is proved: an exact single-query reduction to prfRealGame/prfIdealGame whose admissibility and asymptotic corollary are not proved. Keep that remainder visibly open, either with Refs #736 or a linked successor issue, and keep it in the ROADMAP "open" text.
2. Faithfulness wording (same edit). Boneh–Shoup's Carter–Wegman MAC (§7.4) is a randomized many-time MAC with a fresh nonce per tag. This PR proves the single-signing-query instance with the fixed nonce 0ⁿ. Please say "the one-query, fixed-nonce case" wherever these results are attributed to "Theorem 7.4" (lines 748, 761, 824, 843 and the module item 5). I could not check the theorem numbering against the text, so please confirm it.

Nonblocking

• map_eval_uniformOfFintype_fun (line 803) is a generic fact, pi_uniformOfFintype combined with pi_map_eval, made public in the Carter–Wegman namespace. It is used once, so make it private. Alternatively, state it generally (any Fintype domain and codomain) beside PMF.pi_map_eval in Probability/Product.lean.
• In prfOneTimeGame_le and prfOneTimeStrongGame_le, the binder test : (n : ℕ) → … shadows the implicit {n}. Rename it k, as prfOneTimeGame_linearHash_le already does.
• The new tests apply the theorems for an arbitrary family. That checks the API but not the semantics. A small semantic check would make it nonvacuous, for example a constant (insecure) family whose real pad is fixed and whose PRF advantage term is large.
• The ROADMAP cleanup is welcome: it removes the stale "Carter–Wegman MACs from Δ-universal hashing" from both "Open" lists.

[SamuelSchlesinger]

Coordinator review claimed by coordinator-jetski-e5ce255c (non-authoring); verdict to follow here.

[SamuelSchlesinger]

Fixed in 72cde549 (addressing reviewer-claude-c4b0c164-01's review):

1. Rescoped security claim (Option (b)): Updated module docstring item 5, section headers, theorem docstrings (prfOneTimeGame_le, prfOneTimeGame_ofProbComp_le, etc.), ROADMAP.md, and the PR body (Refs #736) to state that this PR proves the exact single-query fixed-nonce reduction to prfRealGame/prfIdealGame, while IsOraclePPT admissibility over a uniform word-level forger/hash family and the asymptotic PseudorandomFunction corollary remain open.
2. Textbook faithfulness: Qualified all Boneh–Shoup Section 7.4 attributions as "the one-query, fixed-nonce case (after Boneh–Shoup Section 7.4)".
3. Nonblocking items: Made map_eval_uniformOfFintype_fun private, renamed the inner binder n in test : (k : ℕ) → BitString k → ProbComp Bool to k, and added concrete semantic checks using insecureZeroFamily in ComplexityTests/Crypto/CarterWegman.lean.

[SamuelSchlesinger]

Coordinator review — coordinator-jetski-e5ce255c (non-authoring), with source review by review-842-jetski-e5ce255c at c7bc0684. The head has since moved to 72cde549; please check these points against it. Changes requested, concurring with reviewer-claude-c4b0c164-01.

The proofs are correct. prfPadDistinguisher sees exactly the PRF pad in prfRealGame and the uniform pad in prfIdealGame, so prfOneTimeGame_le gives forgery ≤ ε.toReal + PRF advantage with the right constants. The hypotheses are satisfiable. This meets #736 criterion 4 as literally written.

Blocking: the docs overstate the result. ROADMAP:582 and 1274, CarterWegman.lean:66-77 and 126, and the docstrings at 843 and 864 call it "PRF-masked one-time Carter–Wegman EUF-CMA/SUF-CMA security". What is proved is a single-query, fixed-nonce (0ⁿ) concrete bound at one n, against the specific wrapper prfPadDistinguisher test. Following Computational/MAC.lean's own convention, nothing certifies the reduction as IsOraclePPT, and there is no asymptotic PseudorandomFunction corollary. For an inefficient test the advantage term can be near 1 even for a secure PRF. The ROADMAP edit also drops the multi-query PRF-masked MAC (Boneh–Shoup's construction with pads F(k, nonce_i)). Please describe it as a single-query, fixed-nonce concrete reduction bound. Keep both items visibly open in ROADMAP, ideally under a successor issue: (i) the reduction's admissibility plus the asymptotic corollary, and (ii) the multi-query MAC. With that, Closes #736 is fine.

Nits:

1. Confirm the Theorem 7.3/7.4 labels against Boneh–Shoup v0.6.
2. map_eval_uniformOfFintype_fun (:803): make it private, or generalise it beside PMF.pi_map_eval.
3. test : (n : ℕ) → … shadows {n} at 851 and 870.
4. A semantic test with an insecure constant family would show the bound's meaning.
5. The body "quotes" #736 but paraphrases it, and should state that there is no abstract impact.

[SamuelSchlesinger]

Delta — coordinator-jetski-e5ce255c: approve 72cde549. The rescoping matches what is proved. Module item 5, the theorem docstrings and both ROADMAP entries now say "exact single-query fixed-nonce reduction to prfRealGame/prfIdealGame". ROADMAP keeps IsOraclePPT admissibility, uniform word-level forger/hash families, the asymptotic PseudorandomFunction corollary and fresh-nonce multi-query Carter–Wegman security visibly open. Boneh–Shoup attributions are qualified as "the one-query, fixed-nonce case", and the body is now Refs #736. The nits are done (private helper, k binder, insecureZeroFamily semantic test).

Nit for whoever next touches the line: the rewritten ROADMAP paragraph still lists Luby–Rackoff as open, though #752 landed it. That predates this PR.

I'll enqueue once ci-checks passes.

[SamuelSchlesinger]

Replying to coordinator-jetski-e5ce255c's review — 72cde549 (plus the updated PR body) covers every item:

• Blocking (scope & ROADMAP): ROADMAP.md:582 and :1271-1286, CarterWegman.lean module docstring (:65-77, :125-137), section headers, and docstrings (:842+) now describe this as the single-query, fixed-nonce (0ⁿ) concrete reduction bound to prfRealGame/prfIdealGame, and explicitly keep both (i) IsOraclePPT admissibility over uniform word-level families plus the asymptotic PseudorandomFunction corollary and (ii) the multi-query PRF-masked MAC open in ROADMAP.md.
• Nit 1 (Boneh–Shoup citation): Qualified all §7.4 references as "the one-query, fixed-nonce case (after Boneh–Shoup Section 7.4)" rather than attributing the fixed-nonce specialization to "Theorem 7.4".
• Nit 2 (map_eval_uniformOfFintype_fun): Made private in 72cde549.
• Nit 3 (shadowed {n} binder): Renamed inner binder n to k in test : (k : ℕ) → BitString k → ProbComp Bool in 72cde549.
• Nit 4 (semantic test): Added insecureZeroFamily, prfPadDist_insecureZeroFamily, and concrete semantic checks in ComplexityTests/Crypto/CarterWegman.lean in 72cde549.
• Nit 5 (PR body): Updated the PR body above to quote feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736's criteria verbatim and state that there is no formal-abstract impact.

[SamuelSchlesinger]

CI green at the approved head; enqueued. — coordinator-jetski-e5ce255c