These are the underlying hardness + soundness assumptions of the
Magnetar construction. They are NOT closing in any Lux work —
they are the substrate of the security argument and are inherited
from NIST standards and the academic literature.
| Axiom | Reference | Rationale for non-closure |
|---|---|---|
| **FIPS 205 SLH-DSA security (EUF-CMA)** | NIST FIPS 205 (Stateless Hash-Based Digital Signature Standard, 2024); Bernstein et al. SPHINCS+ submission to NIST PQC | Standard NIST analysis. The single-party signing primitive's unforgeability under chosen-message attack is FIPS 205's security goal; Magnetar inherits it via the `cloudflare/circl/sign/slhdsa` dispatch. Not a Magnetar-specific assumption. |
| **SHAKE256 / cSHAKE256 collision + preimage resistance** | NIST FIPS 202 + SP 800-185 | Used in `transcript.go` for domain-separated hashing across DKG, signing, mix-to-seed. Hash function security is standard NIST assumption. Magnetar's threshold-overlay binding arguments (transcript digest equivocation detection, commit-bind reveal, mix-to-seed) reduce to SHAKE256 collision/preimage resistance. |
| **KMAC256 unforgeability** | NIST SP 800-185 | Reserved for v0.4 envelope-authentication tag (matching Pulsar's `PULSAR-DKG-ENVAUTH-V1` pattern). Not in use at v0.1 (envelopes are plaintext); will be load-bearing once v0.4 ML-KEM wrapping lands. |
| **Byte-wise Shamir VSS soundness over GF(257)** | Shamir 1979 (information-theoretic secret sharing); standard textbook result | The classical Shamir construction is information-theoretically secure: any `t-1` shares reveal zero information about the secret. Magnetar applies the construction byte-by-byte to the SLH-DSA scheme seed; the per-byte independence + GF(257) choice (smallest prime > 255) preserve this property. The Lagrange reconstruction at `x=0` is standard. (No Magnetar EC/Lean mechanization of this exists; the prior "cross-cite Pulsar's bridge once our EC shells land" plan is withdrawn — those shells were vacuous and deleted.) |
| **Identity-key signature unforgeability** | Application-level assumption (consensus layer identity keys; for v0.4 envelope-authenticated DKG, this maps to FIPS 204 ML-DSA-65 or equivalent) | Reserved for v0.4 identifiable-abort evidence-signing pattern. At v0.1 the `AbortEvidence.Signature` field is provisioned but not yet wired (the v0.1 reveal-and-aggregate trust model places the aggregator in TCB, so identifiable-abort attribution at the DKG level via digest pairs is sufficient for v0.1; v0.4 will sign evidence under identity keys for slashing). |
| **Domain-separation soundness of cSHAKE customisation strings** | NIST SP 800-185 §3 | Each Magnetar transcript hash uses a distinct customisation string (`MAGNETAR-DKG-COMMIT-V1`, `MAGNETAR-DKG-TRANSCRIPT-V1`, `MAGNETAR-SIGN-R1-V1`, `MAGNETAR-SIGN-MASK-V1`, `MAGNETAR-SEED-SHARE-V1`) plus function-name `"Magnetar"`. SP 800-185 guarantees no collision across distinct (N, S) tuples for the cSHAKE construction. Standard NIST assumption. |
## §2 Implementation-level axioms (TCB)
These are residual gaps between the FIPS-anchored single-party
primitive + the construction-level argument and the shipped Go
| `cloudflare/circl/sign/slhdsa` correctness vs FIPS 205 | indirect via `keygen.go`, `sign.go`, `verify.go`, `slhdsa_internal.go` | Trust the library; community-audited. Cross-implementation check against a non-Go FIPS 205 reference (BoringSSL / pq-crystals) is a tracked gap (OPEN). |
| `golang.org/x/crypto/sha3` cSHAKE256 / KMAC256 correctness vs FIPS 202 / SP 800-185 | indirect via `transcript.go` | Trust the standard library. KAT-determinism (`ref/go/cmd/genkat`) enforces byte-stability. |
| Implementation matches the construction at the protocol level | `thbsse.go`, `pvss_dkg.go`, `thbsse_assemble.go`, `slhdsa_internal.go` | **OPEN, no mechanization.** Evidence is code review + tests only. The prior "EC theory shells at v0.5.0" closure plan was vacuous and is withdrawn. |
| THBS-SE Combine output byte-equals single-party FIPS 205 SignDeterministic on the reconstructed master | `thbsse_assemble.go`; tests `TestSlhdsaInternal_ByteEqualToCirclSign`, `TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl` | ASSERTED by test (correctness/interop). NOT mechanized. NOT a no-leak property — the master IS reconstructed (`ASSEMBLE-INVARIANT.md`). |
| Constant-time of the threshold overlay | `transcript.go` (`ctEqualSlice`, `ctEqual32`) + code review | **OPEN.** No dudect harness. The "CT" AST test is a name lint, not a timing measurement, and CT is moot for a path holding the master in plaintext. |
| PVSS-DKG production transcript hides the master | `pvss_dkg.go` (`RunDKG`); test `TestPVSS_DKG_ProductionTranscriptHidesMaster` | ASSERTED by test. The secrecy reduction to byte-wise Shamir over GF(257) is standard but NOT machine-checked. pk derivation still reconstructs M (inherent). |
| Secret-buffer zeroization | `thbsse_assemble.go`, `pvss_dkg.go`, `zeroize.go` | Defense-in-depth, not a guarantee (GC may copy). In the permissionless THBS-SE path the master IS resident during one Sign call; this is research-grade, not no-leak (`BLOCKERS.md`). |
