mirror of
https://github.com/luxfi/magnetar.git
synced 2026-07-27 02:53:47 +00:00
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.
111 lines
6.6 KiB
Markdown
111 lines
6.6 KiB
Markdown
# PROOF-CLAIMS --- Magnetar (HONEST: proven vs asserted vs open)
|
|
|
|
This document states, per property, exactly what is PROVEN (mechanized),
|
|
what is ASSERTED (tested / by-construction / inherited from a standard),
|
|
and what is OPEN. Read it before reading the code.
|
|
|
|
## §0 One-paragraph truth
|
|
|
|
Magnetar has **no mechanized proof of any threshold property**. The
|
|
per-validator standalone primitive is a thin, sound wrapper over
|
|
`cloudflare/circl/sign/slhdsa` FIPS 205. The permissionless THBS-SE
|
|
threshold path reconstructs the FIPS 205 master at the public combiner
|
|
(research-grade; not no-leak). The dealerless PVSS-DKG production path
|
|
hides the master from transcript observers but still reconstructs it to
|
|
derive the group public key. The EasyCrypt/Lean "proof track" was
|
|
vacuous and has been deleted or reduced to labeled scaffolds. Evidence
|
|
is empirical (tests + KAT determinism + FIPS 205 verifier dispatch),
|
|
not machine-checked.
|
|
|
|
## §1 Per-property status
|
|
|
|
| Property | Status | Basis |
|
|
|---|---|---|
|
|
| Per-validator standalone emits valid single-party FIPS 205 signatures | ASSERTED (by dispatch + test) | `standalone.go` calls `circl/slhdsa`; `TestMagnetar_Wire_FIPS205Verifiable` across 3 SHAKE modes. Inherits FIPS 205 (NIST 2024) security analysis for the single-party layer. |
|
|
| THBS-SE Combine output is byte-identical to `circl/slhdsa.SignDeterministic` on the reconstructed master (valid FIPS 205 signature) | ASSERTED (by test) | `TestSlhdsaInternal_ByteEqualToCirclSign`, `TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`. This is a CORRECTNESS/INTEROP property. NOT mechanized. |
|
|
| THBS-SE Combine is no-leak (master not reconstructed) | **FALSE / OPEN** | The path DOES reconstruct the master at the public combiner (`ASSEMBLE-INVARIANT.md`). There is no no-leak property to prove. RESEARCH-ONLY. |
|
|
| PVSS-DKG production transcript hides the master from observers | ASSERTED (by test) | `RunDKG` emits no constant-term reveals; `TestPVSS_DKG_ProductionTranscriptHidesMaster`. NOT mechanized (the secrecy reduction to byte-wise Shamir over GF(257) is a standard result but is not machine-checked here). |
|
|
| PVSS-DKG: no party EVER holds the master | **FALSE** | `deriveDKGPublicKey` reconstructs M to compute `pk = SLH-DSA.PK(M)` (inherent; see `BLOCKERS.md`). True only on the TEE / dealer paths. |
|
|
| PVSS-DKG robust against malicious dealers (production path) | **NOT DELIVERED** | Hash commitments aren't openable without revealing m_i; production defers malformed-share detection to sign-time commit binding. Robustness holds only on the open-reveal (test) path. |
|
|
| Threshold overlay mechanized refinement (EasyCrypt / Lean / Jasmin) | **NONE** | The prior track was vacuous; deleted/scaffolded. See §2. |
|
|
| Constant-time of the threshold overlay (statistical / dudect) | OPEN | Only local CT helpers + code review. No dudect harness. The "CT" AST test is a name lint, not a timing measurement. |
|
|
| Post-quantum hardness of SLH-DSA | INHERITED | FIPS 205 (NIST 2024); collision/preimage resistance of SHAKE. Nothing Magnetar-specific. |
|
|
|
|
## §2 The deleted/scaffolded "proof track" (HONEST accounting)
|
|
|
|
The earlier submission advertised a mechanized EasyCrypt + Lean track
|
|
with a small "admit budget". Every result in it was vacuous:
|
|
|
|
- `Magnetar_N1_StrictAtom.ec` --- headline theorem
|
|
`magnetar_n1_strict_atom_byte_equality` proved by `apply
|
|
combine_assemble_axiom`, where that axiom RESTATED THE THEOREM
|
|
verbatim. Circular. Plus `strict_atom_discipline_satisfied : bool =
|
|
true`. **Reduced to a 0-content scaffold.**
|
|
- `proofs/lean/.../StrictAtom.lean` --- theorem body `sorry`;
|
|
`strictAtomDisciplineSatisfied : Prop := True`. **Reduced to a
|
|
0-content scaffold.**
|
|
- `Magnetar_N5_PVSS_DKG.ec` --- "secrecy theorem" with conclusion
|
|
`... true` proved by `trivial`; wire-compat `X = X`; composition
|
|
`true`. Doubly false because it claimed secrecy for the open-reveal
|
|
code that PUBLISHES the secret. **Reduced to a 0-content scaffold.**
|
|
- `Magnetar_N1_SHAKE_Expand.ec` --- only non-axiom lemma was
|
|
`shake_expand s = shake_expand s` from `s = s`. **DELETED.**
|
|
- `Magnetar_N1_Atom_Refinement.ec` --- a single restate-as-axiom.
|
|
**DELETED.**
|
|
- `Magnetar_N4_KeyDeriveStable.ec` --- `s = s' => f s = f s'` ("this
|
|
function is a function"). **DELETED.**
|
|
- `lemmas/Magnetar_CT.ec` --- `strict_atom_combine_is_ct` discharged by
|
|
`admit`; comment admitted "abstract level vacuous". CT is also the
|
|
wrong property (the master is in plaintext in the buffer). **DELETED.**
|
|
- `lemmas/SLHDSA_Functional.ec` --- legitimate black-box FIPS 205
|
|
functional axioms, but fed only the deleted files. **DELETED.**
|
|
|
|
The remaining `.ec`/`.lean` files declare no `axiom`, `admit`, `lemma`,
|
|
`theorem`, or `sorry` — they are prose scaffolds recording that the
|
|
properties are NOT proven. See `proofs/README.md`.
|
|
|
|
## §3 What the trust base reduces to (no mechanization)
|
|
|
|
For correctness/interop:
|
|
|
|
- FIPS 205 SLH-DSA standard (NIST 2024).
|
|
- `cloudflare/circl/sign/slhdsa` reference (community-audited).
|
|
- Go reference review of the threshold overlay.
|
|
- KAT determinism (`ref/go/cmd/genkat`).
|
|
- `TestSlhdsaInternal_ByteEqualToCirclSign` /
|
|
`TestMagnetar_Wire_FIPS205Verifiable` /
|
|
`TestThbsSE_Wire_FIPS205Verifiable`.
|
|
|
|
For confidentiality: the ONLY sound posture is the per-validator
|
|
standalone path (no reconstruction). The THBS-SE permissionless path is
|
|
research-grade; the TEE pool relocates trust into attested hardware.
|
|
|
|
## §4 What an auditor should do
|
|
|
|
1. Read this file and `BLOCKERS.md`.
|
|
2. Read `ASSEMBLE-INVARIANT.md` (what THBS-SE Combine does).
|
|
3. `cd ref/go && GOWORK=off go build ./...` (clean).
|
|
4. `GOWORK=off go test -count=1 -short ./pkg/magnetar/` (green),
|
|
including `TestPVSS_DKG_ProductionTranscriptHidesMaster`.
|
|
5. Regenerate KATs and diff (determinism):
|
|
`GOWORK=off go run ./ref/go/cmd/genkat -out=vectors/`,
|
|
`diff -qr vectors_backup/ vectors/`.
|
|
6. Read the Go reference: `params.go`, `types.go`, `keygen.go`,
|
|
`sign.go`, `verify.go`, `thbsse.go`, `thbsse_field.go`,
|
|
`thbsse_assemble.go`, `slhdsa_internal.go`, `standalone.go`,
|
|
`pvss_dkg.go`, `key.go`, `zeroize.go`. (NOTE: the v0.x files
|
|
`shamir.go`, `dkg.go`, `threshold.go`, `combine.go` were DELETED;
|
|
any doc still referencing them is stale.)
|
|
7. Cross-reference FIPS 205 (NIST 2024) §5--§11 and §10.
|
|
|
|
## §5 Open items (tracked)
|
|
|
|
| Item | Status |
|
|
|---|---|
|
|
| Mechanized refinement of the threshold overlay | OPEN (multi-week; prior track was vacuous, now deleted) |
|
|
| No-leak THBS-SE (full MPC over SHAKE) | OPEN RESEARCH |
|
|
| Robust dealerless DKG (group-homomorphic or PVSS+NIZK commitments) | OPEN (separate construction) |
|
|
| dudect statistical CT harness | OPEN |
|
|
| External cryptographer audit | OPEN |
|
|
| Cross-implementation FIPS 205 byte-equality (non-circl) | OPEN |
|