Canonical decision explorer
secp256k1 ECDLP route map
Every route is generated from repo/ECDLP_DECISION_SUBSTRATE.json.
Search by mechanism, scope, evidence, or next action.
Evaluated routes
17 routes
Generic-group lower boundR-GENERIC-LOWER-BOUND
Guardrail
R-GENERIC-LOWER-BOUNDApplicability
direct within the generic-group model
Known cost
Omega(sqrt(n)) generic queries, under the exact formal model and success assumptions.
Current evidence
The collision-counting core and square-root consequence are Lean-verified.
Assumptions
Generic encodings reveal no exploitable representation structure.; Complexity is measured in oracle queries with bounded success probability.
Success gate
Any classical plain-input route must identify and justify the non-generic information that escapes this model.
Stop condition
Reject proposals that merely relabel generic operations or hide work in preprocessing.
Next action
Retain as a mandatory comparison and scope guard; no new experiment.
Evidence files
Ecdlp/Proved/GenericGroupBound.leannotes/SECURITY_SCOPE.md
Baby-step giant-step and Pollard rhoR-GENERIC-BASELINE
Baseline
R-GENERIC-BASELINEApplicability
direct
Known cost
Theta(sqrt(n)) group work; BSGS uses Theta(sqrt(n)) memory while rho can use negligible memory with parallel variants.
Current evidence
Core decomposition, step bound, and collision/periodicity statements are Lean-verified; implementation constants are not a secp256k1 break.
Assumptions
Ord(P) is known.; No special target structure is required.
Success gate
Every candidate route must beat the correct time-memory-precomputation baseline under the same input model.
Stop condition
Do not present hardware scaling or parallel rho as an asymptotic improvement.
Next action
Use as the benchmark comparator in the evaluation harness.
Evidence files
Ecdlp/Proved/BabyStepGiantStep.leanEcdlp/Proved/PollardRho.lean
GLV endomorphism accelerationR-GLV
Constant factor
R-GLVApplicability
direct
Known cost
Known use is a constant-factor acceleration or search-space symmetry; no justified o(sqrt(n)) plain-input algorithm follows.
Current evidence
The rational point action, eigenvalue scope on multiples of G, and orbit facts are Lean-verified.
Assumptions
Use the secp256k1 order-3 endomorphism and its eigenvalue on the generator subgroup.
Success gate
Promotion requires a mechanism that changes relation-generation or search complexity, not only orbit size.
Stop condition
Close any proposal whose only gain is a finite orbit quotient or scalar decomposition.
Next action
Keep as target structure available to a selected route; do not treat it as a standalone attack.
Evidence files
Ecdlp/Proved/GlvTorsionAction.leanexperiments/p0_glv_semaev/RESULTS.md
Pohlig-Hellman subgroup reductionR-POHLIG-HELLMAN
Ruled out for target
R-POHLIG-HELLMANApplicability
the algorithm applies, but secp256k1 has no smaller prime-order factors to exploit
Known cost
Dominated by the largest prime factor of ord(P); for secp256k1 that factor is n itself.
Current evidence
n is Lean-verified prime and the reduction/reconstruction algebra is formalized.
Assumptions
A useful factorization of ord(P) into smaller factors.
Success gate
A proposal must exhibit an actual nontrivial subgroup decomposition of the target instance.
Stop condition
Stop immediately for the standard generator subgroup because n is prime.
Next action
Retain as a machine-checked elimination certificate.
Evidence files
Ecdlp/Proved/Secp256k1PrimeN.leanEcdlp/Proved/PohligHellman.lean
MOV, Frey-Ruck, and Tate/Weil pairing transferR-PAIRING-TRANSFER
Ruled out for target
R-PAIRING-TRANSFERApplicability
no useful low-embedding-degree transfer is available for secp256k1
Known cost
Transfer is only useful when finite-field DLP in F_(p^k) is easier at the target's embedding degree k.
Current evidence
Lean proves the secp256k1 embedding degree is greater than 100, which is a strong practical exclusion of low-degree MOV-style transfers.
Assumptions
The n-torsion embeds into a finite-field multiplicative group of tractable extension degree.; The relevant pairing is non-degenerate on available points.
Success gate
A proposal must state the exact pairing, available torsion points, extension degree, and finite-field DLP cost.
Stop condition
Reject low-degree-transfer claims inconsistent with the verified embedding-degree bound.
Next action
Keep the target-specific exclusion; defer a full pairing library unless a new route needs it.
Evidence files
Ecdlp/Proved/EmbeddingDegree.leanBARRIERS.md
Smart, Satoh-Araki, and Semaev anomalous-curve liftingR-ANOMALOUS-PADIC
Ruled out for target
R-ANOMALOUS-PADICApplicability
inapplicable because secp256k1 is not anomalous
Known cost
Polynomial-time for the anomalous special case; the prerequisite fails here.
Current evidence
Lean proves the anomalous iff trace-one scope and that secp256k1 is ordinary and non-anomalous.
Assumptions
#E(F_p) = p, equivalently trace one in the relevant setting.
Success gate
A p-adic proposal must identify a different valid degeneracy and prove it holds for secp256k1.
Stop condition
Stop Smart/SSSA instantiation when #E(F_p) != p.
Next action
Retain the formal exclusion; do not build an elliptic formal-group stack for this target now.
Evidence files
Ecdlp/Proved/AnomalousScope.lean
Weil descent and GHS-style transferR-WEIL-DESCENT
Ruled out for target
R-WEIL-DESCENTApplicability
the standard extension-field descent mechanism has no nontrivial degree to exploit over the prime field F_p
Known cost
Useful only for selected extension-field settings; degree one gives no descent gain.
Current evidence
Target-field structure rules out the standard GHS setting; no dedicated Lean theorem is claimed.
Assumptions
The curve is defined over an extension field with exploitable descent geometry.
Success gate
A proposal must provide a concrete alternative descent object over F_p and a lower resulting DLP cost.
Stop condition
Reject arguments that silently replace the prime-field target with an extension-field family.
Next action
Document as a target-applicability exclusion; no formal stack now.
Evidence files
data/attack_registry.jsonnotes/SECURITY_SCOPE.md
Prime-field index calculusR-PRIME-FIELD-INDEX-CALCULUS
Open, parked
R-PRIME-FIELD-INDEX-CALCULUSApplicability
conceptually direct, with no validated subgeneric secp256k1 algorithm in the audited evidence
Known cost
No accepted plain-prime-field asymptotic improvement is established here; known toy systems encounter relation-yield, degree, and memory barriers.
Current evidence
S3/S4 foundations and limited toy measurements exist, but they do not establish a degree-of-regularity law or subgeneric scaling.
Assumptions
Efficient factor-base relation generation over a large prime field.; A tractable polynomial-system solving regime.; Linear algebra and descent costs that preserve any relation-generation gain.
Success gate
Provide an exact relation system, independent EC validation, a justified solving-cost model, and multi-size evidence consistent with o(sqrt(n)).
Stop condition
Park when gains rely only on factor-base constants, unvalidated Macaulay proxies, tiny fields, or hidden exhaustive enumeration.
Next action
Preserve evidence and prerequisites; wait for explicit route selection before any new experiment.
Evidence files
Ecdlp/Proved/SemaevThree.leanEcdlp/Proved/SemaevFour.leanexperiments/p1_petit_m3/RESULTS.md
GLV-symmetrized Semaev systemsR-GLV-SEMAEV
Open, parked
R-GLV-SEMAEVApplicability
direct to the j=0 target structure, but only constant-factor evidence exists
Known cost
Measured finite-orbit reductions are constant-factor; the relevant higher-degree invariant-system cost is unresolved.
Current evidence
Lean verifies the GLV and Semaev structural ingredients. Existing experiments close only narrow lookup and toy-presentation windows.
Assumptions
Invariant coordinates reduce relation-generation complexity or solving degree, not only factor-base storage.; The quotient retains enough information to recover valid relations.
Success gate
Exhibit a nonredundant invariant S_m system and a theoretical reason for a lower asymptotic solving exponent, then validate it independently.
Stop condition
Stop if the gain is bounded by orbit size or disappears after complete relation-generation and recovery costs are counted.
Next action
Keep HYP_GLV_SEMAEV_001 parked until route selection explicitly promotes it.
Evidence files
experiments/p0_glv_semaev/RESULTS.mdexperiments/p3_sm_system/RESULTS.mdexperiments/p4_petit/RESULTS.md
Petit-style composed rational mapsR-PETIT-COMPOSED-MAPS
Open, parked
R-PETIT-COMPOSED-MAPSApplicability
unresolved because the repository has not implemented a faithful construction
Known cost
No reliable project estimate; the existing six-variable toy presentation is explicitly non-faithful and descriptive.
Current evidence
The current experiment is useful only as a negative control for one toy presentation.
Assumptions
A correctly specified low-degree rational map yields a useful factor-base or relation system.; Composition, solving, and recovery costs improve the full attack.
Success gate
First reproduce the exact construction from a verified primary source, then compare it under the common evaluation contract.
Stop condition
Reject low-bit filters, redundant auxiliary variables, or presentation-only degree changes as substitutes for the cited construction.
Next action
Park until the source specification and route-selection gate justify implementation.
Evidence files
experiments/p4_petit/README.mdexperiments/p4_petit/RESULTS.md
Elliptic divisibility sequences and division-polynomial re-encodingsR-EDS-DIVISION-POLYNOMIAL
Open, parked
R-EDS-DIVISION-POLYNOMIALApplicability
structurally direct, with no known independent information source or subgeneric inversion method
Known cost
Known recurrences evaluate W_m for a supplied m; they do not cheaply find the unknown first zero or discrete logarithm.
Current evidence
Lean formalizes substantial division-polynomial and normEDS structure. Toy measurements confirm apparition/torsion equivalence and no advantage.
Assumptions
A sequence or polynomial observable can be inverted more cheaply than scalar multiplication or exhaustive apparition search.
Success gate
Identify an observable computable from (P,Q) whose inversion provably avoids equivalent ECDLP work.
Stop condition
Stop when the construction only re-encodes scalar multiplication or requires Theta(ord(P)) search.
Next action
Keep HYP_WARD_EDS_001 parked; finish no additional point-division bridge unless a selected route needs it.
Evidence files
Ecdlp/Proved/NormEDSSomos4.leanexperiments/p2_ward_eds/RESULTS.md
Isogeny, endomorphism-ring, and Frobenius transferR-ISOGENY-ENDOMORPHISM-TRANSFER
Monitor
R-ISOGENY-ENDOMORPHISM-TRANSFERApplicability
no concrete efficiently computable transfer to a weaker target is identified
Known cost
Unspecified without a concrete target and map; special endomorphisms currently support constant-factor GLV acceleration.
Current evidence
The repository has target endomorphism facts but no general isogeny stack or candidate weak codomain.
Assumptions
An efficiently computable map reaches a curve or representation where DLP is materially easier.; Kernel and degree do not erase the gain.
Success gate
Provide an explicit map, target, DLP advantage, and end-to-end cost.
Stop condition
Do not formalize a general stack in advance of a concrete route.
Next action
Monitor literature and reuse GLV facts; no build now.
Evidence files
Ecdlp/Proved/GlvTorsionAction.leanBARRIERS.md
Multi-target and reusable-precomputation tradeoffsR-MULTI-TARGET-PRECOMPUTATION
Conditional inputs
R-MULTI-TARGET-PRECOMPUTATIONApplicability
not applicable to the primary one-target/no-precomputation objective unless costs are explicitly amortized
Known cost
Can change amortized constants and time-memory tradeoffs; it does not by itself solve an arbitrary single target below the proper total-cost baseline.
Current evidence
Covered in the attack registry as a separate conditioned model.
Assumptions
Many targets share a group or base point.; Precomputation storage and setup are available and counted separately.
Success gate
State target count, online/offline split, memory, reuse horizon, and total amortized cost.
Stop condition
Reject comparisons that omit precomputation or compare an amortized online phase to a full single-target baseline.
Next action
Represent in the evaluation contract; no experiment in this phase.
Evidence files
data/attack_registry.jsonnotes/SECURITY_SCOPE.md
Interval DLP, partial-key knowledge, and auxiliary-power algorithmsR-INTERVAL-AUXILIARY-INPUT
Conditional inputs
R-INTERVAL-AUXILIARY-INPUTApplicability
not applicable to an arbitrary full-range scalar without the promised interval or auxiliary data
Known cost
May reduce work relative to the conditioned search space; it does not alter the unconditioned n-sized instance.
Current evidence
The current target contract supplies neither an interval promise nor auxiliary powers.
Assumptions
k lies in a known small interval, or the attacker receives additional algebraic powers or relations involving k.
Success gate
Declare exactly how the auxiliary information is obtained and include its acquisition cost.
Stop condition
Reject any route that assumes the secret information it is meant to recover.
Next action
Keep as a scope category for future protocol or leakage analyses.
Evidence files
notes/SECURITY_SCOPE.md
Hidden-number and lattice attacks on biased or reused ECDSA noncesR-HNP-NONCE-LEAKAGE
Separate threat model
R-HNP-NONCE-LEAKAGEApplicability
important for key security but not a plain ECDLP algorithm
Known cost
Depends on leakage quality, sample count, and lattice dimension; a valid instance can recover a signing key without solving arbitrary ECDLP.
Current evidence
The repository catalogs the attack family but lacks an LLL/BKZ and HNP formal stack.
Assumptions
Signatures leak nonce bits, reuse nonces, or have a statistically exploitable bias.
Success gate
Keep leakage acquisition, statistical model, lattice reduction, and key verification explicit.
Stop condition
Do not classify nonce failures as a mathematical break of secp256k1 ECDLP.
Next action
Preserve as a separate security track; no lattice foundation build for the primary objective now.
Evidence files
data/attack_registry.jsonnotes/SECURITY_SCOPE.md
Invalid-curve, twist, fault, and side-channel routesR-PROTOCOL-FAULT-SIDECHANNEL
Separate threat model
R-PROTOCOL-FAULT-SIDECHANNELApplicability
relevant only when an implementation exposes attacker-controlled inputs or physical leakage
Known cost
Implementation-dependent and often far below generic DLP when the vulnerability exists.
Current evidence
Protocol algebra is formalized at an abstract level; implementation leakage is outside that proof model.
Assumptions
Missing point validation, unsafe scalar multiplication, fault injection, timing, power, cache, or electromagnetic leakage.
Success gate
Specify the concrete implementation, leakage channel, validation behavior, and key-recovery verification.
Stop condition
Keep mathematical protocol soundness separate from implementation hardening claims.
Next action
Record scope; do not expand the Lean substrate until a concrete implementation-verification goal exists.
Evidence files
notes/SECURITY_SCOPE.mdABSTRACT_SCOPE.md
Fault-tolerant quantum ECDLPR-QUANTUM-SHOR
Separate threat model
R-QUANTUM-SHORApplicability
algorithmically direct given sufficiently capable fault-tolerant quantum hardware
Known cost
Polynomial-time quantum algorithm. The 2026 audited preprint reports 835 logical qubits and 2^30.63 Toffoli gates for secp256k1; physical resources and availability are not established by that estimate.
Current evidence
Shor gives the algorithmic route; Luo et al. provide the current project-tracked logical-resource estimate.
Assumptions
Large-scale error-corrected quantum computation.; A reversible elliptic-curve implementation with the quoted logical resources.; Physical error correction overhead is separately accounted for.
Success gate
Distinguish algorithm, logical circuit, error-correction overhead, physical hardware, runtime, and availability.
Stop condition
Do not turn a logical-resource estimate into a claim that present hardware can break secp256k1.
Next action
Update the registry estimate and monitor primary literature; do not build a quantum Lean stack now.