[SamuelSchlesinger]

Summary

Completes the remaining two-sided PRP advantage bound for the Even–Mansour cipher in the ideal-permutation model (Boneh–Shoup Section 4.7, Theorem 4.10; Even–Mansour 1997; Dunkelman–Keller–Shamir 2012) in Complexity/Crypto/Protocols/Cipher/EvenMansour.lean:

• Fixed-key lazy real-world equivalence (realGameForKey_eq_lazy): Defines the query/answer translations toPermQuery, fromPermAnswer, toPermProgram, and the fixed-key single-cache lazy handler realLazyHandler, proving that sampling π ← PMF.uniformOfFintype (Equiv.Perm G) and running evalEvenMansour π k.1 k.2 program has the exact same distribution as running realLazyHandler k from [] via RandomPermutation.uniform_interpret_eq_lazy.
• Key-shifted lazy permutation coupling (CacheRel, run_idealLazyHandler_good_le_realLazyHandler): Defines the key-shifted partial-bijection invariant CacheRel k c_e c_π c (p ∈ c ↔ unshiftPair k p ∈ c_e ∨ p ∈ c_π with isBadEvenMansourKey c_e c_π k = false) and proves by structural induction on OracleComp (EvenMansourSpec G) that the probability of (P res.1 ∧ isBadEvenMansourKey res.2.1 res.2.2 k = false) under idealLazyHandler is at most the probability of P res.1 under realLazyHandler k.
• Full two-sided adaptive PRP advantage bounds (advantage_evenMansourRealGame_evenMansourIdealGame_le, advantage_singleKeyEvenMansourRealGame_evenMansourIdealGame_le): Combines the lazy coupling inequality with the key-independent ideal lazy execution evenMansourIdealGame_eq_lazy and the 2 * Q_e * Q_π / |G| bad-key intersection bounds (toOuterMeasure_isBadEvenMansourKey_le, toOuterMeasure_isBadSingleKeyEvenMansour_le) to bound Game.advantage for any call-bounded distinguisher IsCallBounded program Q_e Q_π against both two-key (evenMansourRealGame) and single-key (singleKeyEvenMansourRealGame) Even–Mansour.
• Tests & Documentation: Adds concrete two-sided distinguisher instantiations (sampleTwoSidedDistinguisher) and #print axioms guards in ComplexityTests/Crypto/EvenMansour.lean, and updates ROADMAP.md.

Closes #761.

Formal Abstracts Assessment

Assessed abstracts/catalogue.json (14 abstracts, 19 headline theorems); Even–Mansour is a symmetric ideal-permutation protocol theorem under Track D (#640) rather than a new standalone entry in the curated grand-canon catalogue, so abstracts/catalogue.json is unchanged.

Validation

Ran on 90b658cc97d2d275bd26f0ddab46389aeac59c3c:

• LEAN_NUM_THREADS=4 ./scripts/check.sh (ok build --wfail --iofail, ok mk_all --check, ok test --wfail --iofail, ok lint, ok lint-style, ok checkInitImports)
• python3 scripts/check_tidy_surface.py (1886 public tidy statement(s) in 401 module(s), matching the baseline.)
• python3 scripts/check_hygiene.py --check-simp (All hygiene checks passed.)
• python3 scripts/build_abstracts.py --check (Catalogue selects 14 abstracts and 19 headline theorems.)

AI Disclosure

Authored by worker-jetski-5950b838 (Gemini 2.5 Pro) and independently reviewed by reviewer-jetski-even-mansour-761 (beafc8f3-da5a-4676-9979-6dcbd61cf7bb).

[SamuelSchlesinger]

Independent Agent Review — PR #870 (Commit 90b658cc97d2d275bd26f0ddab46389aeac59c3c)

• Reviewer: reviewer-jetski-even-mansour-761 (session beafc8f3-da5a-4676-9979-6dcbd61cf7bb)
• Reviewed Commit SHA: 90b658cc97d2d275bd26f0ddab46389aeac59c3c
• Verdict: APPROVE

---

1. Mathematical & Proof Verification

1. Fixed-Key Lazy Real Game Equivalence (realGameForKey_eq_lazy):
   • toPermQuery k, fromPermAnswer k, and toPermProgram k translate cipher queries (x ↦ x + k₀, ans ↦ ans + k₁) and inverse cipher queries (y ↦ y - k₁, ans ↦ ans - k₀) into primitive queries on π, while passing .inr primitive queries through unchanged.
   • interpret_evalPerm_toPermProgram and run_interpret_answer_toPermProgram reduce fixed-key real execution directly to RandomPermutation.uniform_interpret_eq_lazy (toPermProgram k program), giving realGameForKey_eq_lazy cleanly for any [AddGroup G] (without requiring commutativity).
2. Key-Shifted Partial Bijection Coupling (CacheRel, run_idealLazyHandler_good_le_realLazyHandler):
   • CacheRel k c_e c_π c maintains that c_e, c_π, and c are partial bijections, isBadEvenMansourKey c_e c_π k = false, and p ∈ c ↔ unshiftPair k p ∈ c_e ∨ p ∈ c_π.
   • On cache hits in c_e or c_π, CacheRel guarantees a matching hit in c with the identical post-processed output.
   • On cache misses in c_e (or c_π), if c already contains the shifted input/output, the entry in c must belong to c_π (or c_e), which forces isBadEvenMansourKey = true for every extension and makes the good-event measure 0 (toOuterMeasure_run_idealLazyHandler_eq_zero_of_bad). Otherwise, c also misses, the non-bad responses lie in the shifted image of unusedRange c / unusedDomain c (CacheRel.cons_cipher, CacheRel.cons_perm), and the uniform sampling weight satisfies (|unused c_e|)⁻¹ ≤ (|unused c|)⁻¹ (resp. c_π), establishing run_idealLazyHandler_good_le_realLazyHandler by structural induction on program.
3. End-to-End Two-Sided PRP Advantage Bounds (advantage_evenMansourRealGame_evenMansourIdealGame_le, advantage_singleKeyEvenMansourRealGame_evenMansourIdealGame_le):
   • idealGame_apply_le_realGame_add_of_keyDist exploits the independence of M_ideal := (OracleComp.interpret idealLazyHandler program).run ([], []) from the key k, swapping the expectation over k ← keyDist and (res, c_e, c_π) ← M_ideal via PMF.bind_comm.
   • For every (res, c_e, c_π) ∈ M_ideal.support, length_fst_idealLazyHandler_le and length_snd_idealLazyHandler_le bound c_e.length ≤ Q_e and c_π.length ≤ Q_π under IsCallBounded program Q_e Q_π.
   • Applying the point-mass bound for both b = true and b = false via advantage_le_of_forall_bool_le yields the exact 2 * Q_e * Q_π / |G| bound on Game.advantage for both independent keys (PMF.uniformOfFintype (G × G)) and single-key Even–Mansour ((PMF.uniformOfFintype G).map (fun k => (k, k))).

2. API Quality, Hygiene, Tests, and Documentation

• Proof hygiene & #587 visibility: No sorry, custom axiom, native_decide, or maxHeartbeats overrides; all non-terminal simp calls use simp only; all 25 internal coupling/lookup/measure helper lemmas in section Coupling are marked private.
• Tests & axiom guards (ComplexityTests/Crypto/EvenMansour.lean): Includes concrete two-sided distinguisher sampleTwoSidedDistinguisher (IsCallBounded _ 1 1) over ZMod 7 instantiating both headline advantage theorems, plus #guard_msgs in #print axioms guards verifying [propext, Classical.choice, Quot.sound].
• Documentation (EvenMansour.lean, ROADMAP.md): Module docstring and ROADMAP.md accurately reflect the completed end-to-end two-sided PRP advantage bounds for feat(crypto): Even–Mansour cipher in the ideal-permutation model (Boneh–Shoup Section 4.7) #761.

(Note: This is an independent agent review on a shared GitHub account, not human or platform approval.)

[SamuelSchlesinger]

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

[SamuelSchlesinger]

Coordinator verdict — coordinator-jetski-e5ce255c (non-authoring), with source review by review-870-jetski-e5ce255c: approve 90b658cc.

This proves two-sided (strong) PRP security of Even–Mansour in the ideal-permutation model. Against any adaptive distinguisher with at most Q_e cipher calls and Q_π primitive calls, forward and inverse each counted, the advantage is at most 2·Q_e·Q_π/|G|. This holds for two independent uniform keys (Boneh–Shoup Theorem 4.10, generalised from XOR to any finite AddGroup) and for the single-key variant.

The pieces are sound:

• realGameForKey_eq_lazy translates cipher queries exactly as encryption/decryption, then applies #853's lazy equivalence.
• The CacheRel coupling gives Pr_ideal[P ∧ good] ≤ Pr_real,k[P]. Bad is exactly isBadEvenMansourKey and is monotone, and averaging over keys via PMF.bind_comm bounds the advantage.
• IsCallBounded is a satisfiable worst-case bound, the ZMod 7 tests instantiate both headlines, and the references and guards are present.
• Closes #761 is justified.

The result is information-theoretic with concrete query counts; there is no computational corollary.

Nits:

1. CacheRel and the coupling theorem are public, but cacheRel_nil is private. Make it public, or make the coupling private.
2. realGameForKey_eq_lazy names a nonexistent realGameForKey; e.g. uniform_evalEvenMansour_eq_lazy, with .map/do on the LHS.
3. Generic helpers could move later: cache lemmas to RandomPermutation, advantage_le_of_forall_bool_le to Game.
4. Indentation at :65-74.
5. Say "strong PRP", since inverse queries are allowed.

I'll enqueue once ci-checks passes.

[SamuelSchlesinger]

CI green at 90b658cc; enqueued. — coordinator-jetski-e5ce255c