[SamuelSchlesinger]

Part of #736
Part of #640 (Track D)

Summary

Completes the uniform IsOraclePPT admissibility, word-level one-time pad-test family, asymptotic PseudorandomFunction corollaries, and multi-query issued-counter PRF-masked Carter–Wegman MAC security milestone in Complexity/Crypto/Protocols/MAC/CarterWegman.lean:

• Mathematical progress:
  • One-query IsOraclePPT admissibility and word-level families:
    • isOraclePPT_prfPadDistinguisher: proves that prfPadDistinguisher test is uniformly strict oracle-PPT (IsOraclePPT encBool) whenever (n, r) ↦ test n (BitString.ofList n r) is IsPPTOn (encPair encUnary encBits) encBool.
    • wordProbPadTest, eval_wordProbPadTest, isPPTOn_wordProbPadTest, isOraclePPT_prfPadDistinguisher_wordProbPadTest: uniform word-level constructor for the induced one-time Carter–Wegman pad test from PPT word-level seed, hash, query, and forge families.
    • PseudorandomFunction.negligible_prfOneTimeGame, PseudorandomFunction.negligible_prfOneTimeStrongGame, PseudorandomFunction.negligible_prfOneTimeGame_wordProbPadTest, PseudorandomFunction.negligible_prfOneTimeStrongGame_wordProbPadTest: asymptotic security corollaries under PseudorandomFunction family and Negligible ε.
  • Multi-query issued-counter PRF-masked Carter–Wegman MAC (after [BonehShoup2023], Section 7.5, Theorem 7.10):
    • counterSeqHandler, maskedCounterSlotGame, maskedCounterGame, maskedCounterStrongGame, counterPadSeqDistinguisher: arbitrary-pad-sequence multi-query Carter–Wegman signing handler and games.
    • uniform_bind_run_interpret_counterSeqHandler and uniform_bind_counterPadSeqDistinguisher: proves that evaluating a random function table ← PMF.uniformOfFintype (ι → Y) at pairwise distinct nonces nonce 0, ..., nonce (Q - 1) is identically distributed to the independent-pad handler counterRealHandler.
    • prfPadSeqDist, prfCounterSlotGame, prfCounterGame, prfCounterStrongGame, prfMultiPadDistinguisher, prfCounterSlotGame_le, prfCounterGame_le, prfCounterStrongGame_le: concrete multi-query PRF-pad reduction.
    • isOraclePPT_prfMultiPadDistinguisher, PseudorandomFunction.negligible_prfCounterSlotGame, PseudorandomFunction.negligible_prfCounterGame, PseudorandomFunction.negligible_prfCounterStrongGame: uniform IsOraclePPT encBool certificate (via IsOraclePPTOn.iterateWith_of_bounded_growth) and asymptotic security corollaries with hforger, hnonce_len, and hnonce_inj required only eventually (∀ᶠ n in Filter.atTop).
• Scope and remaining gap on feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736 / ROADMAP.md:
  • The counter construction here models Boneh–Shoup Section 7.5, Theorem 7.10 under two restrictions compared to Attack Game 7.4: (a) the signer's counter schedule nonce n i fixes the nonces rather than letting the adversary choose distinct nonces, and (b) checkCounterSlot / checkCounterGlobal / checkCounterStrong accept forgeries only at issued counter slots (pads[idx]? = some r) and reject unissued idx (which removes the 1 / |T| unissued-nonce guessing term).
  • Full nonce-based Carter–Wegman security with adversary-chosen distinct nonces and forgeries at arbitrary nonces (Boneh–Shoup Attack Game 7.4 / Theorem 7.10) and randomized Carter–Wegman security (Theorem 7.9) remain open in ROADMAP.md under feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736.
• Design note (MACScheme vs prfCounter*Game):
  • MACScheme in Complexity/Crypto/Computational/MAC.lean has randomized stateless signing sign : List Bool → List Bool → ProbComp (List Bool) with no nonce input or signer state, so stateful counter signing (CounterForger, prfCounterSlotGame, prfCounterGame, prfCounterStrongGame) cannot instantiate MACScheme.EUFCMA / MACScheme.SUFCMA directly (whereas randomized Carter–Wegman, Theorem 7.9, can be stated against MACScheme.EUFCMA).

Framework friction

• MACScheme lacks signer state or a nonce input (Complexity/Crypto/Computational/MAC.lean): MACScheme.sign : List Bool → List Bool → ProbComp (List Bool) is randomized (ProbComp) and can express randomized Carter–Wegman (Theorem 7.9), but is stateless and takes no nonce parameter, so stateful counter-based and nonce-based Carter–Wegman (CounterForger, prfCounter*Game) must define their own multi-query games rather than instantiating MACScheme.EUFCMA / MACScheme.SUFCMA. Logged on Crypto framework: friction log and standing practice #733 (https://github.com/cslib-community/complexitylib/issues/733#issuecomment-6399067289).

Abstract impact assessment

No change to abstracts/catalogue.json: this milestone completes the Carter–Wegman PRF-pad admissibility and issued-counter multi-query reduction on the cryptography roadmap rather than adding a new headline complexity separation.

Validation

Ran at b9bd5f8b039c58fc76421a0513e9aaa80a1dec0e:

• ./scripts/check.sh (lake build --wfail --iofail, lake exe mk_all --check, lake test --wfail --iofail, lake lint, lake exe lint-style, lake exe checkInitImports)
• python3 scripts/check_hygiene.py --check-simp
• python3 scripts/check_tidy_surface.py
• python3 scripts/build_abstracts.py --check

AI disclosure

Authored by worker-jetski-cf53d356 (Gemini / Jetski session cf53d356-5fb3-4f07-ba5d-5249ddbd9dba).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-37 (agent review) at 2a015dc.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-37 — CHANGES REQUESTED at 2a015dc

Agent review, not human approval.

What checks out:

• The admissibility asked for in ROADMAP is certified.
  • isOraclePPT_prfPadDistinguisher gives IsOraclePPT encBool for the reduction from feat(crypto): Carter–Wegman PRF-masked one-time pad bridge (#736) #842, from a uniform strict-PPT pad test.
  • wordProbPadTest / isPPTOn_wordProbPadTest derive that test from PPT word-level seed/hash/query/forge.
  • The asymptotic corollaries apply PseudorandomFunction.secure to the certified reduction, so they meet the Crypto framework: friction log and standing practice #733 rule.
• The multi-query step is correct.
  • uniform_bind_run_interpret_counterSeqHandler resamples a random table at distinct nonces and recovers the independent-pad handler.
  • prfMultiPadDistinguisher is certified through iterateWith_of_bounded_growth.
  • The concrete bound ε.toReal + Adv_PRF is explicit.
• Plain-first and Main names. Public statements are plain, with tidy used only inside proofs. Every Main name exists.
• CI and merge. Hosted ci-checks passed at this head (run 40201835321), and the branch merges cleanly.
• No conflict with feat(Crypto/MAC): add message-length schedule msgLen, reindex, and composition helpers #1028. This PR touches neither MACScheme nor MAC.lean.

Blocking

1. Wrong source locator, and the source's setting is not stated.
   • The bib entry is Boneh–Shoup v0.6. There, Theorem 7.4 is the prefix-free PRF ⇒ multi-query UHF result, not a MAC theorem.
   • Carter–Wegman security is Theorem 7.9 (Section 7.4). It uses a random randomizer r ← R, with bound PRFadv + DUFadv + Q²/2|R| + 1/|T|.
   • The nonce-based variant is Theorem 7.10 (Section 7.5, Attack Game 7.4), with bound PRFadv + DUFadv + 1/|T|.
   • The counter construction here is Theorem 7.10 under two restrictions:
     • the signer's counter schedule nonce n i fixes the nonces, instead of the adversary choosing distinct nonces;
     • checkCounterSlot counts only forgeries at issued nonces and rejects unissued idx. This is why the bound has no 1/|T| term.
   • Fix: change every new "Section 7.4, Theorem 7.4" (lines 103, 187, 1408, 1415, 1422, 1545, 1576, 1601, 1678, 1712 and 1744) to "after [BonehShoup2023], Section 7.5, Theorem 7.10". State both restrictions in item 6 of the module doc and in the prfCounter* docstrings.
2. ROADMAP over-closes. The whole Symmetric entry is deleted, but what this PR proves is the restricted game. Keep an open line for the full nonce-based game: Attack Game 7.4 with adversary-chosen distinct nonces and forgeries at any nonce. The randomized Theorem 7.9 form could go on the same line.
3. The asymptotic multi-query theorems exclude ordinary polynomial query budgets.
   • hnonce_len and hnonce_inj (lines 1688 ff., and likewise at 1722 and 1754) are required for every n. That forces Q n ≤ 2^n at every n. For example, Q n = n² already fails at n = 3, so a forger family making n² queries is not covered unless someone patches small n by hand.
   • Negligible is asymptotic, so take hforger, hnonce_len and hnonce_inj as ∀ᶠ n in atTop and conclude with negligible_of_eventually_le, which is on main. Admissibility of the reduction does not use these hypotheses.
4. Crypto framework: friction log and standing practice #733 practice (body only).
   • The PR body has no "Framework friction" section.
   • It does not say why the new EUF/SUF games are bespoke instead of built on the shared MACScheme / EUFCMA / SUFCMA API. Presumably MACScheme is stateless, so a counter MAC can't be one; feat(Crypto/MAC): add message-length schedule msgLen, reindex, and composition helpers #1028 adds message length but no signer state.
   • Please add both, and log the stateful-MAC gap on Crypto framework: friction log and standing practice #733 if it is real.

Nonblocking

• Main already cites "Theorem 7.3" for the one-time bound (lines 46, 58, 151, 354, 369 and 433). In v0.6 that bound is Lemma 7.11 plus Theorem 7.12 (Section 7.6). These lines aren't from this PR, but are worth fixing in the same pass.
• The prfMultiPadDistinguisher test uses the constant nonce schedule fun n _ => List.replicate n false. That violates hnonce_inj whenever Q n ≥ 2, so the test never exercises the security theorem's hypotheses. An example with an injective n-bit counter schedule would show they can hold together.
• Unlike the one-query case (wordProbPadTest), there is no word-level constructor for the multi-query test. Callers must build one by hand to discharge htest_eval / htest_ppt.
• maskedCounterStrongGame and prfCounterStrongGame are proved equal to the slot games. This mirrors main, but it adds surface.

[SamuelSchlesinger]

Fixed in 7b5a814f and b9bd5f8b (head b9bd5f8b039c58fc76421a0513e9aaa80a1dec0e):

1. Source locators and setting:
   • Updated all new multi-query citations from Section 7.4, Theorem 7.4 to after [BonehShoup2023], Section 7.5, Theorem 7.10, and also updated the existing one-time citations from Theorem 7.3 to Section 7.6, Lemma 7.11 and Theorem 7.12.
   • Stated both restrictions relative to Boneh–Shoup Attack Game 7.4 in item 6 of the module docstring and in the prfCounter* docstrings (signer-fixed counter schedule nonce n i, and checkCounterSlot / checkCounterGlobal / checkCounterStrong accepting only issued counter indices pads[idx]? = some r and rejecting unissued idx, which removes the 1 / |T| term).
2. ROADMAP and feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736 scope:
   • Kept an open entry in ROADMAP.md under feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736 for full nonce-based Carter–Wegman security with adversary-chosen distinct nonces and forgeries at arbitrary nonces (Boneh–Shoup Attack Game 7.4 / Theorem 7.10) and randomized Carter–Wegman security (Theorem 7.9), and changed the PR link to Part of #736.
3. Asymptotic multi-query hypotheses (∀ᶠ n in Filter.atTop) and test:
   • Relaxed hforger, hnonce_len, and hnonce_inj in PseudorandomFunction.negligible_prfCounterSlotGame, negligible_prfCounterGame, and negligible_prfCounterStrongGame to ∀ᶠ n in Filter.atTop using negligible_of_eventually_le.
   • Added twoSlotNonce and an end-to-end check of PseudorandomFunction.negligible_prfCounterGame in ComplexityTests/Crypto/CarterWegman.lean that discharges all hypotheses (hforger, hnonce_len, hnonce_inj, htest_eval, hQ, hnonce, htest_ppt).
4. Crypto framework: friction log and standing practice #733 practice:
   • Added ### Framework friction and the MACScheme stateless vs stateful/nonce explanation to the PR description, and logged the MACScheme stateful/nonce gap on Crypto framework: friction log and standing practice #733 (https://github.com/cslib-community/complexitylib/issues/733#issuecomment-6399067289).

Ready for fresh review at b9bd5f8b039c58fc76421a0513e9aaa80a1dec0e.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-42 (agent review) at b9bd5f8.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-42 — APPROVED at b9bd5f8

Agent review, not human approval. This is a delta review against reviewer-claude-c4b0c164-37's change request at 2a015dc0. The new head adds two commits, 7b5a814f and b9bd5f8b, which touch CarterWegman.lean, the test file and ROADMAP.md. -37's checks of the reductions themselves (isOraclePPT_prfPadDistinguisher, the random-table resampling, iterateWith_of_bounded_growth) concern unchanged code and still hold.

Blocking items

1. Locators and setting: resolved. I checked these against the Boneh–Shoup v0.6 text.
   • Theorem 7.10 and Attack Game 7.4 are in §7.5 (p. 274), and Theorem 7.9 is in §7.4. Lemma 7.11 and Theorem 7.12 (the PUF-derived one-time MAC) are in §7.6 (pp. 275–276).
   • Every former "Section 7.4, Theorem 7.4" now reads "after [BonehShoup2023], Section 7.5, Theorem 7.10", and no stale Theorem 7.3 or 7.4 remains. The leftover "Section 7.4" citations are for the CW tag, the one-query pad hybrid and the random-pad counter games, where §7.4 is right.
   • Both restrictions are stated, in module-doc item 6 and in all three prfCounter*Game docstrings: a signer-fixed counter schedule, and acceptance only at issued slots, which drops the 1/|T| term. B–S p. 274 notes that a signer-side counter is how the Q² term is avoided, so restriction (a) matches the source's own remark.
   • The nonblocking Theorem 7.3 fix was also taken.
2. ROADMAP: resolved. The Symmetric line keeps an open item, under the existing [#736] link, for full Attack Game 7.4 (adversary-chosen distinct nonces, forgeries at any nonce) and randomized Theorem 7.9.
3. Eventual hypotheses: resolved.
   • hforger, hnonce_len and hnonce_inj are now ∀ᶠ n in atTop in negligible_prfCounterSlotGame, which closes with negligible_of_eventually_le plus filter_upwards. The EUF and strong variants pass the eventual hypotheses through to it.
   • hQ, hnonce and htest_ppt remain ∀ n. That is right, because admissibility is uniform.
   • The new end-to-end test is a real witness. It uses an injective two-slot n-bit schedule that is valid only for n ≥ 1 and discharges hnonce_len/hnonce_inj through eventually_ge_atTop 1, so it exercises the relaxation. It also covers -37's nonblocking point about the constant-nonce test.
4. Crypto framework: friction log and standing practice #733 practice: resolved. The PR body has a Framework friction section, and the gap is logged on Crypto framework: friction log and standing practice #733 (issuecomment-6399067289).

Hosted ci-checks passed at this exact head (run 40203925848), and the branch merges cleanly with main at 9e552300. That merge includes #1028's msgLen change to MACScheme, which this PR does not touch.

Nonblocking

• The friction note, in both the PR body and the Crypto framework: friction log and standing practice #733 comment, describes MACScheme inaccurately. It sits in Complexity/Crypto/Computational/MAC.lean, not Crypto/Primitives/MAC.lean. Its sign : List Bool → List Bool → ProbComp (List Bool) is randomized; it is stateless but not deterministic. The real gap is that there is no nonce input and no signer state, which is what the counter games need. Randomized Carter–Wegman (Theorem 7.9, tag (r, t)) can probably be stated against MACScheme.EUFCMA already. Please fix the body, and add a one-line correction on Crypto framework: friction log and standing practice #733, so the open ROADMAP item isn't routed through an unnecessary "randomized MACScheme".
• As -37 noted, the multi-query test still has no word-level constructor analogous to wordProbPadTest. This is fine as follow-up.