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.
Magnetar v1.1 dudect track --- strict-atom Combine path
The v1.1 dudect track measures the constant-time discipline of the
Magnetar strict-atom Combine path
(ref/go/pkg/magnetar/thbsse_assemble.go +
ref/go/pkg/magnetar/slhdsa_internal.go).
What this directory contains
| File | Role |
|---|---|
strict_atom_combine_ct.go |
Go-side CT static-analysis harness: pattern-checks the strict-atom Go source for secret-dependent branches and secret-dependent memory accesses. Run via go test -tags ct. |
combine_ct |
Legacy v1.0 dudect binary (kept for archival reference; the v1.0 dudect harness modelled the abandoned seed-recombine Combine path). |
dudect_strict_atom_overview.md |
Methodology + threat model for the strict-atom CT track. |
v1.0 -> v1.1 delta
The v1.0 dudect harness measured circl/sign/slhdsa.SignDeterministic
indirectly via the seed-reconstruction Combine path. v1.1 measures the
Magnetar-internal FIPS 205 sec 5/6/7/8 walk DIRECTLY, since the
strict-atom path is the FIPS 205 byte emitter at v1.1 (the call to
circl is bypassed).
Per-push gate
scripts/checks/dudect-smoke.sh runs the Go-side pattern check
(TestStrictAtom_CT_NoSecretDependentBranch). This is fast (<5s) and
catches the obvious classes of CT violation:
- Secret-tagged byte fed into a control-flow branch.
- Secret-tagged byte used as an array/slice index.
- Secret-tagged byte fed into a map lookup.
The Go static checker is necessary but not sufficient; the full dudect statistical test on a compiled C harness (or Go-via-cgo harness) is a release-time gate.
Methodology summary
The strict-atom Combine path's CT obligation is BGL leakage-free under the model:
- The Lagrange basis depends only on PUBLIC evaluation points.
- The per-byte Lagrange sum is straight-line modular arithmetic.
- The SHAKE-256 expansion is constant-time per FIPS 202.
- The PRF / PRF_msg absorb buffers are constructed by positional append; no branch on secret bytes.
- The Magnetar-internal FIPS 205 walk branches only on PUBLIC values (FORS index bits derived from message digest; WOTS+ chain step counts; XMSS layer index).
The Go-side harness asserts items 4 + 5 by static AST inspection of
thbsse_assemble.go + slhdsa_internal.go. The C-side harness (release
gate, not run per-push) asserts items 1 + 2 + 3 by timing distinguishing
attack: fix the public projection of two distinct secret seeds, drive
Combine end-to-end on both, and assert the two execution traces are
indistinguishable above a configurable t-statistic threshold.