mirror of
https://github.com/luxfi/magnetar.git
synced 2026-07-27 02:53:47 +00:00
submission: TRUSTED-COMPUTING-BASE + PROOF-CLAIMS + AXIOM-INVENTORY + FIPS-TRACEABILITY
Tier A documentation shape, second cluster. Honest framing of what Magnetar v0.3.0 proves vs what remains roadmap: - TRUSTED-COMPUTING-BASE.md: enumerates the trust base. cloudflare/circl slhdsa is in TCB at the single-party FIPS 205 layer. Aggregator process is in TCB for the brief seed-reconstruction window (v0.1 reveal-and-aggregate caveat). Comparison table vs Pulsar and Corona TCBs. - PROOF-CLAIMS.md: narrow Class-N1 byte-equality claim — Magnetar threshold output is byte-identical to single-party FIPS 205 slhdsa.SignDeterministic on the reconstructed seed. §3 enumerates 7 explicit NON-claims: mechanized refinement of threshold overlay, post-quantum hardness beyond FIPS 205, byte-equality with FIPS 204/R-LWE, dudect statistical CT, covert channels, protocol-level adversarial robustness beyond reveal-and-aggregate, external Lean theorems. - AXIOM-INVENTORY.md: construction-level + implementation-level axioms. FIPS 205 SLH-DSA security inherited from NIST. Byte-wise Shamir VSS soundness over GF(257) inherited from Shamir 1979. Closure plans for EC theory shells (v0.5.0 roadmap), Lean ↔ EC bridge cross-citation to Pulsar's GF(257) bridges, dudect (v0.6.0). - FIPS-TRACEABILITY.md: FIPS 205 §10.1/10.2/10.3 → keygen/sign/ verify code map. FIPS 202 + SP 800-185 cSHAKE256/KMAC256 customisation tags pinned in transcript.go. Threshold overlay layer traces to SPEC.md §3/§4/§6 (no NIST standard exists for threshold SLH-DSA). NO fake closure language. Every "OPEN" gate is explicit; every closure plan is concrete and dated to a roadmap version.
This commit is contained in:
Hanzo AI
@@ -0,0 +1,129 @@
|
||||
# AXIOM-INVENTORY — Magnetar
|
||||
|
||||
> Honest enumeration of every cryptographic assumption + residual
|
||||
> axiom Magnetar depends on. This document is load-bearing for the
|
||||
> Tier A submission gate: per the project rubric, AXIOM-INVENTORY
|
||||
> MUST be reviewable by an external cryptographer and MUST close
|
||||
> every residual axiom with either a closure plan or an explicit
|
||||
> non-closure rationale.
|
||||
>
|
||||
> Status at v0.3.0: **EC theory artifacts for the threshold overlay
|
||||
> are roadmap**; this document enumerates the construction-level +
|
||||
> implementation-level axioms against which the eventual proofs will
|
||||
> be discharged. The single-party FIPS 205 SLH-DSA layer is NIST-
|
||||
> anchored (FIPS 205, 2024) and inherits NIST's security analysis.
|
||||
|
||||
## §1 Construction-level axioms (cryptographic assumptions)
|
||||
|
||||
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 algebraically identical to Pulsar's GF(257) variant — Pulsar's Lean ↔ EC bridge files cover the algebraic identity and Magnetar can cross-cite them once its EC theory shells land. |
|
||||
| **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
|
||||
implementation. Each has a closure plan.
|
||||
|
||||
| Axiom | Location | Closure plan |
|
||||
|---|---|---|
|
||||
| `cloudflare/circl/sign/slhdsa` correctness vs FIPS 205 | indirect via `keygen.go`, `sign.go`, `verify.go`, `combine.go` | Trust the library; upstream is community-audited Cloudflare reference. Cross-implementation check against a non-Go FIPS 205 implementation (BoringSSL when SLH-DSA matures, or pq-crystals reference C) is roadmap item; see `BLOCKERS.md` BLK-6. |
|
||||
| `golang.org/x/crypto/sha3` cSHAKE256 / KMAC256 correctness vs FIPS 202 / SP 800-185 | indirect via `transcript.go` | Trust the standard-library implementation; widely deployed and quickly patched. KAT-determinism (`ref/go/cmd/genkat`) enforces byte-stability across runs. |
|
||||
| Implementation matches the Magnetar SPEC.md construction at the protocol level | `ref/go/pkg/magnetar/{shamir,dkg,threshold,combine,transcript,zeroize}.go` | **OPEN — gated by EC theory shells.** Roadmap v0.5.0: implement EC theories `Magnetar_N1_Refinement.ec`, `Magnetar_N1_Combine_Refinement.ec`, `Magnetar_DKG_Refinement.ec`. Pulsar got to admit 0/0 over 13 EC iterations; Magnetar will follow the same closure path, with the advantage that the Shamir / Lagrange algebraic identities are identical to Pulsar's (cross-citation to Pulsar's Lean bridges is the closure plan). |
|
||||
| Threshold-Combine output byte-equals single-party FIPS 205 SignDeterministic on reconstructed seed (Class N1 byte-equality) | `combine.go` end-to-end; empirically `n1_byte_equality_test.go` | **OPEN — empirical-only at v0.3.0.** Closure: the byte-equality refinement theorem extracted from the EC theory shells (v0.5.0) would mechanize the property. Until then the evidence is `TestN1_ByteEquality_*` (3 configs) + KAT determinism + the FIPS 205 verifier dispatch. |
|
||||
| Constant-time execution of the threshold overlay (commit verify, pubkey equality, share equality) | `transcript.go` (`ctEqualSlice`, `ctEqual32`), `combine.go`, `keygen.go` | **OPEN.** No `dudect` harness yet for the threshold overlay. Roadmap v0.6.0. Single-party FIPS 205 CT inherits `cloudflare/circl` upstream claims; libjade's SLH-DSA formal CT artifacts are available upstream but not redistributed in this submission. |
|
||||
| Identifiable-abort attribution via DKG Round-3 digest mismatch | `dkg.go` Round3 | Soundness reduces to cSHAKE256 collision resistance (binding the transcript digest) plus identity-key signature unforgeability (when v0.4 signs the evidence). Documented in `SPEC.md` §8 and tested in `dkg_test.go`. Formal proof: roadmap v0.5.0. |
|
||||
| Secret-buffer zeroization on every Combine return path | `combine.go` (every error and success exit), `zeroize.go` | Go's GC may copy buffers around; zeroize is defense-in-depth, not a guarantee. The v0.1 reveal-and-aggregate trust caveat (master seed reconstructed in aggregator memory for ~100ms during Combine) is documented in `DEPLOYMENT-RUNBOOK.md` with the TEE / mlock / ptrace-off hardening matrix. Closure: v0.2 full-MPC construction would eliminate the brief seed-exposure window; research, no committed target. |
|
||||
| Network-observer envelope confidentiality | v0.1: NONE (envelopes are plaintext); v0.4: ML-KEM-768 wrapping under recipient identity key | **OPEN — v0.4 closure plan.** v0.4 wraps each Round-1 envelope as `KEMCiphertext || Sealed` matching Pulsar's `sealEnvelope` pattern (`identity.go:399` in pulsar). See `BLOCKERS.md` BLK-4. |
|
||||
|
||||
## §3 Comparison to Pulsar's AXIOM-INVENTORY
|
||||
|
||||
Pulsar's `~/work/lux/pulsar/AXIOM-INVENTORY.md` enumerates ~36
|
||||
residual EC axioms remaining after the v4-v13 decomposition cascade
|
||||
(see Pulsar's "Trust footprint summary (after v8)" table for the
|
||||
category breakdown). Magnetar v0.3.0 has **zero** EC artifacts for
|
||||
the threshold overlay; the comparable axiom inventory for Magnetar
|
||||
is the **roadmap target** of v0.5.0+.
|
||||
|
||||
Magnetar is structurally easier than Pulsar in one respect: there
|
||||
is no rejection-sampling kappa-loop reasoning. FIPS 205 SLH-DSA
|
||||
signing is deterministic in the `SignDeterministic` mode (no
|
||||
rejection-restart on the hot path; the WOTS+/FORS hash-tree
|
||||
construction is straight-line). Pulsar's hot path includes the
|
||||
ML-DSA rejection-sampling-loop kappa reasoning (an `accept_signing_attempt`
|
||||
predicate plus per-kappa loop unrolling). Magnetar's Class-N1-analog
|
||||
byte-equality is a strictly narrower refinement than Pulsar's:
|
||||
"threshold output equals single-party deterministic FIPS 205 output
|
||||
on the reconstructed seed" with no per-attempt kappa branching.
|
||||
|
||||
Magnetar is structurally harder than Corona in one respect: Corona
|
||||
has no FIPS standard target, so its byte-equality claim is
|
||||
"construction-level interchangeability" with its own verifier.
|
||||
Magnetar's claim is strictly stronger: byte-equality with a NIST
|
||||
standard primitive (FIPS 205) such that any FIPS 205-conformant
|
||||
verifier accepts threshold output with no code change.
|
||||
|
||||
## §4 Honest non-claim
|
||||
|
||||
This document is the **inventory** of axioms Magnetar's proofs
|
||||
WILL discharge. It is NOT a claim that Magnetar's proofs are
|
||||
CLOSED. EC theories for the threshold overlay are explicitly
|
||||
roadmap (see `PROOF-CLAIMS.md` §3 non-claims + this file's §2
|
||||
closure plans).
|
||||
|
||||
At v0.3.0, Magnetar's proof basis is:
|
||||
|
||||
1. FIPS 205 SLH-DSA NIST security analysis (single-party layer).
|
||||
2. Construction soundness inherited from byte-wise Shamir VSS
|
||||
over GF(257) + the classical Lagrange reconstruction identity.
|
||||
3. KAT-determinism (`ref/go/cmd/genkat` is reproducible).
|
||||
4. `TestN1_ByteEquality_*` empirical byte-equality across
|
||||
(committee, threshold) configurations (3,2), (5,3), (7,4).
|
||||
5. Cross-validation: `verify.go` dispatches to
|
||||
`cloudflare/circl/sign/slhdsa.Verify` (the FIPS 205 §10.3
|
||||
verifier verbatim); any FIPS 205-conformant verifier accepts
|
||||
Magnetar threshold output.
|
||||
6. Code review: secret-dependent branches identified and replaced
|
||||
with constant-time helpers (`ctEqualSlice`, `ctEqual32`).
|
||||
7. Test-suite coverage (`go test -count=1 ./ref/go/pkg/magnetar/`
|
||||
green; race-mode skip via `raceEnabled` build-tag pattern for
|
||||
SLH-DSA-heavy tests that exceed race-detector overhead).
|
||||
|
||||
EC mechanization for the threshold overlay is the load-bearing
|
||||
gap between Tier A documentation shape (achieved v0.3.0) and the
|
||||
full Tier A cut-readiness Pulsar v1.0.7 holds (admit 0/0 across
|
||||
13 EC files).
|
||||
|
||||
## §5 Cross-references
|
||||
|
||||
- `SUBMISSION.md` — submission cover sheet
|
||||
- `PROOF-CLAIMS.md` — narrow claim + explicit non-claims
|
||||
- `TRUSTED-COMPUTING-BASE.md` — TCB inventory
|
||||
- `FIPS-TRACEABILITY.md` — FIPS 205 § → code traceability
|
||||
- `DEPLOYMENT-RUNBOOK.md` — operator trust-model disclosure (v0.1
|
||||
reveal-and-aggregate aggregator-as-TCB)
|
||||
- `CRYPTOGRAPHER-SIGN-OFF.md` — independent review verdict
|
||||
- `BLOCKERS.md` — Tier B → A path; gates blocking full Tier A
|
||||
- Roadmap target for EC theory shells: v0.5.0 (see `NIST-SUBMISSION.md`
|
||||
§"Roadmap")
|
||||
- Sibling AXIOM-INVENTORY (Pulsar): `~/work/lux/pulsar/AXIOM-INVENTORY.md`
|
||||
— Tier A reference with admit 0/0 closure; Magnetar's eventual
|
||||
closure plan mirrors this pattern.
|
||||
|
||||
---
|
||||
|
||||
**Document metadata**
|
||||
|
||||
- Name: `AXIOM-INVENTORY.md`
|
||||
- Version: v0.1 (initial Tier A submission-package scaffolding)
|
||||
- Date: 2026-05-18
|
||||
@@ -0,0 +1,202 @@
|
||||
# FIPS-TRACEABILITY — Magnetar
|
||||
|
||||
> **FIPS 205 § → Magnetar code map.** Magnetar IS FIPS-anchored
|
||||
> at the single-party layer. This document maps the NIST FIPS 205
|
||||
> (Stateless Hash-Based Digital Signature Standard, 2024) sections
|
||||
> to the corresponding code paths in `~/work/lux/magnetar/ref/go/`.
|
||||
> The threshold-overlay layer is documented as a Magnetar-specific
|
||||
> overlay traceable to `SPEC.md` sections, not FIPS 205 (no NIST
|
||||
> standard exists for threshold SLH-DSA at submission time).
|
||||
>
|
||||
> Equivalent role to Pulsar's `FIPS-TRACEABILITY.md` (which maps
|
||||
> FIPS 204 § → code) and Corona's (which maps Boschini ePrint
|
||||
> 2024/1113 § → code).
|
||||
|
||||
## §1 Reference
|
||||
|
||||
- **NIST FIPS 205** — *Stateless Hash-Based Digital Signature
|
||||
Standard* (Federal Information Processing Standards Publication
|
||||
205, U.S. Department of Commerce / NIST, August 2024).
|
||||
- **NIST FIPS 202** — *SHA-3 Standard: Permutation-Based Hash and
|
||||
Extendable-Output Functions* (August 2015).
|
||||
- **NIST SP 800-185** — *SHA-3 Derived Functions: cSHAKE, KMAC,
|
||||
TupleHash, and ParallelHash* (December 2016).
|
||||
|
||||
FIPS 205 is the construction-level normative reference for
|
||||
Magnetar's **single-party layer**. The Magnetar threshold overlay
|
||||
(byte-wise Shamir VSS, DKG, two-round commit-bind sign, Combine)
|
||||
is novel work documented in `SPEC.md`; it traces to Shamir 1979 +
|
||||
the classical Lagrange reconstruction identity, not FIPS 205.
|
||||
|
||||
## §2 FIPS 205 section → Magnetar code mapping
|
||||
|
||||
### §2.1 Parameter sets (FIPS 205 §10.1 Table 2)
|
||||
|
||||
Magnetar ships the SHAKE-family small and fast parameter sets at
|
||||
NIST PQ Category 3 (≥192-bit security) and Category 5 (≥256-bit).
|
||||
The SHA-2 family is excluded because Magnetar's transcript-hash
|
||||
suite is uniformly FIPS 202 SHA-3 / SHAKE.
|
||||
|
||||
| FIPS 205 § | Parameter set | Magnetar Mode | Code | Wire sizes |
|
||||
|---|---|---|---|---|
|
||||
| §10.1 Table 2 | SLH-DSA-SHAKE-192s | `ModeM192s` (recommended) | `params.go:124` (`ParamsM192s`) | pk=48 B, sk=96 B, sig=16224 B, seed=96 B |
|
||||
| §10.1 Table 2 | SLH-DSA-SHAKE-192f | `ModeM192f` | `params.go:136` (`ParamsM192f`) | pk=48 B, sk=96 B, sig=35664 B, seed=96 B |
|
||||
| §10.1 Table 2 | SLH-DSA-SHAKE-256s | `ModeM256s` | `params.go:148` (`ParamsM256s`) | pk=64 B, sk=128 B, sig=29792 B, seed=128 B |
|
||||
|
||||
The byte sizes are pinned in `params.go` and validated against the
|
||||
canonical FIPS 205 sizes via `Params.Validate()`; mismatches return
|
||||
`ErrParamsTampered`.
|
||||
|
||||
### §2.2 Key generation (FIPS 205 §10.1 Algorithm 21 — `slh_keygen`)
|
||||
|
||||
| FIPS 205 § | Topic | Magnetar code |
|
||||
|---|---|---|
|
||||
| §10.1 Algorithm 21 (`slh_keygen`) | Sample (`SK.seed`, `SK.prf`, `PK.seed`) randomly; derive `PK.root` from FORS / hypertree | dispatched via `cloudflare/circl/sign/slhdsa.Scheme.DeriveKey` in `keygen.go:90` (`slhDSAKeyFromSeed`) |
|
||||
| §10.1 (key encoding) | `SK` = (SK.seed || SK.prf || PK.seed || PK.root); `PK` = (PK.seed || PK.root) | `keygen.go:64-83` (`KeyFromSeed`); `PrivateKey.Bytes` / `PublicKey.Bytes` carry the byte-equal layout via circl's `MarshalBinary` |
|
||||
|
||||
Magnetar's `GenerateKey(params, rng)` samples a fresh
|
||||
`params.SeedSize`-byte scheme seed from `rng` and dispatches to
|
||||
`KeyFromSeed`. The KAT generator (`ref/go/cmd/genkat`) uses fixed
|
||||
seeds for byte-stable output.
|
||||
|
||||
### §2.3 Sign (FIPS 205 §10.2 Algorithm 22 — `slh_sign`)
|
||||
|
||||
| FIPS 205 § | Topic | Magnetar code |
|
||||
|---|---|---|
|
||||
| §10.2 Algorithm 22 (`slh_sign`) | Compute SK.seed → FORS leaves; hypertree → root signature; pack (FORS sig || hypertree sig) | dispatched via `cloudflare/circl/sign/slhdsa.SignDeterministic` (or `SignRandomized`) in `sign.go:82-92` (`slhSign`) |
|
||||
| §10.2 (context string) | `ctx` ≤ 255 bytes; bound into the hash chain alongside the message | `sign.go:52-54` validates `len(ctx) > 255` → `ErrCtxTooLong`; circl's `SignDeterministic`/`SignRandomized` consume the ctx per FIPS 205 |
|
||||
| §10.2 (deterministic mode) | `slh_sign` is deterministic given (SK, M, ctx) | Magnetar's `Sign(params, sk, msg, ctx, randomized=false, rng)` produces byte-deterministic output; this is the load-bearing property that the threshold Combine path preserves |
|
||||
|
||||
Magnetar's threshold-Combine path uses `randomized=false` to
|
||||
guarantee byte-identical output to single-party Sign on the
|
||||
reconstructed seed (the Class-N1-analog byte-equality theorem,
|
||||
`SPEC.md` §6).
|
||||
|
||||
### §2.4 Verify (FIPS 205 §10.3 Algorithm 23 — `slh_verify`)
|
||||
|
||||
| FIPS 205 § | Topic | Magnetar code |
|
||||
|---|---|---|
|
||||
| §10.3 Algorithm 23 (`slh_verify`) | Parse signature; recompute hypertree root from signature + PK.seed; compare to PK.root | dispatched via `cloudflare/circl/sign/slhdsa.Verify` in `verify.go:104-109` (`slhVerify`) |
|
||||
| §10.3 (input validation) | Reject sigs/keys of wrong size; reject context > 255 | `verify.go:84-92` validates pk/sig sizes against `params.PublicKeySize` / `params.SignatureSize`; `len(ctx) > 255` returns `ErrCtxTooLong` |
|
||||
|
||||
Magnetar's `Verify` is intentionally minimal — a thin dispatch over
|
||||
circl's FIPS 205 `slhdsa.Verify`. This is the **Class-N1-analog
|
||||
manifesto in code**: any FIPS 205-conformant verifier accepts
|
||||
Magnetar threshold-emitted signatures with no code change. Adding
|
||||
logic to `Verify` would break output interchangeability with
|
||||
single-party FIPS 205 — the whole point of the Magnetar threshold
|
||||
variant.
|
||||
|
||||
### §2.5 Hash family (FIPS 202 + SP 800-185)
|
||||
|
||||
Magnetar's transcript-hash suite is uniformly FIPS 202 SHA-3 /
|
||||
SHAKE plus SP 800-185 cSHAKE256 / KMAC256. The function-name `N`
|
||||
is pinned to `"Magnetar"`; the customisation strings `S` are
|
||||
distinct per protocol round.
|
||||
|
||||
| FIPS 202 / SP 800-185 § | Primitive | Magnetar code |
|
||||
|---|---|---|
|
||||
| FIPS 202 §6.3 (cSHAKE256) | Customisable SHAKE256 with function-name `N` and customisation `S` | `transcript.go:46-52` (`cshake256(input, outLen, customisation)`) |
|
||||
| SP 800-185 §3 (cSHAKE algorithm) | `cSHAKE256(X, N, S, L) = SHAKE256(bytepad(encode_string(N) ‖ encode_string(S), 136) ‖ X, L)` | Implemented via `golang.org/x/crypto/sha3.NewCShake256` |
|
||||
| SP 800-185 §4 (KMAC256) | Keyed MAC over Keccak; output length specified | `transcript.go:56-65` (`kmac256(key, msg, outLen, customisation)`); reserved for v0.4 envelope auth |
|
||||
| SP 800-185 §2.3 (encoders) | `left_encode`, `right_encode`, `encode_string`, `bytepad` | `transcript.go:72-124` |
|
||||
| SP 800-185 §5 (TupleHash256) | Domain-separated tuple hash | Magnetar uses the TupleHash256-style construction inline via `transcriptHash` / `transcriptHash32` in `transcript.go:132-156` |
|
||||
|
||||
The customisation tags used in Magnetar:
|
||||
|
||||
| Tag | Purpose | Defined at |
|
||||
|---|---|---|
|
||||
| `MAGNETAR-DKG-COMMIT-V1` | committee-root digest | `transcript.go:29` (`tagDKGCommit`) |
|
||||
| `MAGNETAR-DKG-TRANSCRIPT-V1` | DKG transcript digest | `transcript.go:30` (`tagDKGTranscript`) |
|
||||
| `MAGNETAR-SIGN-R1-V1` | threshold-sign Round-1 commit `D_i` | `transcript.go:31` (`tagSignR1`) |
|
||||
| `MAGNETAR-SIGN-R1-MAC-V1` | (reserved for v0.4 MAC envelope) | `transcript.go:32` (`tagSignR1MAC`) |
|
||||
| `MAGNETAR-SIGN-MASK-V1` | per-attempt mask derivation | `transcript.go:33` (`tagSignMask`) |
|
||||
| `MAGNETAR-SEED-SHARE-V1` | Shamir coefficient stream + seed mix | `transcript.go:34` (`tagSeedShare`) |
|
||||
| `lux-magnetar-v0.1` | protocol-wide domain-separation context | `transcript.go:35` (`tagDomainSep`) |
|
||||
|
||||
## §3 Magnetar threshold overlay traceability (SPEC.md → code)
|
||||
|
||||
The threshold overlay layer is novel work; it does not trace to
|
||||
FIPS 205 (no NIST standard exists for threshold SLH-DSA). It
|
||||
traces to `SPEC.md` and to the classical literature it cites.
|
||||
|
||||
### §3.1 Byte-wise Shamir VSS over GF(257)
|
||||
|
||||
| `SPEC.md` § | Topic | Magnetar code | Classical reference |
|
||||
|---|---|---|---|
|
||||
| §3 Round-1 | Dealer Shamir-shares contribution byte-by-byte | `shamir.go:70-120` (`shamirDealRandomGF`) | Shamir 1979 (information-theoretic secret sharing) |
|
||||
| §4 Combine step 3 | Aggregator Lagrange-interpolates byte-sum at `x=0` over GF(257) | `shamir.go:127-174` (`shamirReconstructGF`) | Classical Lagrange interpolation |
|
||||
| §3 wire layout | Share encoded as 1 big-endian uint16 per byte position (GF(257) packed in 16-bit lane) | `shamir.go:198-206` (`shareToBytes`); `shamir.go:208-216` (`shareFromBytes`) | — |
|
||||
|
||||
### §3.2 Three-round DKG
|
||||
|
||||
| `SPEC.md` § | Topic | Magnetar code |
|
||||
|---|---|---|
|
||||
| §3 Round-1 | Dealer samples contribution `c_i`, Shamir-shares it, broadcasts per-recipient envelopes (`share || contribution`) | `dkg.go:137-181` (`DKGSession.Round1`) |
|
||||
| §3 Round-2 | Each party validates envelope set; computes transcript digest binding ordered envelope set; broadcasts digest | `dkg.go:185-240` (`DKGSession.Round2`) + `dkg.go:244-269` (`computeR2Digest`) |
|
||||
| §3 Round-3 | Each party verifies digests; sums per-byte shares; sums contributions; mixes byte-sum + committee root via cSHAKE256 to recover master seed; derives group public key via `KeyFromSeed`; outputs `KeyShare` | `dkg.go:278-418` (`DKGSession.Round3`) |
|
||||
| §3 identifiable abort (equivocation) | Digest mismatch produces `AbortEvidence{Kind: ComplaintEquivocation, Evidence: my_digest || accused_digest}` | `dkg.go:304-317` |
|
||||
|
||||
### §3.3 Two-round threshold sign + Combine
|
||||
|
||||
| `SPEC.md` § | Topic | Magnetar code |
|
||||
|---|---|---|
|
||||
| §4 Round-1 | Signer samples `rngBytes`; derives `r_i = cSHAKE256(rngBytes || sid || attempt || NodeID, tagSignMask)`; computes `masked_i = share_i XOR r_i`; commits `D_i = cSHAKE256(r_i || masked_i || tau_1, tagSignR1)` | `threshold.go:150-194` (`ThresholdSigner.Round1`) |
|
||||
| §4 Round-2 | Reveal `(r_i, masked_i)` packed as `PartialSig = r_i || masked_i` | `threshold.go:198-223` (`ThresholdSigner.Round2`) |
|
||||
| §4 Combine step 1 | Re-derive `D'_i` from reveals; gate on `ctEqual32(D'_i, D_i)`; reject on mismatch | `combine.go:75-116` |
|
||||
| §4 Combine step 2 | Recover `share_i = masked_i XOR r_i` | `combine.go:110-114` |
|
||||
| §4 Combine step 3 | Collect `t` distinct shares; Lagrange-interpolate at `x=0` over GF(257) | `combine.go:118-150` |
|
||||
| §4 Combine step 4-5 | Compute committee root; mix byte-sum + committee_root via cSHAKE256 (identical to DKG Round-3 step 6) | `combine.go:151-158` |
|
||||
| §4 Combine step 6-7 | Derive SLH-DSA secret key via `KeyFromSeed`; sanity-check pk matches `groupPubkey`; sign via FIPS 205 `slhdsa.SignDeterministic` | `combine.go:163-195` |
|
||||
| §4 Combine step 8 | Zeroize every secret-bearing buffer on every return path | `combine.go:164-203` (explicit, no `defer`) |
|
||||
| §6 byte-equality claim | Threshold output byte-equals `slhdsa.SignDeterministic(KeyFromSeed(S), msg, ctx)` | empirically `n1_byte_equality_test.go:TestN1_ByteEquality_*` |
|
||||
|
||||
### §3.4 Domain separation + transcript binding
|
||||
|
||||
| Topic | Magnetar code |
|
||||
|---|---|
|
||||
| Per-protocol-round customisation strings | `transcript.go:28-36` (all tags constant; rotating a tag invalidates KATs pinned at that tag) |
|
||||
| TupleHash256-style binding (length-prefixed parts) | `transcript.go:126-156` (`transcriptHash`, `transcriptHash32`) |
|
||||
| Constant-time byte equality | `transcript.go:158-179` (`ctEqualSlice`, `ctEqual32`) |
|
||||
| Canonical committee ordering (big-endian byte order) | `transcript.go:181-190` (`nodeIDLess`); used to sort committee for `committeeRoot` |
|
||||
|
||||
## §4 What this document is NOT
|
||||
|
||||
- NOT a NIST FIPS 140-3 module-validation reference (FIPS 140-3
|
||||
applies to packaged cryptographic modules, not the algorithm
|
||||
reference).
|
||||
- NOT an ACVP test-vector specification (NIST has no ACVP test
|
||||
vector set for threshold SLH-DSA; the single-party FIPS 205 layer
|
||||
in `cloudflare/circl/sign/slhdsa` is independently ACVP-testable).
|
||||
- NOT a security proof. FIPS 205's security is NIST's analysis;
|
||||
Magnetar's threshold-overlay security argument lives in
|
||||
`SPEC.md` §6 (byte-equality claim) and is empirically validated
|
||||
by `TestN1_ByteEquality_*`. EC theories that mechanize this
|
||||
mapping for the threshold overlay are roadmap v0.5.0 (see
|
||||
`AXIOM-INVENTORY.md` §2 + `PROOF-CLAIMS.md` §3).
|
||||
- NOT a mechanized refinement against FIPS 205. The single-party
|
||||
FIPS 205 layer is NIST-anchored; the threshold overlay is novel.
|
||||
|
||||
This document is the **citation discipline**: every operation in
|
||||
the shipped code traces to a specific FIPS 205 / FIPS 202 /
|
||||
SP 800-185 section (for the single-party + hash layer), or to a
|
||||
specific `SPEC.md` section (for the Magnetar threshold overlay).
|
||||
|
||||
## §5 Cross-references
|
||||
|
||||
- `SUBMISSION.md` — submission cover sheet
|
||||
- `SPEC.md` — protocol specification (single-party + threshold overlay)
|
||||
- `AXIOM-INVENTORY.md` — residual axiom inventory
|
||||
- `PROOF-CLAIMS.md` — narrow claim + non-claims
|
||||
- `TRUSTED-COMPUTING-BASE.md` — TCB
|
||||
- NIST FIPS 205 — single-party SLH-DSA normative reference
|
||||
- NIST FIPS 202 — SHA-3 / SHAKE normative reference
|
||||
- NIST SP 800-185 — cSHAKE / KMAC normative reference
|
||||
|
||||
---
|
||||
|
||||
**Document metadata**
|
||||
|
||||
- Name: `FIPS-TRACEABILITY.md`
|
||||
- Version: v0.1 (initial Tier A submission-package scaffolding)
|
||||
- Date: 2026-05-18
|
||||
+306
@@ -0,0 +1,306 @@
|
||||
# PROOF-CLAIMS — Magnetar (HONEST framing)
|
||||
|
||||
> **What this submission proves, and — critically — what it does NOT.**
|
||||
> Companion to `TRUSTED-COMPUTING-BASE.md` (TCB) and `SUBMISSION.md`
|
||||
> (cover sheet).
|
||||
>
|
||||
> Read this before reading the Magnetar code. The framing matters as
|
||||
> much as the implementation.
|
||||
|
||||
## §1 The narrow claim Magnetar makes at this submission
|
||||
|
||||
The strongest precise statement supported by Magnetar v0.3.0:
|
||||
|
||||
> **Byte-equal threshold to single-party FIPS 205 SLH-DSA
|
||||
> (Class N1).** For any honest threshold-sign session over committee
|
||||
> `[n]` with reconstruction threshold `t`, any signing quorum `Q ⊆ [n]`
|
||||
> of size `t`, message `m`, context `ctx`, session-id `sid`, attempt
|
||||
> `kappa`, where each party holds a `KeyShare` from a successful
|
||||
> Magnetar DKG ceremony, the signature byte string `sigma` emitted by
|
||||
> Magnetar `Combine(...)` satisfies:
|
||||
>
|
||||
> `sigma = slhdsa.SignDeterministic(slhdsa.Scheme(ID).DeriveKey(S), NewMessage(m), ctx)`
|
||||
>
|
||||
> where `S` is the master SLH-DSA scheme seed computed at DKG Round 3
|
||||
> (which equals the Lagrange-reconstructed seed at Combine time).
|
||||
> Therefore `sigma` verifies under unmodified FIPS 205
|
||||
> `slhdsa.Verify(pk, NewMessage(m), sigma, ctx)` with `pk` = the
|
||||
> DKG-output group public key.
|
||||
|
||||
**Formal-statement status**: this is stated in prose and code,
|
||||
validated by test (`TestN1_ByteEquality_*` across (3,2), (5,3), (7,4)
|
||||
configurations), validated by KAT determinism, and inherited from
|
||||
FIPS 205 SLH-DSA's NIST security analysis for the single-party
|
||||
layer. It is **NOT mechanized** in EasyCrypt, Lean, Jasmin, or any
|
||||
other proof assistant at this submission **for the threshold
|
||||
overlay layer**. See §3 below for the explicit non-claims list.
|
||||
|
||||
## §2 What IS provided
|
||||
|
||||
| Aspect | Status | Source |
|
||||
|---|---|---|
|
||||
| Implementation of the FIPS 205 single-party layer | ✓ by dispatch to `cloudflare/circl/sign/slhdsa` (community-audited mainstream Go FIPS 205 implementation) | `keygen.go`, `sign.go`, `verify.go` |
|
||||
| Class N1 (threshold output byte-identical to centralized FIPS 205 SignDeterministic on reconstructed seed) | ✓ by test (no mechanized refinement) | `n1_byte_equality_test.go` — `TestN1_ByteEquality_ThresholdMatchesCentralized`, `TestN1_ByteEquality_DifferentQuorumsSameSignature` |
|
||||
| KAT determinism | ✓ by deterministic regeneration | `vectors/{keygen,sign,verify,threshold-sign,dkg}.json`; `ref/go/cmd/genkat` consumes fixed seeds + committed config |
|
||||
| Constant-time discipline on commit verification and pubkey equality | ✓ by code (local `ctEqualSlice` / `ctEqual32` helpers) | `transcript.go` (helpers), `combine.go` (Round-2 commit gate), `keygen.go` (PublicKey.Equal) |
|
||||
| Identifiable-abort evidence (DKG equivocation) | ✓ by test | `dkg.go` Round-3 emits `AbortEvidence{Kind: ComplaintEquivocation, Evidence: my_digest || accused_digest}` on digest mismatch |
|
||||
| Domain separation across protocol round transcripts | ✓ by code (single source of truth: `transcript.go`) | `tagDKGCommit`, `tagDKGTranscript`, `tagSignR1`, `tagSignMask`, `tagSeedShare` — all centralised constants |
|
||||
| Secret-buffer zeroization on every Combine return path | ✓ by code review | `combine.go` — explicit `zeroizeBytes`/`zeroizePrivateKey` at every error and success exit, no `defer` (locally-legible secret lifetime) |
|
||||
|
||||
## §3 What is NOT proved (HONEST)
|
||||
|
||||
This section is the load-bearing honesty disclosure. Read it.
|
||||
|
||||
### §3.1 NOT proved: mechanized refinement of the threshold overlay
|
||||
|
||||
Magnetar ships **no EasyCrypt theories, no Lean theorems, no Jasmin
|
||||
sources** specific to the threshold overlay layer. Pulsar (the M-LWE
|
||||
sibling at `~/work/lux/pulsar/`) ships 13/13 EasyCrypt files
|
||||
compiling clean with 0/0 admits, 5/5 Lean ↔ EC bridges, and 3/3
|
||||
jasmin-ct blocking gates on the threshold layer. **Magnetar does
|
||||
NOT** ship this for the threshold overlay.
|
||||
|
||||
**What IS available upstream (but NOT redistributed in this
|
||||
submission)**: libjade has SLH-DSA formal CT artifacts for the
|
||||
**single-party FIPS 205 layer**. Magnetar's `Verify` and the
|
||||
Combine-internal `SignDeterministic` call route through
|
||||
`cloudflare/circl/sign/slhdsa`, not libjade's extracted code, so
|
||||
Magnetar does not redistribute or re-verify libjade's artifacts.
|
||||
A future Tier A++ delivery could either (a) integrate libjade's
|
||||
verified single-party SLH-DSA, or (b) cross-cite libjade's CT
|
||||
analysis as supporting evidence for the single-party half of the
|
||||
trust chain. Neither is in scope for v0.3.0.
|
||||
|
||||
**Why no mechanized refinement of the overlay**: writing EC theories
|
||||
for the threshold overlay (byte-wise Shamir VSS over GF(257),
|
||||
three-round DKG transcript binding, two-round commit-bind sign,
|
||||
cSHAKE256 mix to reconstructed seed) is a multi-month research
|
||||
project. Pulsar took ~13 EC iterations (v4-v13) to drive admit
|
||||
budget to 0/0 with extensive Lean-bridged algebraic identities.
|
||||
Magnetar's algebraic identities are essentially identical to
|
||||
Pulsar's (same byte-wise Shamir over GF(257), same Lagrange
|
||||
reconstruction). The closure path is cross-citation: many Magnetar
|
||||
EC theory shells can re-use Pulsar's Lean ↔ EC bridges for the
|
||||
Shamir / Lagrange identities, with Magnetar-specific theory shells
|
||||
covering only the SLH-DSA-specific mix and key derivation. See
|
||||
`AXIOM-INVENTORY.md` §2 for the closure plan.
|
||||
|
||||
**What this means in practice**: a NIST reviewer should NOT expect
|
||||
to find a `Magnetar_N1.ec` file with a `magnetar_n1_byte_equality_extracted`
|
||||
lemma analogous to Pulsar's. The trust base for Magnetar's
|
||||
byte-equality correctness reduces to:
|
||||
|
||||
- The FIPS 205 SLH-DSA standard (NIST 2024).
|
||||
- The `cloudflare/circl/sign/slhdsa` Go reference implementation.
|
||||
- The Go reference implementation review of the threshold overlay.
|
||||
- The KAT determinism check (`ref/go/cmd/genkat`).
|
||||
- The `TestN1_ByteEquality_*` empirical byte-equality harness.
|
||||
- The constant-time review documented in this file's §3.4.
|
||||
|
||||
### §3.2 NOT proved: post-quantum hardness of SLH-DSA
|
||||
|
||||
This submission says nothing about the post-quantum hardness of
|
||||
SLH-DSA itself. SLH-DSA's security rests on the collision and
|
||||
preimage resistance of the underlying hash (SHAKE for the Magnetar
|
||||
parameter sets), under the FIPS 205 (NIST 2024) analysis.
|
||||
|
||||
**The defensible PQ-safety claim**:
|
||||
> Magnetar implements FIPS 205 SLH-DSA (NIST 2024 stateless
|
||||
> hash-based signature standard) on three parameter sets:
|
||||
> SHAKE-192s (NIST PQ Cat 3, recommended), SHAKE-192f (Cat 3 fast),
|
||||
> SHAKE-256s (Cat 5). The single-party security analysis is NIST's
|
||||
> per FIPS 205; the post-quantum hardness assumption is collision
|
||||
> and preimage resistance of SHAKE, with no lattice dependence.
|
||||
|
||||
**NOT defensible**:
|
||||
> Magnetar is proved post-quantum secure beyond the FIPS 205
|
||||
> analysis.
|
||||
|
||||
### §3.3 NOT proved: byte-equality with FIPS 204 ML-DSA or any R-LWE construction
|
||||
|
||||
Magnetar signatures are NOT byte-equal to FIPS 204 ML-DSA
|
||||
signatures (that is Pulsar's claim) or to any R-LWE construction
|
||||
(Corona's domain). The three constructions use different hardness
|
||||
families:
|
||||
|
||||
- Magnetar: hash-based (FIPS 205 SLH-DSA, SHAKE).
|
||||
- Pulsar: M-LWE (FIPS 204 ML-DSA).
|
||||
- Corona: R-LWE (Boschini et al. ePrint 2024/1113).
|
||||
|
||||
Any reviewer expecting cross-construction byte-equality should look
|
||||
at the dedicated sibling for the desired hardness family.
|
||||
|
||||
### §3.4 NOT proved: statistical constant-time validation (dudect)
|
||||
|
||||
Magnetar's threshold-overlay code paths use constant-time helpers
|
||||
(`ctEqualSlice`, `ctEqual32`) for every commit verification and
|
||||
public-key equality check; secret-dependent branches are absent
|
||||
from `verify.go`, `sign.go`, and the Combine commit-verify gate.
|
||||
**However, no dudect-style statistical timing harness ships at
|
||||
v0.3.0.** A dudect harness is roadmap item v0.4+; at submission
|
||||
scaffolding time the constant-time evidence is:
|
||||
|
||||
- Code review: secret-dependent branches identified and replaced
|
||||
with constant-time helpers in `transcript.go`.
|
||||
- `cloudflare/circl`'s upstream constant-time claims for the
|
||||
FIPS 205 single-party layer.
|
||||
- The single-party layer's eventual libjade CT formal artifacts
|
||||
(available upstream, not redistributed here).
|
||||
|
||||
Pulsar's dudect harness is wired but not yet at submission-grade
|
||||
sample count (10⁹). Magnetar's equivalent harness is roadmap.
|
||||
|
||||
### §3.5 NOT proved: implementation-side covert-channel safety
|
||||
|
||||
The constant-time review does NOT address:
|
||||
- Memory-access leakage (cache-timing side channels)
|
||||
- Power side-channels
|
||||
- EM side-channels
|
||||
- Fault attacks
|
||||
- Microarchitectural leakage (Spectre / Meltdown class)
|
||||
- Statistical timing under realistic deployment conditions
|
||||
|
||||
Production deployments MUST follow the hardening checklist in
|
||||
`DEPLOYMENT-RUNBOOK.md` (mlock pinning, core-dump disable, ptrace
|
||||
disable, TEE attestation, dedicated host, etc.).
|
||||
|
||||
### §3.6 NOT proved: protocol-level adversarial robustness beyond reveal-and-aggregate
|
||||
|
||||
The byte-equality claim in §1 is **honest-quorum correctness +
|
||||
aggregator-trusted-during-Combine**. It says: "when all parties
|
||||
follow the protocol AND the aggregator process is trusted for the
|
||||
brief seed-reconstruction window, the output verifies under
|
||||
single-party FIPS 205." It does NOT prove:
|
||||
|
||||
- **Unforgeability** under adaptive corruption of the threshold
|
||||
protocol — inherited (with caveats) from the reveal-and-aggregate
|
||||
trust model where the aggregator is TCB; no Magnetar-specific
|
||||
mechanization.
|
||||
- **Identifiable abort** under network partition — synchronous
|
||||
network assumptions hold; async abort is out of scope.
|
||||
- **Robust completion** under `f < t/2` Byzantine parties — the
|
||||
honest-quorum claim does not address robust signing under
|
||||
partial dishonesty.
|
||||
- **Network-observer envelope confidentiality in v0.1** — v0.1
|
||||
envelopes are plaintext (KAT-deterministic). A passive observer
|
||||
can collect shares; v0.4 closes this with ML-KEM-768 envelope
|
||||
wrapping (matching Pulsar CR-8). See `BLOCKERS.md` BLK-4.
|
||||
- **Threshold secrecy without aggregator trust** — v0.1 is
|
||||
reveal-and-aggregate. A v0.2 full-MPC construction (aggregator
|
||||
never sees the seed) is on the research path, no committed target.
|
||||
|
||||
### §3.7 NOT proved: external Lean theorems or EC bridges specific to Magnetar
|
||||
|
||||
Magnetar has NO Lean-bridged algebraic axioms specific to its
|
||||
implementation. Pulsar has 5: `lagrange_inverse_eval`,
|
||||
`threshold_partial_response_identity`, `add_share_zeroR`,
|
||||
`reconstruct_linear`, `shamir_correct`. The Lagrange-aggregation
|
||||
identity over GF(257) that Magnetar uses in Combine is
|
||||
**algebraically identical** to Pulsar's GF(257) variant (same
|
||||
field, same Shamir secret-sharing scheme, same Lagrange basis
|
||||
evaluation at `x=0`). Closure plan: cross-citation to Pulsar's
|
||||
`proofs/lean-easycrypt-bridge.md` once Magnetar's EC theory shells
|
||||
land at v0.5.0; Magnetar-specific bridge entries needed only for
|
||||
the SLH-DSA-specific mix (cSHAKE256 with `MAGNETAR-SEED-SHARE-V1`
|
||||
tag) and the KeyFromSeed → SignDeterministic dispatch.
|
||||
|
||||
## §4 Refinement chain (what's connected to what)
|
||||
|
||||
```
|
||||
Go implementation (ref/go/pkg/magnetar/*.go)
|
||||
implements (by code review + KAT + TestN1_ByteEquality_*)
|
||||
FIPS 205 SLH-DSA standard (single-party layer)
|
||||
+ Magnetar threshold overlay (SPEC.md §3 DKG, §4 threshold sign, §6 byte-equality)
|
||||
conforms to (by inspection)
|
||||
SPEC.md §6 byte-equality claim (Class-N1-analog)
|
||||
← validated empirically by n1_byte_equality_test.go
|
||||
← validated empirically against cloudflare/circl FIPS 205 Verify
|
||||
```
|
||||
|
||||
Each "implements" / "conforms" relation is by **inspection and
|
||||
test**, NOT machine-checked for the threshold overlay. Compare to
|
||||
Pulsar's refinement chain (machine-checked at every step via
|
||||
EasyCrypt 13/13 + Lean bridges 5/5 + Jasmin-CT 3/3 against
|
||||
FIPS 204).
|
||||
|
||||
The single-party FIPS 205 layer IS NIST-anchored (FIPS 205 2024),
|
||||
which is the standard's analysis; Magnetar inherits it via the
|
||||
`cloudflare/circl/sign/slhdsa` dispatch in `keygen.go`, `sign.go`,
|
||||
`verify.go`, and the Combine-internal `slhSign` call.
|
||||
|
||||
## §5 What an auditor verifying this submission should do
|
||||
|
||||
1. **Read** the `SUBMISSION.md` cover sheet for context.
|
||||
2. **Read** this document (`PROOF-CLAIMS.md`) for what's proved vs not.
|
||||
3. **Read** `TRUSTED-COMPUTING-BASE.md` for the implementation TCB.
|
||||
4. **Read** `FIPS-TRACEABILITY.md` for the FIPS 205 § → code map.
|
||||
5. **Read** FIPS 205 (NIST 2024) §10 for the underlying single-party
|
||||
construction analysis (NIST standard).
|
||||
6. **Read** `SPEC.md` §3 (DKG), §4 (threshold sign), §6 (byte-equality
|
||||
claim), §7 (trust model).
|
||||
7. **Run** `GOWORK=off go test -count=1 -short -timeout 240s
|
||||
./ref/go/pkg/magnetar/` — expect all tests green, including
|
||||
`TestN1_ByteEquality_ThresholdMatchesCentralized` and
|
||||
`TestN1_ByteEquality_DifferentQuorumsSameSignature`.
|
||||
8. **Run** the KAT regeneration determinism check: backup `vectors/`,
|
||||
run `GOWORK=off go run ./ref/go/cmd/genkat -out=vectors/`, then
|
||||
`diff -qr vectors_backup/ vectors/` — expect zero differences.
|
||||
9. **Read** the Go reference implementation: `keygen.go`, `sign.go`,
|
||||
`verify.go`, `shamir.go`, `transcript.go`, `dkg.go`,
|
||||
`threshold.go`, `combine.go`, `zeroize.go`.
|
||||
|
||||
## §6 The honest one-paragraph version
|
||||
|
||||
> Magnetar's submission package establishes that the Go reference
|
||||
> implementation faithfully implements the FIPS 205 SLH-DSA
|
||||
> single-party standard via the `cloudflare/circl/sign/slhdsa` Go
|
||||
> reference, and adds a novel threshold lifecycle (byte-wise Shamir
|
||||
> VSS over GF(257) of the SLH-DSA scheme seed, three-round DKG with
|
||||
> transcript-digest equivocation detection, two-round commit-bind
|
||||
> threshold sign with masked-share reveal, identifiable-abort
|
||||
> evidence pipeline, KAT-deterministic Magnetar-SHA3 hash suite via
|
||||
> cSHAKE256 / KMAC256 per FIPS 202 + SP 800-185). Magnetar's headline
|
||||
> claim is byte-identity to single-party FIPS 205 SLH-DSA
|
||||
> `slhdsa.SignDeterministic` on the reconstructed master seed —
|
||||
> empirically validated by `TestN1_ByteEquality_*` across three
|
||||
> committee/threshold configurations. Unlike the Pulsar sibling
|
||||
> submission (which ships a mechanized EasyCrypt + Lean + Jasmin
|
||||
> refinement chain against FIPS 204), Magnetar ships NO machine-checked
|
||||
> refinement at this submission **for the threshold overlay layer** —
|
||||
> the SLH-DSA single-party layer is FIPS-anchored (NIST 2024) but
|
||||
> mechanizing the threshold overlay itself is a multi-month research
|
||||
> roadmap item. Magnetar's correctness evidence reduces to: code
|
||||
> review of the Go reference against the FIPS 205 standard + the
|
||||
> Magnetar SPEC.md, the KAT determinism check, the
|
||||
> `TestN1_ByteEquality_*` empirical byte-equality harness against
|
||||
> single-party FIPS 205, and the constant-time review documented in
|
||||
> §3.4. The proof tier is intentionally less mature than Pulsar's
|
||||
> for the threshold overlay; the roadmap items in `NIST-SUBMISSION.md`
|
||||
> §"Roadmap" lay out the multi-version path to mechanized refinement.
|
||||
|
||||
## §7 Roadmap (multi-version closure path)
|
||||
|
||||
| Milestone | Target version |
|
||||
|---|---|
|
||||
| ML-KEM-768 envelope wrapping of DKG Round-1 envelopes (closes passive-network-observer channel) | v0.4.0 |
|
||||
| Reshare protocol (Refresh + ReshareToNewSet) — Class N4-analog evidence | v0.4.0 |
|
||||
| EasyCrypt theory shells for the threshold overlay (refinement to FIPS 205) | v0.5.0 (research; multi-month) |
|
||||
| Lean ↔ EC bridge (cross-citation to Pulsar's Shamir / Lagrange bridges; or Magnetar-specific entries if needed) | v0.5.0 |
|
||||
| dudect-style statistical CT validation harness for the threshold overlay | v0.6.0 |
|
||||
| External cryptographic audit (engaged lab) | v0.6.0 |
|
||||
| Cross-implementation FIPS 205 verifier harness (BoringSSL / pq-crystals when SLH-DSA matures) | when third-party FIPS 205 implementations ship |
|
||||
| v0.2 full-MPC construction (aggregator never sees the master seed) | research, no committed target |
|
||||
|
||||
The closure path is real but long. The honest framing at this
|
||||
submission: production-hardened implementation of a FIPS-anchored
|
||||
single-party primitive with a novel reveal-and-aggregate threshold
|
||||
overlay, NOT machine-checked refinement of the threshold overlay
|
||||
against FIPS 205.
|
||||
|
||||
---
|
||||
|
||||
**Document metadata**
|
||||
|
||||
- Name: `PROOF-CLAIMS.md`
|
||||
- Version: v0.1 (initial Tier A submission-package scaffolding)
|
||||
- Date: 2026-05-18
|
||||
@@ -0,0 +1,246 @@
|
||||
# TRUSTED-COMPUTING-BASE — Magnetar implementation TCB
|
||||
|
||||
> **What you must trust to rely on Magnetar's byte-equality
|
||||
> correctness claim.** Companion to `PROOF-CLAIMS.md` (proof scope)
|
||||
> and `DEPLOYMENT-RUNBOOK.md` (operator-facing trust-model
|
||||
> disclosure).
|
||||
>
|
||||
> **HONESTY NOTE**: Magnetar's TCB is structurally simpler than
|
||||
> Pulsar's because Magnetar ships NO mechanized refinement layer for
|
||||
> the **threshold overlay** (no EasyCrypt theories specific to the
|
||||
> overlay, no Lean ↔ EC bridges specific to the overlay, no Jasmin
|
||||
> sources for the overlay). The FIPS 205 SLH-DSA single-party layer
|
||||
> DOES have upstream formal artifacts available (libjade's SLH-DSA
|
||||
> work) but Magnetar does not redistribute or re-verify them in this
|
||||
> submission. That removes the overlay-specific proof-tool TCB but
|
||||
> increases the trust placed in (i) the Go reference implementation
|
||||
> review of the threshold overlay, (ii) KAT determinism, and (iii)
|
||||
> the byte-equality test harness against the
|
||||
> `cloudflare/circl` FIPS 205 verifier. See `PROOF-CLAIMS.md` for
|
||||
> the honest framing.
|
||||
|
||||
## §0 Layered trust bases
|
||||
|
||||
The Magnetar byte-equality claim rests on three layered trust bases:
|
||||
|
||||
1. **The FIPS 205 SLH-DSA standard** — NIST FIPS 205 (2024). The
|
||||
single-party signing primitive's security analysis is NIST's; the
|
||||
Magnetar submission inherits it.
|
||||
2. **The Go reference implementation** — `ref/go/pkg/magnetar/`
|
||||
(~2200 LOC) plus `cloudflare/circl/sign/slhdsa` (the FIPS 205
|
||||
single-party reference). Reviewed by code inspection + KAT replay
|
||||
+ the `TestN1_ByteEquality_*` empirical byte-equality harness.
|
||||
3. **The trusted-computing base (TCB) below the implementation** —
|
||||
this document.
|
||||
|
||||
If any element of the TCB is unsound, the implementation's
|
||||
correctness is unsound regardless of how clean the code review was.
|
||||
|
||||
## §1 Implementation TCBs
|
||||
|
||||
### §1.1 Reference implementation (Go)
|
||||
|
||||
| Component | Trust | Mitigations |
|
||||
|---|---|---|
|
||||
| Magnetar Go reference (this repository) | Go standard-library correctness, `crypto/rand` randomness quality, transcript-hash primitives in `transcript.go` (cSHAKE256 / KMAC256), Shamir / Lagrange in `shamir.go`, DKG protocol in `dkg.go`, threshold-sign protocol in `threshold.go`, Combine in `combine.go` | Reviewed by code inspection; KAT replay (`vectors/*.json` regenerated byte-stably); `TestN1_ByteEquality_*` empirical byte-equality vs single-party FIPS 205 |
|
||||
| `github.com/cloudflare/circl/sign/slhdsa` | Cloudflare's audited Go reference implementation of FIPS 205 SLH-DSA. Used for: scheme-seed derivation (`Scheme.DeriveKey`), `SignDeterministic`, `Verify`. | Version pinned in `go.mod`. circl is the canonical mainstream Go FIPS 205 implementation; community-audited at Cloudflare scale. |
|
||||
| `golang.org/x/crypto/sha3` | cSHAKE256, KMAC256, TupleHash256 primitives (Go-stdlib-style). | Version pinned in `go.mod`. |
|
||||
| `crypto/subtle` | Constant-time byte-blob compare. Standard library. (Note: Magnetar uses local `ctEqualSlice` / `ctEqual32` constant-time helpers in `transcript.go` rather than `crypto/subtle.ConstantTimeCompare` for direct legibility; the algorithm is identical: scan every byte with `diff |= a[i] ^ b[i]`, return `diff == 0`.) | Standard library; bundled with the Go toolchain. |
|
||||
|
||||
### §1.2 Production targets (out of scope for v0.3.0)
|
||||
|
||||
| Target | Status |
|
||||
|---|---|
|
||||
| Optimized Rust crate | TODO — not in this submission |
|
||||
| C library + FFI | TODO — not in this submission |
|
||||
| WASM build | TODO |
|
||||
| no_std embedded | TODO |
|
||||
| C++ port | TODO — a future cross-runtime byte-equality harness (matching Pulsar's `luxcpp/crypto/pulsar/` and Corona's `luxcpp/crypto/corona/`) is a possible Tier A → Tier A++ evidence enhancement |
|
||||
|
||||
For each future target, an independent constant-time audit + KAT
|
||||
cross-validation + binding-level fuzzing is required before
|
||||
considering it "production." The byte-equality claim does NOT
|
||||
automatically transfer to these targets — each target's correctness
|
||||
must be re-verified.
|
||||
|
||||
## §2 Build TCBs
|
||||
|
||||
| Layer | What you trust | Reproducibility |
|
||||
|---|---|---|
|
||||
| **Go toolchain** | The Go compiler used to build the reference. The `go.mod` directive pins the language version. | Hard-pinned in `go.mod`; `go.sum` enforces module checksums. |
|
||||
| **`scripts/cut-submission.sh`** | The cut orchestrator's correctness — that it produces deterministic outputs from a fresh checkout. | Mirrors Pulsar's pattern; runs build → tests → KAT-regen verification → tar. |
|
||||
| **`scripts/check-high-assurance.sh`** | The high-assurance gate's correctness — `go build` + `go vet` + secret-log smoke scan. Skips proof-tool checks since Magnetar ships none for the overlay layer. | Honest about what's checked and what's not; documented in the script header. |
|
||||
| **`ref/go/cmd/genkat`** | Deterministic regeneration of KAT vectors. | The genkat tool consumes fixed seeds and produces byte-stable JSON output; re-running on a clean checkout produces byte-identical files. |
|
||||
|
||||
## §3 What the TCB does NOT include
|
||||
|
||||
Magnetar's TCB is **structurally simpler** than Pulsar's because
|
||||
Magnetar ships no mechanized refinement layer for the threshold
|
||||
overlay. The following are NOT in the Magnetar TCB:
|
||||
|
||||
- **EasyCrypt prover** (Pulsar trusts it; Magnetar has no EC
|
||||
theories for the overlay layer)
|
||||
- **Lean 4 + Mathlib** (Pulsar uses Lean-bridged algebraic axioms
|
||||
for Shamir / Lagrange identities; Magnetar has none of its own —
|
||||
closure plan is cross-citation to Pulsar's bridges, since the
|
||||
underlying GF(257) algebra is identical)
|
||||
- **Jasmin verified compiler** (Pulsar's threshold layer is in
|
||||
Jasmin; Magnetar's is pure Go)
|
||||
- **OCaml runtime** (EC is OCaml; Magnetar has no EC)
|
||||
- **jasmin-ct** (Magnetar's CT evidence is local-helper
|
||||
`ctEqualSlice` / `ctEqual32` review + the
|
||||
`cloudflare/circl` upstream constant-time claims for the FIPS 205
|
||||
single-party layer; statistical CT measurement is roadmap)
|
||||
|
||||
What IS in the Magnetar TCB but NOT in Pulsar's:
|
||||
|
||||
- **Greater dependence on the Go reference review of the threshold
|
||||
overlay.** Pulsar can fall back to the EC refinement chain if a
|
||||
Go reviewer misses a bug in the threshold layer; Magnetar's only
|
||||
line of defense for the overlay is reviewer + KAT determinism +
|
||||
the `TestN1_ByteEquality_*` harness against single-party FIPS 205.
|
||||
- **Greater dependence on `cloudflare/circl`'s FIPS 205
|
||||
implementation.** Pulsar's spec target (FIPS 204) is implemented
|
||||
both by `cloudflare/circl` AND independently by BoringSSL FIPS /
|
||||
AWS-LC / OpenSSL 3.0 (interop targets exist). Magnetar's spec
|
||||
target (FIPS 205) is at a less mature interop point — circl is
|
||||
the canonical Go implementation, but the mainstream third-party
|
||||
FIPS 205 implementations (BoringSSL, OpenSSL) are still landing
|
||||
at submission time.
|
||||
|
||||
## §4 What the TCB does NOT cover
|
||||
|
||||
These are explicitly NOT part of the trust base for Magnetar's
|
||||
byte-equality correctness claim:
|
||||
|
||||
- **Specific operating system** (Linux, macOS, BSD, Windows) — the
|
||||
Go reference is OS-independent.
|
||||
- **Specific CPU architecture** — Go compiles to amd64/arm64; both
|
||||
exercised in development.
|
||||
- **Network protocol stack** — Magnetar's transport is out of scope.
|
||||
- **Storage layer** — how `KeyShare` material is stored at rest is
|
||||
out of scope. Production deployments use HSM-backed share material
|
||||
or TEE-attested host configurations; see `DEPLOYMENT-RUNBOOK.md`.
|
||||
- **Key management policies** — key lifecycle is application-level
|
||||
(governed by the consuming consensus layer, e.g. Quasar Polaris
|
||||
profile).
|
||||
- **Application code calling Magnetar** — Magnetar's API contract
|
||||
is the trust boundary.
|
||||
|
||||
## §5 TCB risks and mitigations
|
||||
|
||||
### §5.1 Construction-soundness risk
|
||||
|
||||
| Risk | Mitigation |
|
||||
|---|---|
|
||||
| FIPS 205 SLH-DSA has a latent cryptanalytic flaw | NIST FIPS 205 (2024) is the published standard with extensive cryptanalytic review. Lux tracks cryptanalysis literature; any flaw would prompt NIST guidance, which Magnetar would inherit. The fundamental hardness assumption (collision/preimage resistance of SHAKE) is conservative. |
|
||||
| The Magnetar threshold lifecycle additions (byte-wise Shamir VSS, DKG, two-round commit-bind sign) have a latent bug | Per-protocol tests in `ref/go/pkg/magnetar/dkg_test.go`, `threshold_test.go`, `kat_test.go`, `n1_byte_equality_test.go`. Independent third-party audit is roadmap item, see `BLOCKERS.md` BLK-9. The byte-equality property to single-party FIPS 205 is the load-bearing N1 invariant; any threshold-layer bug that broke it would manifest in `TestN1_ByteEquality_*` failure. |
|
||||
|
||||
### §5.2 Implementation-correctness risk
|
||||
|
||||
| Risk | Mitigation |
|
||||
|---|---|
|
||||
| Go reference implementation diverges from the construction | `TestN1_ByteEquality_*` runs end-to-end DKG → threshold-sign → Combine and asserts byte-equality with `slhdsa.SignDeterministic(KeyFromSeed(reconstructed_seed), msg, ctx)`. Divergence = test failure. |
|
||||
| KAT vectors are subtly wrong | Deterministic generation from fixed seeds via `ref/go/cmd/genkat`. The KAT replay test (`kat_test.go`) validates that the package implementation reproduces every KAT entry verbatim. |
|
||||
| `cloudflare/circl/sign/slhdsa` has a bug in FIPS 205 implementation | circl is the canonical mainstream Go FIPS 205 implementation; community-audited at Cloudflare scale. A circl bug would also affect any other Go consumer of FIPS 205. Closure: cross-implementation verifier harness against a non-Go FIPS 205 implementation (e.g., pq-crystals reference C, BoringSSL when SLH-DSA lands) is roadmap, see `BLOCKERS.md` BLK-6. |
|
||||
| Hash-suite implementation bug (cSHAKE256 / KMAC256) | `golang.org/x/crypto/sha3` is a widely-used standard library implementation; bugs are rare and quickly patched. The Magnetar Shamir / Lagrange / mix operations route every call through `transcript.go` so any drift is a single-file change. |
|
||||
|
||||
### §5.3 Build / reproducibility risk
|
||||
|
||||
| Risk | Mitigation |
|
||||
|---|---|
|
||||
| `scripts/cut-submission.sh` produces non-deterministic output | The build is deterministic from fixed seeds; reproducible-build property is checked at every cut. The KAT regen step explicitly compares regenerated vectors against committed copies. |
|
||||
| Toolchain version drift between commits | `go.mod` pin + `go.sum` enforcement. |
|
||||
| KAT drift across runs | `ref/go/cmd/genkat` consumes only fixed seeds and committed config; output is byte-stable. The cut script diffs regenerated KATs against committed copies and fails on any divergence. |
|
||||
|
||||
### §5.4 Side-channel risk
|
||||
|
||||
| Risk | Mitigation |
|
||||
|---|---|
|
||||
| Timing leakage on secret-dependent paths in the threshold overlay | Constant-time helpers (`ctEqualSlice`, `ctEqual32`) are used for every commit verification and public-key equality check. Secret-dependent branches absent from `verify.go`, `sign.go`, and the Combine commit-verify gate. **Statistical validation via dudect is NOT yet in place** — roadmap item, see `PROOF-CLAIMS.md` §3.4. |
|
||||
| Timing leakage in the single-party FIPS 205 layer | `cloudflare/circl/sign/slhdsa` documents constant-time properties per FIPS 205 §6.3 guidance; libjade has SLH-DSA formal CT artifacts for the broader ecosystem. Magnetar does not redistribute these but inherits the upstream guarantees. |
|
||||
| Memory-access / cache-timing leakage | Not addressed at the software level. Production deployments should use TEE attestation (SGX, SEV-SNP, TDX) per `DEPLOYMENT-RUNBOOK.md` §1 ("v0.1 reveal-and-aggregate trust caveat"). |
|
||||
| Secret-buffer lifetime / coredump risk | The Combine path explicitly zeroizes every secret-bearing buffer (`masterSeed`, `sk_rec`, `byteSumBytes`, `mixInput`) at every error and success exit (`combine.go`). No `defer`-based zeroization; explicit at the return site for locally-legible secret lifetime. |
|
||||
|
||||
## §6 Independent verification protocol
|
||||
|
||||
To independently verify Magnetar's claims, a reviewer should:
|
||||
|
||||
1. Clone the repo at the submission tag.
|
||||
2. `GOWORK=off go build ./...` — expect clean build.
|
||||
3. `GOWORK=off go test -count=1 -short -timeout 240s ./ref/go/pkg/magnetar/` — expect all tests passing, including `TestN1_ByteEquality_*` across (3,2), (5,3), (7,4).
|
||||
4. Backup `vectors/`, run `GOWORK=off go run ./ref/go/cmd/genkat -out=vectors/`, then `diff -qr vectors_backup/ vectors/` — expect zero differences (KAT determinism).
|
||||
5. Read the Go reference implementation:
|
||||
- `params.go`, `types.go` — public types + FIPS 205 parameter sets
|
||||
- `keygen.go`, `sign.go`, `verify.go` — single-party FIPS 205 dispatch
|
||||
- `shamir.go` — byte-wise Shamir VSS over GF(257)
|
||||
- `transcript.go` — cSHAKE256 / KMAC256 / SP 800-185 helpers
|
||||
- `dkg.go` — three-round DKG
|
||||
- `threshold.go`, `combine.go` — two-round threshold sign + aggregator
|
||||
- `zeroize.go` — secret-buffer wipes
|
||||
6. Cross-reference with FIPS 205 (NIST 2024) §10.1 (parameter sets),
|
||||
§10.2 (Sign), §10.3 (Verify).
|
||||
7. Cross-reference with `SPEC.md` §3 (DKG), §4 (threshold sign),
|
||||
§6 (byte-equality claim), §7 (trust model).
|
||||
|
||||
If all 7 steps pass, the trust base reduces to the TCB enumerated
|
||||
in this document.
|
||||
|
||||
## §7 What this means for downstream consumers
|
||||
|
||||
For a downstream consumer (e.g., a Quasar consensus chain
|
||||
incorporating Magnetar as the hash-based PQ leg of the Polaris
|
||||
profile):
|
||||
|
||||
- **The byte-equality claim is conditional on the TCB.** If you
|
||||
change the Go toolchain, port to a different runtime, or modify
|
||||
the hash suite, the claim's transferable guarantees attenuate.
|
||||
- **For FIPS 140-3 module validation**, Magnetar's path is via
|
||||
the FIPS 205 SLH-DSA standard (NIST). The single-party FIPS 205
|
||||
layer in `cloudflare/circl` is independently validatable when
|
||||
FIPS 205 modules ship; the threshold overlay is not subject to
|
||||
FIPS 140-3 directly (there is no NIST standard for threshold
|
||||
SLH-DSA).
|
||||
- **For NIST MPTC review**, Magnetar's role is the algorithm-level
|
||||
reference + production lifecycle artifacts; module packaging +
|
||||
external audit are downstream.
|
||||
- **For threshold signing in a Quasar Polaris deployment**, Magnetar
|
||||
is the hash-based PQ kernel; the consuming consensus layer is
|
||||
responsible for the chain-of-custody and validator-rotation
|
||||
orchestration. The Magnetar reshare protocol (v0.4 roadmap)
|
||||
will provide the Class N4-analog primitive when it lands.
|
||||
|
||||
## §8 Honest comparison to Pulsar's and Corona's TCBs
|
||||
|
||||
| TCB element | Pulsar | Magnetar | Corona |
|
||||
|---|---|---|---|
|
||||
| EasyCrypt prover | YES (foundation of refinement proof, 13 files, 0/0 admits) | NO (no EC theories for the overlay layer) | NO |
|
||||
| Lean 4 + Mathlib | YES (5 Lean-bridged axioms) | NO (cross-citation closure on roadmap; Shamir/Lagrange algebraically identical to Pulsar's GF(257)) | NO |
|
||||
| Jasmin verified compiler | YES (threshold layer in Jasmin) | NO (pure Go; libjade covers SLH-DSA single-party but is not redistributed here) | NO (pure Go) |
|
||||
| OCaml runtime | YES (EC is OCaml) | NO | NO |
|
||||
| Go toolchain | YES (Go reference) | YES (Go reference; primary) | YES (Go reference) |
|
||||
| `cloudflare/circl` FIPS 205 | NO (Pulsar uses FIPS 204) | YES (FIPS 205 single-party kernel) | NO (R-LWE; no FIPS standard) |
|
||||
| `luxfi/lattice/v7` (lattigo fork) | NO | NO | YES (R-LWE primitives) |
|
||||
| `crypto/subtle` (or local CT helpers) | YES | YES (local `ctEqualSlice` / `ctEqual32`) | YES |
|
||||
| `golang.org/x/crypto/sha3` | YES | YES | YES |
|
||||
| NIST standard target | FIPS 204 ML-DSA | FIPS 205 SLH-DSA | none (Boschini ePrint 2024/1113) |
|
||||
| Third-party FIPS-validated verifier available | YES (BoringSSL FIPS / AWS-LC / OpenSSL 3.0 ML-DSA) | PARTIAL (FIPS 205 still landing in third-party stacks at submission time) | NO (none exists for R-LWE threshold) |
|
||||
|
||||
**Net effect**: Magnetar's TCB is smaller than Pulsar's (fewer
|
||||
proof-tool dependencies) but the trust per-component is higher
|
||||
(no fall-back to a mechanized refinement chain if a Go reviewer
|
||||
misses a bug in the threshold overlay). Compared to Corona, Magnetar
|
||||
has a STRONGER baseline because the single-party layer is FIPS-anchored
|
||||
(FIPS 205) while Corona's underlying construction is a 2024 academic
|
||||
paper with less cryptanalytic surface area.
|
||||
|
||||
---
|
||||
|
||||
**Document metadata**
|
||||
|
||||
- Name: `TRUSTED-COMPUTING-BASE.md`
|
||||
- Version: v0.1 (initial Tier A submission-package scaffolding)
|
||||
- Date: 2026-05-18
|
||||
- Go toolchain pin: see `go.mod`
|
||||
- `cloudflare/circl` pin: see `go.mod`
|
||||
- `golang.org/x/crypto` pin: see `go.mod`
|
||||
Reference in New Issue
Block a user