mirror of
https://github.com/luxfi/magnetar.git
synced 2026-09-24 00:25:23 +00:00
zooqueen
135f43e531
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.
66 lines
4.8 KiB
Plaintext
66 lines
4.8 KiB
Plaintext
(* -------------------------------------------------------------------- *)
|
|
(* Magnetar --- THBS-SE Combine byte-equality *)
|
|
(* SCAFFOLD: 0 mechanized content. This file proves NOTHING. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* *)
|
|
(* HONEST STATUS *)
|
|
(* ============ *)
|
|
(* *)
|
|
(* This file is a SCAFFOLD. It does not contain a mechanized proof of *)
|
|
(* anything. Read this banner before reading any line below it. *)
|
|
(* *)
|
|
(* The earlier revision of this file claimed a headline theorem *)
|
|
(* *)
|
|
(* magnetar_n1_strict_atom_byte_equality *)
|
|
(* *)
|
|
(* whose entire "proof" was `apply combine_assemble_axiom`, where *)
|
|
(* `combine_assemble_axiom` RESTATED THE CONCLUSION VERBATIM. That is *)
|
|
(* a circular non-proof: the axiom and the theorem were byte-identical *)
|
|
(* statements. Asserting a theorem as an axiom and then "applying" the *)
|
|
(* axiom proves nothing. It has been removed. *)
|
|
(* *)
|
|
(* WHAT IS ACTUALLY TRUE ABOUT THE CODE THIS FILE WAS MEANT TO MODEL *)
|
|
(* ------------------------------------------------------------------ *)
|
|
(* *)
|
|
(* - `thbsse_assemble.go::assembleSignatureBytes` reconstructs the *)
|
|
(* FIPS 205 master byte-by-byte via Lagrange interpolation into a *)
|
|
(* buffer (`derivedExpandInput`), SHAKE-expands it into a single *)
|
|
(* buffer (`derivedMaterial` = skSeed || skPrf || pkSeed), and *)
|
|
(* drives a FIPS 205 sec 5--sec 8 walk that reads positional slices *)
|
|
(* of that buffer. The full FIPS 205 master is therefore present in *)
|
|
(* the public combiner's process memory for the duration of one *)
|
|
(* Sign call. The "strict-atom" renaming of the buffer (avoiding *)
|
|
(* the identifier `seed`) does NOT change this fact: it is the same *)
|
|
(* seed reconstruction as the v1.0 path, with a different variable *)
|
|
(* name. There is NO no-leak property here to mechanize. *)
|
|
(* *)
|
|
(* - The ONLY property with empirical support is byte-IDENTITY of the *)
|
|
(* emitted signature to `circl/slhdsa.SignDeterministic` on the *)
|
|
(* reconstructed master. That support is the Go test *)
|
|
(* `TestSlhdsaInternal_ByteEqualToCirclSign` (per SHAKE mode) plus *)
|
|
(* `TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`. It is a *)
|
|
(* correctness/interop property (the threshold output is a valid *)
|
|
(* FIPS 205 signature), NOT a confidentiality property. *)
|
|
(* *)
|
|
(* WHAT A REAL PROOF WOULD REQUIRE (NOT DONE) *)
|
|
(* ----------------------------------------- *)
|
|
(* *)
|
|
(* A genuine mechanized byte-equality result would need an EasyCrypt *)
|
|
(* port of the FIPS 205 sec 5 (WOTS+), sec 6 (XMSS), sec 7 (hypertree), *)
|
|
(* and sec 8 (FORS) byte walks, proven equal to an independent abstract *)
|
|
(* `slh_sign` model (not to circl, and not to a restatement of the *)
|
|
(* conclusion). That is a multi-week effort and is NOT attempted here. *)
|
|
(* It is tracked as OPEN in PROOF-CLAIMS.md. *)
|
|
(* *)
|
|
(* The supporting refinement files in this directory *)
|
|
(* (`Magnetar_N1_SHAKE_Expand.ec`, `Magnetar_N1_Atom_Refinement.ec`) *)
|
|
(* are ALSO scaffolds: their "lemmas" are either `X = X` rewrites or *)
|
|
(* `apply axiom` against axioms that restate the goal. See each file's *)
|
|
(* banner. *)
|
|
(* *)
|
|
(* This file intentionally contains NO `theorem`, NO `lemma`, and NO *)
|
|
(* `axiom`. It is prose-as-EasyCrypt-comment so that the directory's *)
|
|
(* axiom/admit count for this file is exactly ZERO and cannot be *)
|
|
(* mistaken for discharged content. *)
|
|
(* -------------------------------------------------------------------- *)
|