Antje Worring
df4c537c16
True no-reconstruction threshold SLH-DSA is impossible in the no-dealer /
no-preprocessing model a public, leaderless, permissionless chain needs
(Kondi-Kumar-Vanegas: extractable hash-based signatures cannot be thresholded
by black-box hash use). Stop pretending otherwise.
De-cheat:
- DELETE the circular/vacuous proofs that manufactured false assurance:
Magnetar_N1_Atom_Refinement.ec, Magnetar_N1_SHAKE_Expand.ec,
Magnetar_N4_KeyDeriveStable.ec, lemmas/{Magnetar_CT,SLHDSA_Functional}.ec.
The headline "strict-atom byte-equality" theorem was `apply <axiom that
restates the theorem>`; the Lean side was `sorry`/`:= True`.
- Re-open MAGNETAR-STRICT-ATOM (BLOCKERS): the public combiner DOES
reconstruct the full FIPS 205 master every signature; the v1.1 "closure"
only renamed identifiers. PROOF-CLAIMS / AXIOM-INVENTORY / TCB docs now say
what the code does.
- Re-label the name-grep "strict-atom" / "CT" checks as identifier-hygiene
lint, NOT security or constant-time properties.
- PVSS-DKG open-reveal (publishes the master to any observer) is gated as a
TEST-ONLY path with HONEST LIMITATIONS; production does not rely on it.
- Remove dead htRootCompute; staticcheck clean.
Honest three-leg posture (SPEC 1.0, BLOCKERS):
- Permissionless production = INDEPENDENT FIPS 205 sigs + the weighted quorum
certificate (luxfi/consensus), optionally STARK/FRI-compressed (luxfi/p3q).
No key sharing, no reconstruction.
- Trusted-hardware custody = TEE-attested combiner (trust-relocation, NOT MPC).
- THBS-SE = RESEARCH-ONLY (transient seed reconstruction at the combiner);
the T-SLH-DSA-MPC track (MPC over SHAKE) is the other research escape hatch.
Tests green (CGO=1, 71s). Net -923 lines.
1.3 KiB
Magnetar EasyCrypt track (HONEST: empty)
This directory contains no mechanized EasyCrypt proof. It holds two SCAFFOLD files only:
| File | Content |
|---|---|
Magnetar_N1_StrictAtom.ec |
0-content scaffold. Records that THBS-SE Combine byte-equality is NOT proven; explains the prior circular "proof". |
Magnetar_N5_PVSS_DKG.ec |
0-content scaffold. Records that PVSS-DKG secrecy is NOT proven, and that the prior secrecy "theorem" was vacuous AND false for the open-reveal code it modeled. |
Neither file declares an axiom, admit, lemma, or theorem.
Why the rest was deleted
The earlier EC track (Magnetar_N1_SHAKE_Expand.ec,
Magnetar_N1_Atom_Refinement.ec, Magnetar_N4_KeyDeriveStable.ec,
lemmas/SLHDSA_Functional.ec, lemmas/Magnetar_CT.ec) advertised a
small "admit budget" (5--6 admits) over a set of theorems that proved
nothing: X = X rewrites, conclusion = true discharged by
trivial, a CT lemma discharged by admit, and a headline
byte-equality theorem discharged by apply-ing an axiom that restated
it verbatim. A nonzero theorem count with a tidy admit budget is not
evidence when the theorems are vacuous. The files were removed rather
than left to imply a proof track exists.
See ../README.md (proof-track overview) and ../../PROOF-CLAIMS.md
(per-property breakdown).