A decision criterion for torsion-point leakage

Formal statement

Setting. An isogeny-based protocol reveals, alongside its curves, auxiliary information $\mathcal I$, typically including images of torsion points under a secret isogeny.

Find. Necessary and sufficient conditions on $\mathcal I$ for a Kani-embedding or higher-dimensional isogeny attack to apply.

Realistic target. Produce a mechanically applicable checklist whose inputs are protocol-level leakage parameters and whose outputs distinguish:

• a published attack theorem that applies;
• a published attack strategy whose remaining hypotheses require a protocol-specific witness;
• no known Kani-embedding route from the public transcript.

The checklist must classify SIDH and SIKE as vulnerable and CSIDH as not vulnerable by this attack family. It must trace each condition to a published attack requirement, stress-test boundary cases, and avoid presenting a merely sufficient condition as necessary.

Requested deliverables

1. A precise requirement analysis separating required inputs from conveniences.
2. A leakage-parameter vocabulary.
3. A protocol comparison table covering SIDH, SIKE, CSIDH, and SQIsign, plus any relevant newer protocol whose sources can be verified.
4. An ordered decision procedure with a verdict at every leaf.
5. Boundary stress-tests with verdicts and justifications.
6. An explicit decision whether to implement a toy attack.

State in five lines

PROVED The project is abandoned and recorded as failure at the user's request. PROVED The universal necessary-and-sufficient leakage criterion was not proved. PROVED A scoped R8/K2-CD/K2-MM invocation checklist remains as a partial artifact. PROVED Coordinate-level leakage closure and numerical K2 checks were implemented. PROVED A001 and A002 are dead; Q011 is the mathematical obstruction.

What is established (tagged)

• CITED Full rank-two smooth torsion action can trigger Robert's dimension-8 recovery route under its degree, access, and recovery hypotheses (Robert 2023).
• CITED K2 surface routes need protocol-specific auxiliary construction witnesses in addition to degree identities (Castryck--Decru 2023; Maino--Martindale 2023).
• PROVED Source records in $(\mathbb Z/N\mathbb Z)^2$ span the full module exactly when $N$ and all $2\times2$ source minors have gcd one; Section 8 of CHECKLIST.md contains the proof.
• PROVED Same-map action matrices combine across orders only with compatible bases and generalized-CRT agreement on the overlap.
• EMPIRICAL: 15 P3.4 test methods Classifier, closure, and surface-certificate tests pass; 61 shared tests also pass.

What is ruled out

• A001 is dead: finite published-template normalization cannot prove universal necessity against unenumerated higher-dimensional attacks.
• A002 is dead: mechanizing leakage closure and integer certificates does not close the same template-completeness gap.
• PROVED A valid numerical K2 identity does not prove that an auxiliary isogeny exists or is efficiently evaluable.

Active thread

None. The problem is abandoned.

Next action

None unless explicitly reopened. A reopening should address Q011 before adding more classifier fields.

Invariants -- do not violate

• NO_PUBLISHED_ROUTE is not a security proof.
• Do not mix records from different target maps or incompatible torsion bases.
• Keep numerical K2 validity separate from construction/evaluation evidence.
• Do not describe the partial checklist as a universal necessary condition.

Files that matter

• CHECKLIST.md: partial scoped result and failure banner.
• attempts/A001-known-attack-checklist.md: first failure post-mortem.
• attempts/A002-derived-leakage-closure.md: second failure post-mortem.
• code/leakage_checklist.py: scoped classifier.
• code/leakage_closure.py: coordinate-level action derivation.
• code/surface_certificates.py: numerical K2 checks only.
• OPEN_QUESTIONS.md Q011: missing universal-completeness theorem.

What I would tell my replacement

PROVED The partial implementation is not the failed part; the failure is the unclosed quantifier over all Kani embeddings and higher-dimensional recovery routes. More fixtures cannot resolve that logical gap.