Repository navigation
Shared lazy bidirectional random-permutation sampler for ideal-permutation proofs #834
Description
Two crypto results are blocked on the same missing piece of shared infrastructure: a lazily sampled random permutation with forward and inverse queries, together with its coupling to a uniformly random permutation.
- feat(crypto): Even–Mansour cipher in the ideal-permutation model (Boneh–Shoup Section 4.7) #761, Even–Mansour (feat(crypto): Even–Mansour cipher in the ideal-permutation model (#761) #772 merged): turning the proved bad-key bound into
Game.advantage ≤ 2·Q_e·Q_π/|G|needs the lazy bidirectional coupling. - feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748, Luby–Rackoff (feat(crypto): Feistel networks and the Luby-Rackoff theorem (#748) #752 merged): the quantitative bound against
idealStrongGameand the PRP-switching step (the 3-round result is proved againstrandomFunctionGame) need the same sampler.
The #733 friction log already records this.
Done when:
- a lazy bidirectional permutation oracle exists, shared in the Crypto or Probability foundations;
- a proof shows that its query distribution equals one drawn from a uniformly random
Equiv.Perm, up to the standard collision bound; - one client, either feat(crypto): Even–Mansour cipher in the ideal-permutation model (Boneh–Shoup Section 4.7) #761's final bound or feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748's switching step, uses it.
Follow Boneh–Shoup's treatment (the ideal-permutation model, Section 4.7, and the PRF switching lemma, Section 4.4.3). Look for existing OracleComp caching and lazy-sampling machinery before adding new machinery, and check what VCVio does here; adopt it only if it is clearly better.
Status: available. Claim it here before starting.
🤖 Generated with Claude Code
Metadata
Metadata
Assignees
Labels
No labels
Activity
SamuelSchlesinger commentedon Oct 24, 2026
Worker Claim (
worker-jetski-5950b838, session5950b838-6b97-49cb-8bc9-a5de75fd93c5)activefeat/lazy-bidirectional-perm-834(.worktrees/wt-834-lazy-perm)Complexity/Languages/Probabilistic/RandomPermutation.lean), reusingOracleComp.run_interpret_simulation_of_invariantandOracleComp.IdenticalUntilBadto prove:π ← PMF.uniformOfFintype (Equiv.Perm α)and the lazy bidirectional permutation samplerRandomPermutation.answer;Q.choose 2 / |α|, Boneh–Shoup Section 4.4.3 & Section 4.7) against forgetful lazy sampling /RandomOracle.answer.LubyRackoff.lean(feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748, 3-round PRP bound againstidealPermGameand quantitative1 - O(|G|⁻¹)CCA bound againstidealStrongGame) and/orEvenMansour.lean(feat(crypto): Even–Mansour cipher in the ideal-permutation model (Boneh–Shoup Section 4.7) #761,Game.advantage ≤ 2 * Q_e * Q_π / |G|).SamuelSchlesinger commentedon Oct 24, 2026
Status update (
worker-jetski-5950b838/5950b838-6b97-49cb-8bc9-a5de75fd93c5)awaiting reviewfeat/lazy-bidirectional-perm-834ate089e2eff4f8f1d7ae0f985468725e1374d9c61c)Complexity.Languages.Probabilistic.RandomPermutation(PermQuery,PermOracleSpec,evalPerm,answer,answer_complete,uniform_interpret_eq_lazy,toOuterMeasure_bad_choose_two_le,uniformPerm_bind_apply_le_forgetful,abs_sub_uniformPerm_forgetful_le,abs_sub_uniformPerm_uniformFunc_le), upgradedLubyRackoff.lean(simplifiedtoOuterMeasure_hasVCollision_le, added 3-round PRP bounds againstidealPermGame, and proved the quantitative nonnegligible CCA advantage lower bound1 - |G|⁻¹ - 4 * |G|⁻¹ ^ 2 ≤ Game.advantage ...againstidealStrongGameinle_advantage_feistel3CCAAttack_idealStrongGame_of_ne), and upgradedEvenMansour.lean(re-exportedPermQuery/PermOracleSpec/evalPermand provedevenMansourIdealGame_eq_lazy). Full validation and independent review (APPROVEbyreviewer-jetski-lazy-perm-834) are recorded on feat(Languages/Probabilistic): add shared lazy bidirectional random-permutation sampler (#834) #853.fix(Languages/Probabilistic): address coordinator review on RandomPer…
SamuelSchlesinger commentedon Oct 24, 2026
Status update (
worker-jetski-5950b838, session5950b838-6b97-49cb-8bc9-a5de75fd93c5)awaiting reviewfeat/lazy-bidirectional-perm-834atab877c3743dbcbe58a38ccfb955fa56bf0b579a3)ab877c3743dbcbe58a38ccfb955fa56bf0b579a3(fixed[BonehShoup2023]citation, privatized internal coupling helpers, inlinedRandomPermutationnames inEvenMansour.lean, and added concreteFin 3test instances and#print axiomsguards inComplexityTests/Crypto/LubyRackoff.lean). Ready for coordinator re-review.feat(Languages/Probabilistic): add shared lazy bidirectional random-p…
doc(crypto): align Luby-Rackoff and Carter-Wegman entries in ROADMAP (c…