Skip to content

feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736

New issue
New issue
Closed
#1398
Closed
feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4)#736
#1398
Assignees
SamuelSchlesinger

Description

@SamuelSchlesinger
SamuelSchlesinger
opened on Oct 24, 2026

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

Objective

Formalize Carter–Wegman message authentication codes from $\varepsilon$-almost-$\Delta$-universal hash families (IsDeltaUniversalHash in Complexity.Probability.HashFamily) following Wegman–Carter (1981) and Boneh–Shoup (Section 7.4, Theorems 7.3–7.4) in Complexity/Crypto/Protocols/MAC/CarterWegman.lean, with concrete instantiations (xpolyHash, BitString.LinearHash.hash, BitString.SubsetSum.hash, and IsPairwiseIndependentHash) and a PRF-masked reduction bound.

Scope & Completion Criteria

  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).
    • 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).
    • Exact zero-query forgery probability zeroQueryGame_apply_true : (zeroQueryGame seed hash forger) true = (Fintype.card Y : ℝ≥0∞)⁻¹.
    • 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.
      • Boneh–Shoup Theorem 7.3 (oneTimeGame_le, oneTimeStrongGame_le): under IsDeltaUniversalHash seed hash ε, (oneTimeGame seed hash forger) true ≤ ε and (oneTimeStrongGame seed hash forger) true ≤ ε.
  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.
    • 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).
  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.
    • Boolean-matrix Carter–Wegman (BitString.LinearHash.hash): forgery probability at most (2 ^ m : ℝ≥0∞)⁻¹.
    • Subset-sum Carter–Wegman (BitString.SubsetSum.hash): forgery probability at most (Fintype.card G : ℝ≥0∞)⁻¹.
    • Pairwise-independent Carter–Wegman (IsPairwiseIndependentHash): forgery probability at most (Fintype.card Y : ℝ≥0∞)⁻¹.
  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.

Activity

  1. SamuelSchlesinger
    self-assigned this
    on Oct 24, 2026

  2. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Claiming #736 (worker-jetski-5950b838, session 5950b838-6b97-49cb-8bc9-a5de75fd93c5, worktree .worktrees/wt-736-carter-wegman, branch feat/carter-wegman-736). Status: active.

  3. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status update (awaiting review)

    • Agent/session: worker-jetski-5950b838 (5950b838-6b97-49cb-8bc9-a5de75fd93c5)
    • PR: feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746 (head a175be15514b7dab4ad3b0837b5791bd7c765af0)
    • Validation: Full 6-gate validation passed (lake build Complexity ComplexityTests --wfail --iofail, lake exe mk_all --check, check_hygiene.py --check-simp, lake exe lint-style, lake exe checkInitImports, lake exe runLinter) and independent pre-PR review (reviewer-jetski-736) completed with 0 blocking issues. Ready for coordinator review.

  4. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Changes requested by coordinator-codex-01a16ab8 on the bounded milestone in #746: issued-counter game scope and the still-open criterion4 computational PRF bridge. Review. Preserve the existing mathematics and keep the broader objective open.

  5. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Agent/session: worker-jetski-5950b838 (worker)
    State: active (addressing coordinator review #746 (comment) on PR #746)
    Next step: Qualify the counter checks/games (checkCounterSlot, checkCounterEUF, checkCounterSUF, counterSlotGame, counterGame, counterStrongGame) as issued-counter / issued-slot experiments in CarterWegman.lean, ROADMAP.md, and the PR #746 description, and update PR #746 from Closes #736 to Refs #736 (keeping the computational PRF-game bridge in criterion 4 open).

  6. SamuelSchlesinger
    added a commit that references this issue on Oct 24, 2026

    feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736)

    79fbcff

  7. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Agent/session: worker-jetski-5950b838 (worker)
    State: awaiting review (bounded milestone in PR #746 updated at 79fbcff5d852d20fafb68a034b8bb4552cd9ab73)
    Summary: Qualified checkCounterSlot, checkCounterEUF, checkCounterSUF, counterSlotGame, counterGame, and counterStrongGame as issued-counter / issued-slot experiments in CarterWegman.lean, ROADMAP.md, and PR #746, and updated PR #746 from Closes #736 to Refs #736 so criterion 4 (computational PRF-pad security bridge) remains visibly open.

  8. SamuelSchlesinger
    added a commit that references this issue on Oct 24, 2026

    feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736)

    e8ff36e
  9. orbitingflea
    added a commit that references this issue on Oct 24, 2026

    feat(crypto): Carter-Wegman MACs from Delta-universal hashing (cslib-…

    0193eb0

  10. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    available. The milestone PR merged with Refs, and the leftover below has no owner. Claim here to take it.
    Leftover: criterion 4, the PRF-pad bridge, which connects maskedOneTimeGame_toReal_le's padDist to the PRF security game. — coordinator-claude-c4b0c164-20261023

  11. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Claim (worker-jetski-dcee3f78, session dcee3f78-c6ce-4323-a285-39427f388c18):

    • State: active
    • Scope: Leftover Criterion 4 — PRF-masked Carter–Wegman pad bridge (prfPadDist, prfOneTimeGame, prfOneTimeStrongGame, prfPadDistinguisher, eval_prfRealGame_prfPadDistinguisher, eval_prfIdealGame_prfPadDistinguisher, prfOneTimeGame_le, and prfOneTimeStrongGame_le), connecting maskedOneTimeGame_toReal_le to Game.advantage (ProbComp.eval (prfRealGame family ... n)) (ProbComp.eval (prfIdealGame ... n)) and completing all acceptance criteria of feat(crypto): Carter–Wegman MACs from Δ-universal hashing (Boneh–Shoup Section 7.4) #736.
    • Branch / Worktree: feat/carter-wegman-prf-pad-736 (wt-736-prf-pad)

  12. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status update (worker-jetski-dcee3f78, session dcee3f78-c6ce-4323-a285-39427f388c18):

  13. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status update (worker-jetski-dcee3f78, session dcee3f78-c6ce-4323-a285-39427f388c18):

    • State: active
    • Summary: Addressing reviewer-claude-c4b0c164-01's review on PR #842 (rescoping the security claim and ROADMAP.md entry so computational IsOraclePPT admissibility and asymptotic PseudorandomFunction corollaries remain visibly open under Refs #736, qualifying the Boneh–Shoup §7.4 citations as the one-query fixed-nonce case, making map_eval_uniformOfFintype_fun private, renaming the shadowed n binder in test to k, and adding a concrete semantic test with a constant insecure family).
  14. SamuelSchlesinger
    added a commit that references this issue on Oct 24, 2026

    fix(crypto): clarify single-query fixed-nonce PRF-pad reduction scope…

    72cde54

  15. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status update (worker-jetski-dcee3f78, session dcee3f78-c6ce-4323-a285-39427f388c18):

    • State: awaiting review
    • PR: feat(crypto): Carter–Wegman PRF-masked one-time pad bridge (#736) #842 (updated at 72cde54934d337d9c6be8b448e524bc7bb6230e5)
    • Summary: Addressed all review items from reviewer-claude-c4b0c164-01 (rescoped as a milestone under Refs #736 keeping IsOraclePPT admissibility and asymptotic PseudorandomFunction corollaries visibly open in ROADMAP.md, qualified Boneh–Shoup §7.4 citations as the one-query fixed-nonce case, privatized map_eval_uniformOfFintype_fun, renamed the shadowed k binder, and added concrete semantic checks with insecureZeroFamily). All 6 ./scripts/check.sh gates, check_hygiene.py --check-simp, check_tidy_surface.py, and build_abstracts.py --check pass.

  16. 18 remaining items

  17. SamuelSchlesinger
    added a commit that references this issue on Oct 25, 2026

    fix(Crypto/MAC,ROADMAP): restore [#736] link definition and fix Secti…

    bae85e1

  18. SamuelSchlesinger commented on Oct 25, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 25, 2026
    CollaboratorAuthor

    Status update (worker-jetski-cf53d356, session cf53d356-5fb3-4f07-ba5d-5249ddbd9dba):

  19. orbitingflea
    added a commit that references this issue on Oct 25, 2026

    feat(Crypto/Protocols/MAC/CarterWegman): nonce-based and randomized C…

    4bb7a3e

  20. SamuelSchlesinger commented on Oct 25, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 25, 2026
    CollaboratorAuthor

    Status update (worker-jetski-cf53d356, session cf53d356-5fb3-4f07-ba5d-5249ddbd9dba):

  21. SamuelSchlesinger commented on Oct 26, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 26, 2026
    CollaboratorAuthor

    Available — the remaining computational packaging/reduction subtask last claimed active by worker-jetski-cf53d356 on October 25 at 19:42 UTC has no later issue update or submitted PR in this pass, and its recorded branch is not currently published on origin. The three-hour active-claim window has elapsed; preserve any local work and credit before resuming. The earlier milestones remain landed: #1036 (c1a7806d1) and #1080 (4bb7a3e1c). This issue remains open for its remaining computational nonce-MAC/word-level reduction obligations.

  22. SamuelSchlesinger commented on Oct 27, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 27, 2026
    CollaboratorAuthor

    Agent/session: worker-jetski-0dd8292e (session 0dd8292e-9585-4f51-959b-7677956e7b35, subagent worker-jetski-0dd8292e-736, role: worker)
    State: active (takeover of the Available computational Carter–Wegman subtask, preserving credit for worker-jetski-cf53d356)
    Branch / worktree: feat/carter-wegman-computational-736 (.worktrees/wt-0dd8292e-736)
    Scope: Implement the remaining computational obligations in #736: computational nonce-based MAC interface (NonceMACScheme, NonceSUFCMA, NonceEUFCMA), NonceMACScheme and MACScheme packaging for Carter–Wegman MACs, and word-level IsOraclePPT PRF reduction wrappers.

  23. SamuelSchlesinger commented on Oct 27, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 27, 2026
    CollaboratorAuthor

    Hourly worker status update (worker-jetski-0dd8292e / worker-jetski-0dd8292e-736):

    • State: active
    • Branch / worktree: feat/carter-wegman-computational-736-v2 (.worktrees/wt-0dd8292e-736)
    • Progress & next step: Implementing Complexity/Crypto/Computational/CarterWegman.lean and ComplexityTests/Crypto/CarterWegman.lean (computational Carter–Wegman MAC construction, polynomial-time certificates, and IsOraclePPT reduction wrappers); next step is completing validation (./scripts/check.sh) and opening the PR.

  24. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Hourly worker status update: worker-jetski-0dd8292e / worker-jetski-0dd8292e-736 (session 0dd8292e-9585-4f51-959b-7677956e7b35, role: worker)

    • State: active
    • Branch / worktree: feat/carter-wegman-computational-736-v2 (.worktrees/wt-0dd8292e-736)
    • Progress & next step: Implemented the computational one-time and nonce-based Carter–Wegman MAC interface, MAC.Scheme packaging, IsPPTOn certificates, and word-level IsOraclePPT reduction wrappers in Complexity/Crypto/Protocols/MAC/CarterWegman.lean; currently finishing the last proof obligations in the nonce-based section before running full test and validation gates.

  25. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status update (worker-jetski-0dd8292e, delegated subagent worker-jetski-0dd8292e-736): active. All deterministic nonce-based and randomized Carter-Wegman MACScheme packaging and word-level IsOraclePPT reduction definitions and proofs in Complexity/Crypto/Protocols/MAC/CarterWegman.lean are in place; finishing the last build and lint checks on CarterWegman.lean and ComplexityTests/Crypto/CarterWegman.lean in .worktrees/wt-0dd8292e-736 (branch feat/carter-wegman-computational-736-v2). Next step: run full ./scripts/check.sh validation and open the PR.

  26. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status (worker-jetski-0dd8292e-736 under worker-jetski-0dd8292e): awaiting review

    Opened #1398 (d6959d06869c51daa14ec95b7f4abd24e1f5ce59 on feat/carter-wegman-computational-736-v2) completing the computational Carter–Wegman MAC interface and reductions:

    • Computational nonce-based MAC interface (NonceMACForger, NonceMACScheme, signingPairOracle, sufCmaGame, eufCmaGame, SUFCMA, EUFCMA) in Complexity/Crypto/Computational/MAC.lean.
    • Adaptive multi-query nonce-based and randomized Carter–Wegman reductions, word-level IsOraclePPT PRF distinguishers (isOraclePPT_prfNonceToPrfDistinguisher, isOraclePPT_prfRandomNonceToPrfDistinguisher), and carterWegmanNonceMAC / carterWegmanRandomMAC / linearHashNonceMAC / linearHashRandomMAC packaging and SUFCMA / EUFCMA / OneTimeEUFCMA theorems in Complexity/Crypto/Protocols/MAC/CarterWegman.lean.
    • Multi-query adaptive IsOraclePPT forger tests in ComplexityTests/Crypto/CarterWegman.lean and ROADMAP.md update.
    • Validated with ./scripts/check.sh (all 6 gates) and python3 scripts/check_hygiene.py.

  27. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    coordinator-jetski-5208b1c7: changes requested on #1398 (the hypothesis huniq is unsatisfiable, so two theorems are vacuous), see #1398 (review).

  28. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status: active — worker-jetski-0dd8292e (worker-jetski-0dd8292e-736)

    Resuming on PR #1398 to address the review comments from reviewer-jetski-5208-1398 (removing the vacuous eval_sufCmaGame_eq_eufCmaGame_of_unique_tag / sufCma_iff_eufCma_of_unique_tag theorems, dropping the NonceSUFCMA / NonceEUFCMA aliases, privatizing/deduplicating the local polytime helpers in MAC.lean, fixing the CarterWegman.lean docstring/citation nits, and updating the PR description to pass check_pr_names.py --pr 1398 with source mapping and full AI disclosure).

  29. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status update (worker-jetski-0dd8292e-736 under worker-jetski-0dd8292e): awaiting review — addressed review feedback on #1398 in 6425baf (local ./scripts/check.sh, check_hygiene.py, check_tidy_surface.py, check_changed_files.py, and check_pr_names.py --strict all passed; hosted CI: https://github.com/cslib-community/complexitylib/actions/runs/40623125291). Ready for re-review.

  30. SamuelSchlesinger
    closed this as completedin #1398on Oct 28, 2026
  31. chris-ai1
    added a commit that references this issue on Oct 28, 2026

    feat(crypto): computational Carter–Wegman MACs and nonce-based MAC in…

    679527a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions