luxfi/magnetar
1
0
Fork 0
mirror of https://github.com/luxfi/magnetar.git synced 2026-07-27 02:53:47 +00:00
Code Issues Packages Projects Releases Wiki Activity

magnetar: remove proof-by-rename + circular proofs; honest threshold status

Browse Source 
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.
This commit is contained in:
Antje Worring
2026-06-21 13:06:57 -07:00
parent 2326a880cd
commit df4c537c16
33 changed files with 1685 additions and 2608 deletions
Download Patch File Download Diff File Expand all files Collapse all files
ASSEMBLE-INVARIANT.md
+65 -110
View File
@@ -1,128 +1,83 @@
# Magnetar v1.1 strict-atom Combine invariant
# Magnetar THBS-SE Combine: what the assemble path actually does
This document is the load-bearing prose statement of the strict-atom
discipline that closes `MAGNETAR-STRICT-ATOM-V11` in the v1.1 release.
This document used to be the "load-bearing prose statement of the
strict-atom discipline that closes MAGNETAR-STRICT-ATOM-V11". That
framing was wrong. MAGNETAR-STRICT-ATOM-V11 is **NOT closed** (see
`BLOCKERS.md`). This document now states plainly what
`ref/go/pkg/magnetar/thbsse_assemble.go` does.
## The four forbidden FIPS 205 master-binder identifiers
## The fact
The strict-atom emit path (`ref/go/pkg/magnetar/thbsse_assemble.go`)
is the public combiner's only point of contact with the FIPS 205
master byte material. The v1.1 audit grep that defines compliance:
`assembleSignatureBytes` RECONSTRUCTS the full FIPS 205 master at the
public combiner, every signature:
```
grep -rE "SK\.seed|SK\.prf|sk_seed|sk_prf" ref/go/pkg/magnetar/thbsse_assemble.go
```
1. It Lagrange-interpolates the t share envelopes byte-by-byte into a
buffer `derivedExpandInput`.
2. It SHAKE-expands that into a single buffer `derivedMaterial`
= `skSeed || skPrf || pkSeed` (FIPS 205 §10.1).
3. It drives a FIPS 205 §5--§8 signing walk that reads positional
slices of `derivedMaterial` (the §5/§6/§7/§8 PRF input and the
§11.2 PRF_msg key).
MUST return zero matches. The four sentinel patterns are:
For the duration of one Sign call, the entire private key is resident
in the combiner's process memory. The combiner is PUBLIC (any peer can
run it), so this is a reconstruction at an untrusted party.
| Pattern | Matches |
|---|---|
| `SK\.seed` | The FIPS 205 master skSeed field reference (dot notation, e.g. `SK.seed`, `sk.seed`). |
| `SK\.prf` | The FIPS 205 master skPrf field reference (dot notation). |
| `sk_seed` | The C-style snake-case form of skSeed (used in FIPS 205 reference C implementations). |
| `sk_prf` | The C-style snake-case form of skPrf. |
## The "strict-atom" naming convention is not a security property
The v1.0 Combine path (now deleted) had `seed := make(...)` and
`sk, err := KeyFromSeed(params, seed)` which would have tripped a
broader version of this grep on the variable name `seed`. The v1.1
strict-atom path does NOT have a `seed` variable; the corresponding
byte material exists ONLY as positional slices of a SHAKE-expansion
output buffer called `derivedMaterial`, named for the SHAKE absorb
context it feeds, not for the FIPS 205 field it represents.
The earlier revision avoided the identifier `seed` (and `skSeed`,
`skPrf`, ...) and routed access through closures over positional
slices of `derivedMaterial`. It then claimed this "secures" something
that a `seed []byte` local did not, and called it a discipline that
"closes" the no-leak gap.
## The discipline
That is false. Renaming the buffer changes the spelling, not the data.
`derivedMaterial` holds `skSeed || skPrf || pkSeed` exactly as a
variable named `seed` would. A memory-disclosure adversary (coredump,
`/proc/self/mem`, a compromised combiner process) observes the master
during the Sign call either way. There is no confidentiality property
to rely on, and the "strict-atom invariant" buys none.
1. The 96-byte Magnetar share envelope (the Shamir share of the
FIPS 205 master) is reconstructed BYTE-WISE into a transient
buffer `derivedExpandInput` for the duration of one
`SHAKE256(...)` absorb call. The buffer is zeroized immediately
after.
This is a fundamental property of hash-based signatures, not a fixable
implementation detail: there is no algebraic structure to aggregate,
so producing one FIPS 205-shaped signature from shares requires either
reconstructing the seed at some party (this path) or full MPC over the
SHAKE hash tree (open research; multi-second, multi-megabyte per
signature). See `standalone.go`'s banner for the literature
(Cozzo-Smart 2019, Bonte-Smart-Tan 2023, NIST IR 8214).
2. The SHAKE-256 expansion output `derivedMaterial[0:3n]` is the
v1.1 substrate for every secret-side PRF / PRF_msg call. It is
partitioned by POSITION:
## What the path actually gives
- `derivedMaterial[0 : n ]` --- the FIPS 205 §5/§6/§7/§8 PRF
secret input.
- `derivedMaterial[n : 2n ]` --- the FIPS 205 §11.2 PRF_msg
secret input.
- `derivedMaterial[2n : 3n ]` --- the public PK.seed segment,
cross-checked against the committee's published `pkBytes`.
ONE property, and it is a CORRECTNESS/INTEROP property, not a
confidentiality one:
The variable NAMESPACE of `thbsse_assemble.go` includes NO binder
for these segments. They are accessed exclusively by positional
slicing inside closures (`makePRFClosure`, `makePRFMsgClosure`).
> The emitted signature is byte-identical to
> `circl/slhdsa.SignDeterministic` on the reconstructed master, so any
> unmodified FIPS 205 verifier accepts it.
3. Each closure composes its SHAKE absorb input inside a transient
per-call buffer (`prfAbsorb`, `prfMsgAbsorb`), runs the SHAKE-256
call, and zeroizes the absorb buffer before returning.
Pinned by `TestSlhdsaInternal_ByteEqualToCirclSign` and
`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`.
4. The Magnetar-internal FIPS 205 §5--§8 walk
(`ref/go/pkg/magnetar/slhdsa_internal.go::slhSignAtom`) is driven
by the two callbacks. The walk itself touches only PUBLIC bytes
(the output of completed PRF calls is public per FIPS 205 §11.2);
the secret-side seam is exactly the two callbacks.
The scratch buffers (`prfAbsorb`, `prfMsgAbsorb`) and the derived
buffers (`derivedExpandInput`, `derivedMaterial`) are zeroized after
use. That is defense-in-depth against lingering heap copies, NOT a
guarantee the master was never resident — it was.
5. After `slhSignAtom` returns the FIPS 205 wire bytes,
`derivedMaterial` is zeroized via deferred wipes.
## Deployment positioning (see BLOCKERS.md and the product decision)
## What this discipline buys vs the v1.0 transient-seed model
- **Permissionless THBS-SE (this path): RESEARCH-GRADE.** Master is
reconstructed at an untrusted public combiner. Do not present as
production or as "no host in the TCB at sign time".
- **Production default:** per-validator standalone (`standalone.go`) —
N independent FIPS 205 signatures, no reconstruction anywhere.
- **Opt-in trusted-hardware:** the TEE-attested combiner pool in
`luxfi/threshold/protocols/slhdsa-tee`. That relocates the
reconstruction into a measured enclave; it ADDS a host to the TCB
(trust-relocation), it is not MPC.
The v1.0 transient-seed model had a `seed` variable in the public
combiner's stack frame for the duration of one
`circl.SignDeterministic` call. A peer-local memory-disclosure
adversary at exactly the combine moment could observe the seed.
## The lint
The v1.1 strict-atom discipline:
- Forbids any FIPS 205 master-binder identifier in `thbsse_assemble.go`
by the audit grep. Static, file-local invariant.
- Bounds the lifetime of the SHAKE-expanded master material to the
enclosing function call. `derivedMaterial` is allocated, used,
zeroized, and dropped in one function activation.
- Bounds the lifetime of the SHAKE-absorb scratch buffers to the
enclosing per-PRF-call closure. Each `prfAbsorb` /
`prfMsgAbsorb` lives across one SHAKE-256 absorb and is zeroized
before the closure returns.
What it does NOT buy (the Cozzo-Smart bound on threshold-MPC for
hash-based signatures):
- The bytes of the FIPS 205 master DO exist transiently in
`derivedMaterial` and in `derivedExpandInput`. A coredump or
/proc/self/mem dump at exactly the right wall-clock instant
would observe them.
This is the residual gap, honestly documented. Closing it would
require either:
- Full MPC over the SHAKE-256 hash tree (~minutes per signature,
~megabytes of comms; open research). NIST IR 8214 classifies this
as the highest threshold-MPC cost across FIPS 203/204/205.
- A TEE-attested host in the TCB (sibling primitive at
`luxfi/threshold/protocols/slhdsa-tee`; out of scope for Magnetar
which is the public-BFT-safe permissionless surface).
The strict-atom discipline is the strictest discipline available
without crossing into either of those two regimes. Audit grep +
positional-slice discipline + bounded lifetimes is the v1.1 bar.
## How this is enforced
| Layer | Mechanism | Source |
|---|---|---|
| Per-push Go test | AST walk + raw-byte grep | `ref/go/pkg/magnetar/thbsse_assemble_test.go::TestThbsSE_StrictAtom_NoTransientSeed` |
| Per-push shell gate | Raw grep, exit 2 on hit | `scripts/checks/strict-atom-ast.sh` |
| Per-push Go CT gate | AST walk on secret-tagged identifiers | `ct/dudect/strict_atom_combine_ct_test.go::TestStrictAtom_CT_NoSecretDependentBranch` |
| EasyCrypt abstract model | The abstract `assemble_signature_bytes` operator has no named seed binder | `proofs/easycrypt/Magnetar_N1_StrictAtom.ec` |
| Lean abstract model | `strictAtomDisciplineSatisfied` is the abstract counterpart | `proofs/lean/Crypto/Magnetar/StrictAtom.lean` |
## Backward compatibility
The wire format, share format, slot-guard state, and protocol round
structure of THBS-SE are UNCHANGED at v1.1. KAT vectors regenerate
to the same bytes. v1.0.0 consumers bump to v1.1.0 transparently
with no API break.
`TestThbsSE_AssembleIdentHygiene` (Go) and `scripts/checks/strict-atom-ast.sh`
are an IDENTIFIER-HYGIENE LINT over `thbsse_assemble.go`. They assert
no variable is *spelled* `seed`/`skSeed`/... . That is a style/naming
check. It is not, and does not claim to be, a no-leak proof.
AXIOM-INVENTORY.md
+54 -59
View File
@@ -11,11 +11,12 @@
> 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.
> Status: **there are NO EC/Lean theorems for the threshold overlay,
> present or planned.** The prior ones were vacuous and have been
> deleted (`PROOF-CLAIMS.md` §2). This document enumerates the
> construction-level + implementation-level axioms the code relies on;
> NONE are discharged by machine. The single-party FIPS 205 SLH-DSA
> layer is NIST-anchored (FIPS 205, 2024) and inherits NIST's analysis.
## §1 Construction-level axioms (cryptographic assumptions)
@@ -29,7 +30,7 @@ from NIST standards and the academic literature.
| **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. |
| **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. |
@@ -39,66 +40,62 @@ 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 |
> NOTE: the v0.x files this table once cited (`shamir.go`, `dkg.go`,
> `threshold.go`, `combine.go`) were DELETED. The current code is in
> `thbsse.go`, `thbsse_field.go`, `thbsse_assemble.go`,
> `slhdsa_internal.go`, `standalone.go`, `pvss_dkg.go`. The "closure
> plan = EC theory shells" entries below were FALSE: the EC track was
> vacuous and has been deleted (see `PROOF-CLAIMS.md` §2). Nothing here
> is on a credible near-term mechanization path.
| Axiom | Location | Status |
|---|---|---|
| `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. |
| `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`). |
| 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+.
Whatever Pulsar's posture, Magnetar has **zero** mechanized artifacts
for the threshold overlay. The prior claim that "the comparable axiom
inventory for Magnetar is the roadmap target of v0.5.0+" implied a
credible path; it was not credible (the EC track that was supposed to
seed it turned out vacuous and is deleted). Treat Magnetar as having NO
mechanized threshold proof, present or planned, until someone writes a
real one.
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.
What is genuinely simpler about Magnetar (if a proof were ever
attempted): SLH-DSA `SignDeterministic` is straight-line (no
rejection-sampling kappa loop), so a hypothetical byte-equality
refinement would be narrower than Pulsar's. But none exists.
## §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).
This document is NOT a claim of any closed proof, and NOT a roadmap to
one. There are no EC/Lean theorems for the threshold overlay, present
or scheduled; the prior ones were vacuous and removed (`PROOF-CLAIMS.md`
§2).
At v0.3.0, Magnetar's proof basis is:
Magnetar's actual 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.
2. Byte-wise Shamir over GF(257) + Lagrange reconstruction (standard,
not mechanized here).
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).
4. Byte-identity tests vs single-party FIPS 205
(`TestSlhdsaInternal_ByteEqualToCirclSign`,
`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`,
`TestMagnetar_Wire_FIPS205Verifiable`).
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`).
`cloudflare/circl/sign/slhdsa.Verify`; any FIPS 205-conformant
verifier accepts the output.
6. Code review: secret-dependent branches replaced with constant-time
helpers (`ctEqualSlice`, `ctEqual32`) where applicable.
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).
@@ -116,13 +113,11 @@ full Tier A cut-readiness Pulsar v1.0.7 holds (admit 0/0 across
- `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.
- `CRYPTOGRAPHER-SIGN-OFF.md` — internal review verdict (standalone
primitive only)
- `BLOCKERS.md` — sound / open / falsely-closed enumeration
- `PROOF-CLAIMS.md` §2 — the vacuous proof track that was deleted
- `proofs/README.md` — the empty proof track (scaffolds only)
---
BLOCKERS.md
+149 -248
View File
@@ -1,286 +1,187 @@
# Magnetar --- Blockers
Honest enumeration of what remains open at each release.
Honest enumeration of what is sound, what is open, and what was
falsely marked closed.
## v1.2 ship state (current)
## Deployment model (the product decision)
v1.2 closes `MAGNETAR-PVSS-DKG-V11` --- the leaderless PVSS-DKG that
removes the trusted dealer from the THBS-SE setup. The v1.2 ship
state is the first Magnetar release with a fully dealerless setup
path; the dealer-path `NewThbsSeKey` is retained for KAT
reproducibility but is no longer recommended for production.
Magnetar ships ONE construction to each of three deployment regimes:
The two paths emit byte-shape-identical share envelopes (pinned by
`TestPVSS_DKG_ByteCompatWithDealerPath`), so already-deployed share
material is forward-compatible with the dealerless setup.
| Regime | Construction | Posture |
|---|---|---|
| **Permissionless public-BFT (DEFAULT, production)** | Per-validator standalone (`standalone.go`) | SOUND. Each validator holds its own FIPS 205 keypair, signs independently; consensus collects N signatures into a `ValidatorAggregateCert`. No DKG, no dealer, no reconstruction anywhere. |
| **Trusted-hardware / custody (opt-in, production)** | TEE-attested combiner pool (`luxfi/threshold/protocols/slhdsa-tee`) | SOUND under an explicit, honest trust model: the whole seed is reconstructed INSIDE a measured enclave on t hosts that must agree. This is TRUST-RELOCATION (it adds a host to the TCB), NOT MPC. |
| **Permissionless threshold THBS-SE (RESEARCH-ONLY)** | `thbsse.go` + `thbsse_assemble.go` + PVSS-DKG | RESEARCH-GRADE. The public combiner reconstructs the full FIPS 205 master every signature. Do NOT present as production or "no host in the TCB at sign time". |
## v1.1 ship state (historical)
The hash-based-signature literature is unambiguous that this is
fundamental (Cozzo-Smart EUROCRYPT 2019; Bonte-Smart-Tan 2023; NIST IR
8214): SLH-DSA has no aggregatable structure, so one FIPS 205-shaped
signature from shares requires either reconstructing the seed at some
party or full MPC over the SHAKE hash tree. Magnetar's PRIMARY
production answer (per-validator standalone) sidesteps the dilemma by
emitting N independent signatures.
v1.1 closed the v1.0 strict-atom + proof-track + dudect open items.
See `CHANGELOG.md` v1.1.0 for the closure summary.
## OPEN --- MAGNETAR-STRICT-ATOM --- THBS-SE reconstructs the master
## v1.0 ship state
**Status: OPEN. (Previously, and falsely, marked CLOSED.)**
The two primitives shipped at v1.0 are:
`assembleSignatureBytes` (`thbsse_assemble.go`) reconstructs the full
FIPS 205 master at the public combiner: it Lagrange-interpolates the
shares into `derivedExpandInput`, SHAKE-expands them into
`derivedMaterial` (= skSeed || skPrf || pkSeed), and drives the FIPS
205 §5--§8 walk reading positional slices of that buffer
(`ASSEMBLE-INVARIANT.md`). The whole private key is resident in the
combiner's memory for one Sign call.
- **Per-validator standalone**
(`ref/go/pkg/magnetar/standalone.go`) --- the public-BFT primary
primitive. Each validator runs `PerValidatorKeypair` and
`ValidatorSign`; the consensus layer collects N signatures into
`ValidatorAggregateCert` and verifies via `VerifyAggregateCert`.
This is the production-ready surface.
The earlier "strict-atom" closure was PROOF BY RENAME: the path avoids
*spelling* a variable `seed`, and a name-grep test/lint
(`TestThbsSE_AssembleIdentHygiene`, `scripts/checks/strict-atom-ast.sh`)
enforces the spelling. Renaming the buffer does not change the data.
The "CT" gate (`ct/dudect/strict_atom_combine_ct_test.go`) is likewise
a name lint, not a timing measurement — and constant-time is the wrong
property to claim for a path that holds the master in plaintext.
- **THBS-SE** (Threshold Hash-Based Signatures with Selected-Element
Reconstruction;
`ref/go/pkg/magnetar/thbsse.go` + `thbsse_field.go`) --- the
permissionless threshold companion. t-of-n committee, slot-bound
commit-and-reveal, anyone-can-combine public combiner, slashable
evidence for equivocation and malformed shares.
**What IS true:** the emitted signature is byte-identical to
`circl/slhdsa.SignDeterministic` on the reconstructed master (a
correctness/interop property, pinned by
`TestSlhdsaInternal_ByteEqualToCirclSign` and
`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`). That is the only
property the path delivers. It is NOT a no-leak property.
Both emit byte-identical FIPS 205 signatures any unmodified verifier
accepts.
**Closing it** requires full MPC over the SHAKE hash tree (open
research; multi-second, multi-megabyte per signature) or a TEE-attested
host in the TCB (the opt-in pool below). The permissionless THBS-SE
path stays RESEARCH-ONLY.
## Open items at v1.0
## SOUND (with an honest trust model) --- TEE-attested combiner pool
### MAGNETAR-STRICT-ATOM-V11 --- Strict per-atom THBS-SE Combine
The strict-PQ / custody regime routes Combine through a t-of-n
attested-combiner pool in
`luxfi/threshold/protocols/slhdsa-tee/pool.go`, gated by the single
profile function `magnetarRefuseUnderStrictPQ` in
`luxfi/threshold/pkg/thresholdd/magnetar.go` (mirrors the precompile
`contract.RefuseUnderStrictPQ` discipline: ONE function, ONE place, ONE
refusal sentinel `slhdsatee.ErrMagnetarNoTEEAttestation`).
**Status:** CLOSED at v1.1.0. See `ASSEMBLE-INVARIANT.md` for the
load-bearing prose statement and `CHANGELOG.md` v1.1.0 for the
release summary.
**Honest trust model.** The seed is still RECONSTRUCTED in full — but
inside a MEASURED ENCLAVE whose binary + firmware chain-validate to the
vendor root (AMD KDS / Intel PCS / NVIDIA NRAS). t hosts must agree on
the output. This is TRUST-RELOCATION: it moves the reconstruction from
an untrusted public combiner into attested hardware, ADDING that
hardware (and the attestation chain, and the t hosts) to the TCB. It is
NOT MPC; no party is prevented from seeing the seed — the enclave sees
it. Use it when you are willing to trust attested hardware; do not call
it threshold cryptography that keeps the seed secret from every party.
**Closure shape.** The v1.1 Combine path is implemented at
`ref/go/pkg/magnetar/thbsse_assemble.go::assembleSignatureBytes`
backed by `ref/go/pkg/magnetar/slhdsa_internal.go::slhSignAtom`
(Magnetar-internal FIPS 205 sec 5--sec 8 walk for the SHAKE family).
The strict-atom discipline is the four-pattern audit grep:
**Production attestation kinds.** SEV-SNP is the only `cc/attest`
verifier currently production-implemented. TDX / NRAS verifiers are
stubs returning `ErrNotImplemented` (tracked at #222 stages 2--3); they
wire through the same pool contract once shipped (an addition to
`CombinerPoolConfig.KnownIssuers`, no magnetar-side change).
```
grep -rE "SK\.seed|SK\.prf|sk_seed|sk_prf" thbsse_assemble.go
```
**Pool policy defaults:** `Threshold = 2` (2-of-3 attested combiners),
`RotationWindow = 60s` (per-member attestation freshness),
`KnownIssuers = {"amd.sev.snp"}`.
returns ZERO, enforced by `TestThbsSE_StrictAtom_NoTransientSeed`
(AST walk + raw-byte grep) and `scripts/checks/strict-atom-ast.sh`
(shell gate). Byte-identity to `cloudflare/circl/sign/slhdsa.
SignDeterministic` is pinned by `TestSlhdsaInternal_ByteEqualToCirclSign`
across all three SHAKE modes.
**Verification gates (BUILD + PASS under `-race`).** As of the
`luxfi/zap` bump to v0.3.1 in `luxfi/threshold` (which restores the
`NodeConfig.TLS` field that `pkg/thresholdd` needs to build), the five
gates build and pass under `-race`:
**Residual gap.** The bytes of the FIPS 205 master DO exist
transiently inside `derivedMaterial` (the SHAKE-expansion output
buffer) and `derivedExpandInput` (the Lagrange-reconstructed input
to SHAKE) for the duration of the SHAKE absorb. A coredump or
/proc/self/mem dump at exactly the right wall-clock instant would
observe them. Closing this gap requires either full MPC over the
SHAKE-256 hash tree (open research; multi-second per signature) or
a TEE-attested host in the TCB (sibling primitive at
`luxfi/threshold/protocols/slhdsa-tee`). The strict-atom discipline
is the strictest discipline available without crossing into either
regime; see `ASSEMBLE-INVARIANT.md` for the honest statement.
- `TestMagnetarCombine_StrictPQProfile_RequiresTEE` --- PASS (~77s)
- `TestMagnetarCombine_AttestationVerified_AllowsSign` --- PASS (~95s)
- `TestMagnetarCombine_StaleAttestation_RejectsSign` --- PASS (~128s)
- `TestMagnetarCombine_TwoOfThreeAttestedCombiners_MatchSig` --- PASS (~94s)
- `TestMagnetarCombine_SignatureDivergence_HardRefusal` --- PASS (~91s)
**Residual closed for `strict-PQ` chain profile at 2026-06-01** via
`luxfi/threshold/pkg/thresholdd/magnetar.go` profile gate +
`luxfi/threshold/protocols/slhdsa-tee/pool.go` t-of-n attested-
combiner pool. Strict-PQ chains route every Combine through a
TEE-attested combiner whose binary + firmware chain-validate to the
vendor root (AMD KDS / Intel PCS / NVIDIA NRAS JWKS) --- the bytes
only ever exist inside a measured enclave. The single profile gate
`magnetarRefuseUnderStrictPQ` mirrors the precompile-side
`contract.RefuseUnderStrictPQ` discipline: ONE function, ONE place,
ONE canonical refusal sentinel
(`slhdsatee.ErrMagnetarNoTEEAttestation`, wire identifier
`ERR_MAGNETAR_NO_TEE_ATTESTATION`). The legacy-compat profile
retains the strict-atom commodity-host path verbatim; no caveat
under strict-PQ. See `SECURITY.md` for the full threat-model
statement.
(`ok github.com/luxfi/threshold/pkg/thresholdd` ~487s under `-race`.)
These gates exercise the profile refusal, attestation freshness, t-of-n
agreement, and divergence-refusal logic. They do NOT change the trust
model: the seed is reconstructed inside the enclave.
**Production attestation kinds.** Strict-PQ deployments today MUST
use SEV-SNP --- the only `cc/attest` verifier currently production-
implemented. TDX and NRAS verifiers are stubs returning
`ErrNotImplemented` (tracked at #222 stages 2--3); they wire through
the same pool contract once shipped --- no magnetar-side code change
required, only an addition to `CombinerPoolConfig.KnownIssuers`.
## FIXED --- PVSS-DKG open-reveal leak (P2)
**Pool policy defaults:** `Threshold = 2` (2-of-3 attested combiners,
no single-host quorum), `RotationWindow = 60s` (per-member
attestation freshness), `KnownIssuers = {"amd.sev.snp"}` (strict
vendor pin). Operators rotating attestations re-attest each pool
member on a per-block tick (~1s); the 60s rotation window absorbs
~60 blocks of control-plane latency before any sign would refuse.
**Status: FIXED for the production default; honest limits documented.**
**Verification gates** (all green under `-race`):
The earlier DKG ran in OPEN-REVEAL mode: `RunDKGSimulation` called
`RevealMsg()` for EVERY party, and `RevealMsg()` publishes
`PolyCoeffs[b][0] = m_i`. With every constant term public, the master
M = Σ m_i was reconstructible by ANY observer of the transcript — not
merely by t-1 colluding insiders. The "complaint-conditional reveal"
was prose only.
- `TestMagnetarCombine_StrictPQProfile_RequiresTEE` --- strict-PQ
refuses `Sign` and `Sign_Ctx`; permits `Combine_TEE` only when pool
is wired; profile flip is reversible + idempotent.
- `TestMagnetarCombine_AttestationVerified_AllowsSign` --- end-to-end
pool drive against committed AMD Milan SEV-SNP fixture; output
verifies under `magnetar.VerifyBytes` (no caller awareness of the
pool's existence).
- `TestMagnetarCombine_StaleAttestation_RejectsSign` --- members
outside rotation window refused; partial re-attestation recovers.
- `TestMagnetarCombine_TwoOfThreeAttestedCombiners_MatchSig` ---
2-of-3 attested-fresh quorum surfaces signature; 1-of-3 stops.
- `TestMagnetarCombine_SignatureDivergence_HardRefusal` --- pool
refuses byte-divergent quorum output (no silent winner-picking).
**The fix (`pvss_dkg.go`):**
**v1.0 ship state (archival).** Magnetar v1.0 routed the final FIPS
205 byte production via `circl/slhdsa.SignDeterministic` on a seed
reconstructed by the PUBLIC COMBINER (NOT a privileged aggregator).
The seed was briefly present in the public combiner's memory for one
Sign call and zeroized before return. The combiner role was PUBLIC.
- Production entry `RunDKG` emits a transcript with `Reveals == nil`:
no constant terms are published, so M is NOT reconstructible from the
transcript. `tr.RevealsMaster()` is false. Regression-gated by
`TestPVSS_DKG_ProductionTranscriptHidesMaster` (asserts production
hides M, open-reveal reveals M, and the open-reveal path refuses
without an explicit hazard ack).
- `VerifyDKGTranscript` dispatches on transcript type: the production
(no-reveal) path verifies commitment shape + setup binding and
qualifies well-shaped parties; the open-reveal path additionally
verifies shares against published reveals.
- The leaking open-reveal simulation is renamed
`RunDKGSimulationOpenRevealTestOnly` and gated behind a required
`AckOpenRevealRevealsMaster` barrier (greppable, impossible to call
by accident). It is TEST/KAT only.
This was materially stronger than a TEE-attested
privileged-aggregator model (no host in the TCB; the combiner was
a pure function any peer could run on its own substrate). v1.1
materially tightens the discipline by replacing the seed binder
with positional slices of a SHAKE-expansion buffer.
**Honest limits of the fixed production path (`RunDKG` HONEST
LIMITATIONS in code):**
### MAGNETAR-PVSS-DKG-V11 --- Leaderless PVSS-DKG for THBS-SE setup
1. **PK derivation still reconstructs M.** `pk = SLH-DSA.PK(M)` is a
hash tree over M; there is no way to derive it from shares without
reconstructing M somewhere (or TEE/MPC). `deriveDKGPublicKey`
reconstructs M transiently to compute pk and zeroizes it. M is not
published, but SOME party (whoever derives pk) holds it for an
instant. "No party EVER holds M" is achievable only via the TEE or
dealer paths. The earlier banner's "NO-MASTER-IN-MEMORY DISCIPLINE"
(naming a buffer `lagrangeScratch`) was the same proof-by-rename and
is corrected.
**Status:** CLOSED at v1.2.0. See `ref/go/pkg/magnetar/pvss_dkg.go`
for the construction, `ref/go/pkg/magnetar/key.go` for the
`NewThbsSeKeyFromDealerlessDKG` constructor,
`proofs/easycrypt/Magnetar_N5_PVSS_DKG.ec` for the EasyCrypt theory,
and `CHANGELOG.md` v1.2.0 for the release summary.
2. **No robust malicious-dealer exclusion at DKG time.** Hash
commitments are not openable without revealing m_i, so a recipient
cannot non-interactively verify a received share. The production
path therefore does NOT exclude malicious dealers at setup;
malformed shares are caught later at THBS-SE sign time (commit
binding; `TestThbsSE_RejectOversizedShareWireSize`,
`TestThbsSE_RejectTamperedShareCommitMismatch`) and via a complaint
that reveals only the disputed recipient's share value. For
adversarial committees, prefer the dealer path or the TEE pool.
**Closure shape.** A Schoenmakers-style PVSS-DKG over GF(257). Each
party i samples its own contribution m_i and a degree-(t-1)
polynomial per byte; publishes hash-based commitments to every
polynomial coefficient at Round 1; distributes shares to each
recipient via authenticated point-to-point channels; reveals the
polynomial at Round 2 alongside blinding randomness so any third
party can verify; aggregates received shares to produce its final
Shamir share. The implicit master M = sum_{i in Q} m_i mod 257
byte-wise is NEVER assembled in any party's memory at any time
during setup. The only point at which M is transiently materialised
is inside the `deriveDKGPublicKey` closure (named `lagrangeScratch`,
zeroized at closure exit) when an external auditor invokes
`VerifyDKGTranscript` to derive the public key.
Sound robust dealerless DKG would need group-homomorphic (Feldman /
Pedersen) commitments or encrypted-shares + NIZK (proper Schoenmakers
PVSS) — a separate construction, not attempted here.
**Hard invariants enforced (regression-tested):**
## OPEN --- Mechanized proofs (there are none)
- `TestPVSS_DKG_NoSinglePartyHoldsMaster` --- exercises the full DKG
and asserts no party's in-memory state contains the master, with an
AST-walk guard on `pvss_dkg.go` against master-naming.
- `TestPVSS_DKG_ByteCompatWithDealerPath` --- the dealerless share
envelopes byte-equal what the dealer path would emit for the same
implicit master.
- `TestPVSS_DKG_AdversarialReveals` --- t-1 corrupted parties cannot
recover the master from their partial-sum view.
- `TestPVSS_DKG_RobustnessAgainstMaliciousCommitments` --- malicious
parties are detected at Round 2 and excluded from Q; the protocol
terminates with valid output when |Q| >= t and fails cleanly with
`ErrPVSSQuorumLost` otherwise.
- `TestPVSS_DKG_EndToEnd_SignAndVerify` --- the closing loop: a
dealerless-DKG-produced `ThbsSeKey` flows into `ThbsSeRound1` /
`Combine` unchanged and emits a signature that verifies under
unmodified `cloudflare/circl/sign/slhdsa.Verify`.
There is NO mechanized proof of any Magnetar threshold property. The
EasyCrypt/Lean "proof track" was vacuous (a headline theorem proved by
`apply`-ing an axiom that restated it; lemmas of the form `X = X`; a CT
lemma discharged by `admit`; a PVSS secrecy "theorem" with conclusion
`true`) and has been deleted or reduced to explicitly-labeled scaffolds
that prove nothing. See `proofs/README.md` and `PROOF-CLAIMS.md`. A
genuine result (an abstract `slh_sign` model proven equal to the Go
implementation) is multi-week work and is OPEN.
**Production deployment.** Each party runs its own
`NewPVSSPartyState`, broadcasts its `PublicContribution`,
distributes its `ShareTo(j)` rows over authenticated channels, and
publishes its `RevealMsg` at Round 2. An external auditor (or any
party) collates the public-form payloads into a `PVSSTranscript` and
invokes `NewThbsSeKeyFromDealerlessDKG` to assemble the final
`ThbsSeKey`. The dealer-path `NewThbsSeKey` is retained for KAT
reproducibility and foundation-HSM bootstrap; the wire shapes match.
## OPEN --- External cryptographer audit
### MAGNETAR-PROOF-TRACK-V11 --- THBS-SE EasyCrypt + Lean track
No external audit. The internal sign-off
(`CRYPTOGRAPHER-SIGN-OFF.md`) covers only the per-validator standalone
primitive (sound) and explicitly does NOT bless the permissionless
THBS-SE path as no-leak.
**Status:** CLOSED at v1.1.0. See `proofs/easycrypt/README.md` for
the v1.1 theory inventory and `proofs/lean-easycrypt-bridge.md` for
the cross-reference table.
## OPEN --- Cross-implementation FIPS 205 byte-equality
**Theory files.** `Magnetar_N1_StrictAtom.ec` carries the headline
byte-equality theorem for the strict-atom Combine path;
`Magnetar_N1_SHAKE_Expand.ec` and `Magnetar_N1_Atom_Refinement.ec`
discharge the supporting refinements; `lemmas/SLHDSA_Functional.ec`
and `lemmas/Magnetar_CT.ec` provide the FIPS 205 SHAKE primitive
definitions + CT lemma. Lean side at
`proofs/lean/Crypto/Magnetar/StrictAtom.lean`.
**Axiom budget.** 5 substantive admits + 1 abstract-vacuous CT
admit. Cross-cites Pulsar Shamir (Lean) and Lux SHA3 (Lean) for the
algebraic content.
### MAGNETAR-DUDECT-V11 --- v1.1 dudect harness
**Status:** CLOSED at v1.1.0. See `ct/dudect/README.md` for the
methodology + Go-side gate.
**Per-push gate.** `ct/dudect/strict_atom_combine_ct_test.go::
TestStrictAtom_CT_NoSecretDependentBranch` (build tag `ct`) walks
the strict-atom emit path's AST and asserts no secret-tagged
identifier feeds an `if` / `switch` condition or an index
expression. Run via `scripts/checks/dudect-smoke.sh`.
**Release-time gate.** The full dudect statistical test on a
compiled harness is documented in `ct/dudect/README.md` and is
release-time only.
### MAGNETAR-EXTERNAL-AUDIT-V11 --- External cryptographer review
**Status:** OPEN. Scope: v1.1 / post-v1.1.
The v0.x internal cryptographer sign-off applies to the v0.x
construction surface, much of which has been removed. The v1.1
external audit should target the THBS-SE construction shape, the
strict-atom-assembly path, and the leaderless PVSS-DKG setup, all
of which land at v1.1.
## v1.3 / v1.4 work items (proposed 2026-06-03 audit)
### MAGNETAR-GPU-PORT-V13 --- Batched FIPS 205 hash-tree GPU kernels
**Status:** PROPOSED. Scope: v1.3.
Land four batched SHAKE256-based kernels at
`lux-private/gpu-kernels/ops/crypto/slhdsa/` and wire through
`luxcpp/gpu` to the magnetar `slhSignAtom` substrate. Kernels:
- `magnetar_wotsplus_chain_batch` --- FIPS 205 §5 chain
(CPU `wotsChain`).
- `magnetar_fors_subtree_batch` --- FIPS 205 §8.2 FORS subtree
(CPU `forsNodeCompute`).
- `magnetar_xmss_subtree_batch` --- FIPS 205 §6.1 XMSS subtree
(CPU `xmssNodeCompute`).
- `magnetar_hmsg_prfmsg_batch` --- FIPS 205 §11.2 SHAKE H_msg /
PRF_msg (CPU `hMsgPub` and `prfMsg` callback).
Full design + throughput estimates + 5-backend file layout
in `GPU-PORT-PLAN.md`.
Consumers: high-throughput bridge custody signing, N=100+
aggregate-cert verification, slashing-evidence sweep across
historical blocks. NOT required for consensus-rate signing
(~1 sig/block CPU-bound on commodity hardware is sufficient).
### MAGNETAR-PROACTIVE-RESHARE-V13 --- Zero-secret refresh
**Status:** PROPOSED. Scope: v1.3.
Augment the PVSS-DKG with proactive resharing against the same
group public key. Lifts the static-corruption bound to a
refresh-window-bounded adaptive-corruption bound. Share envelope
shape is forward-compatible; no wire break.
### MAGNETAR-APPLE-SE-HSM-V14 --- Apple Keychain SE-only hsm.Provider
**Status:** PROPOSED. Scope: v1.4.
`hsm.Provider` implementation backed by Apple Keychain with
`kSecAttrAccessControl = kSecAccessControlSecureEnclaveOnly`.
Tests can mock; production Apple Silicon hosts get a first-class
HSM substrate that layers BELOW the attestation chain (the
Apple SE is NOT a substitute for SEV-SNP / TDX / NRAS
attestation, it is the at-rest seed wrap).
Byte-equality is checked only against `cloudflare/circl`. A cross-check
against an independent FIPS 205 reference (pq-crystals C, BoringSSL
when SLH-DSA lands) is a tracked gap (not yet done).
## Cross-references
- v1.0 construction spec: `THBS-SPEC.md`
- v1.0 normative spec: `SPEC.md`
- v1.0 proof track: `proofs/README.md`
- v1.0 CT track: `ct/README.md`
- v1.0 release notes: `CHANGELOG.md` v1.0.0 entry
- v1.2 audit: `AUDIT-2026-06.md`
- v1.3 TEE integration spec: `TEE-INTEGRATION.md`
- v1.3 GPU port plan: `GPU-PORT-PLAN.md`
- `README.md`, `DESIGN.md` --- construction overview.
- `ASSEMBLE-INVARIANT.md` --- what the THBS-SE Combine path does.
- `PROOF-CLAIMS.md` --- per-property proven/asserted/open breakdown.
- `TEE-INTEGRATION.md` --- TEE-attested production surface spec.
- `CHANGELOG.md` --- release history.
CRYPTOGRAPHER-SIGN-OFF.md
+71 -94
View File
@@ -1,121 +1,98 @@
# Cryptographer sign-off --- luxfi/magnetar v1.0.0
# Cryptographer sign-off --- luxfi/magnetar
Independent review of the Magnetar SLH-DSA implementation at `main`
of `github.com/luxfi/magnetar` at tag `v1.0.0`. Date of review:
2026-05-31. Reviewer: cryptographer agent (internal review).
Internal review of the Magnetar SLH-DSA implementation at `main` of
`github.com/luxfi/magnetar`. Reviewer: cryptographer agent (internal).
## Summary
**APPROVED WITH OPEN ITEMS** for production deployment of the
per-validator standalone primitive and for the THBS-SE
permissionless threshold construction under the threat model
documented in `DEPLOYMENT-RUNBOOK.md` sec 2.1. The v1.0.0 review
covers:
**APPROVED for the per-validator standalone primitive only.** The
threshold paths are NOT blessed as no-leak.
- **Per-validator standalone**
(`ref/go/pkg/magnetar/standalone.go`) --- the public-BFT primary
primitive. APPROVED for production. The construction is a thin
wrapper around `cloudflare/circl/sign/slhdsa` v1.6.3 FIPS 205
SignDeterministic; the wire-identity claim
(TestMagnetar_Wire_FIPS205Verifiable) passes across all 3 SHAKE
modes. The aggregate-cert verifier has explicit
unknown-validator + pubkey-mismatch handling and parallel-CPU
dispatch with observable provenance via
`LastValidatorBatchTier`.
- **Per-validator standalone** (`standalone.go`): **APPROVED for
production.** A thin, sound wrapper over
`cloudflare/circl/sign/slhdsa` FIPS 205 SignDeterministic. No shared
seed, no DKG, no reconstruction. Wire identity
(`TestMagnetar_Wire_FIPS205Verifiable`) passes across all 3 SHAKE
modes. The aggregate-cert verifier handles unknown-validator +
pubkey-mismatch and parallel-CPU dispatch with observable provenance.
- **THBS-SE** (`ref/go/pkg/magnetar/thbsse.go` + `thbsse_field.go`)
--- the permissionless threshold companion. APPROVED for the
documented threat model (public combiner, anyone-can-combine,
no host in TCB at sign time). The 8 mandated test gates pass:
TestThbsSE_Wire_FIPS205Verifiable (3 modes),
TestThbsSE_RejectSeedReveal, TestThbsSE_RejectUnselectedFORS,
TestThbsSE_RejectUnselectedWOTS, TestThbsSE_SlotReuseRejected,
TestThbsSE_OverselectedCommittee,
TestThbsSE_SlotBindingDomainSeparation, and
BenchmarkThbsSE_Sign_5of7 (192f at < 100 ms/op on Apple M1 Max).
The KAT replay (TestKAT_ThbsSe) is deterministic at
(n=7, t=4) x 3 modes x 3 messages.
- **TEE-attested combiner pool** (`luxfi/threshold/protocols/slhdsa-tee`):
**APPROVED under an explicit attested-hardware trust model.** The
seed is reconstructed inside a measured enclave on t hosts that must
agree. This is trust-relocation (adds a host to the TCB), NOT MPC.
The five `TestMagnetarCombine_*` gates build and pass under `-race`
after the `luxfi/zap` v0.3.1 bump in `luxfi/threshold`.
## Honest open items (v1.1)
- **Permissionless THBS-SE** (`thbsse.go`, `thbsse_assemble.go`): **NOT
APPROVED as a no-leak / no-host-in-TCB primitive.** The public
combiner RECONSTRUCTS the full FIPS 205 master every signature
(`ASSEMBLE-INVARIANT.md`). It is RESEARCH-GRADE. It may be used where
the combiner host is trusted by deployment policy, but it must not be
presented as keeping the seed secret from the combiner. The byte
identity to single-party FIPS 205 is a correctness/interop property,
not a confidentiality one.
1. **MAGNETAR-STRICT-ATOM-V11** --- The strictest formulation of
the THBS-SE invariant ("no party or combiner EVER reconstructs
SK.seed, even transiently in memory") requires a v1.1
strict-atom-assembly path. v1.0 ships a PUBLIC COMBINER that
holds the seed for the duration of one
`slhdsa.SignDeterministic` call and zeroizes. This is materially
stronger than a TEE-attested privileged-aggregator model (no host
in TCB) and materially weaker than the strict invariant (a
peer-local memory-disclosure adversary at the precise sub-second
combine moment could observe the seed). See
`BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11`.
## Open items (corrected)
2. **MAGNETAR-PVSS-DKG-V11** --- v1.0 ships a deterministic-dealer
setup (`NewThbsSeKey`). Production deployments needing the
leaderless PVSS-DKG variant route through the sibling
`luxfi/threshold` DKG package; the share envelope is
wire-equivalent. See
`BLOCKERS.md::MAGNETAR-PVSS-DKG-V11`.
1. **MAGNETAR-STRICT-ATOM --- OPEN (was falsely marked CLOSED).** The
"strict-atom" Combine does NOT eliminate seed reconstruction; it
renames the buffer. The earlier sign-off's claim that v1.0/v1.1 was
"materially stronger than a TEE-attested model (no host in TCB)" was
wrong: whoever runs the public combiner sees the seed, so there IS a
host in the TCB at sign time. Closing this needs full MPC over the
SHAKE hash tree (open research) or the TEE pool. See `BLOCKERS.md`.
3. **MAGNETAR-PROOF-TRACK-V11** --- The legacy EasyCrypt
scaffolding modeling the abandoned v0.x seed-recombine path has
been removed. The v1.0 proof track ports to the THBS-SE
construction shape; full EC + Lean coverage lands at v1.1. See
`BLOCKERS.md::MAGNETAR-PROOF-TRACK-V11`.
2. **PVSS-DKG open-reveal leak --- FIXED.** The earlier DKG published
every party's constant term, making the master reconstructible by
any observer. The production path (`RunDKG`) now publishes no
reveals; `TestPVSS_DKG_ProductionTranscriptHidesMaster` gates it.
Honest residual limits: pk derivation still reconstructs the master
(inherent), and the production path does not robustly exclude
malicious dealers at DKG time. See `BLOCKERS.md` (P2).
4. **MAGNETAR-DUDECT-V11** --- v1.0's CT story is "inherit CIRCL"
(`ct/README.md`). The v1.1 dudect harness lands alongside the
strict-atom-assembly path. See
`BLOCKERS.md::MAGNETAR-DUDECT-V11`.
3. **Mechanized proofs --- NONE.** The earlier EC/Lean track was
vacuous (a headline theorem proved by `apply`-ing an axiom that
restated it; `X = X` lemmas; a CT lemma by `admit`; a PVSS secrecy
"theorem" with conclusion `true`). It has been deleted or reduced to
labeled scaffolds. There is no mechanized refinement, present or on
a credible near-term path. See `PROOF-CLAIMS.md` §2.
5. **MAGNETAR-EXTERNAL-AUDIT-V11** --- The v0.x internal sign-off
applied to the v0.x construction surface, much of which has been
removed at v1.0. The v1.1 external audit should target the
THBS-SE construction shape, the strict-atom-assembly path, and
the leaderless PVSS-DKG setup. See
`BLOCKERS.md::MAGNETAR-EXTERNAL-AUDIT-V11`.
4. **dudect / statistical CT --- OPEN.** Only local CT helpers + code
review. The "CT" AST test is a name lint, not a timing measurement
(and CT is moot for a path holding the master in plaintext).
## What changed since v0.5.x
5. **External audit --- OPEN.**
The full v1.0 changeset is in `CHANGELOG.md::[1.0.0]`. The
load-bearing deletions:
## What changed since v0.x
- `threshold.go`, `aggregate.go`, `combine.go`, `shamir.go`,
`dkg.go` and their tests --- the legacy seed-recombine threshold
path.
- `pkg/thbs/` (entire subtree) --- the legacy true-HBS path
including the `dkg2/` PVSS skeleton.
- `vectors/threshold-sign.json`, `vectors/dkg.json` --- legacy KATs.
- `jasmin/threshold/`, `jasmin/lib/` --- legacy Jasmin model.
- `proofs/easycrypt/` (entire tree) --- legacy EC theories.
- `ct/dudect/` (entire tree) --- legacy dudect harness.
The load-bearing v1.0 deletions (recorded for provenance): the v0.x
seed-recombine threshold files `threshold.go`, `aggregate.go`,
`combine.go`, `shamir.go`, `dkg.go` and their tests; `pkg/thbs/`; the
legacy KATs; the legacy Jasmin model; the legacy EC tree; the legacy
dudect harness. The current code lives in `thbsse.go`,
`thbsse_field.go`, `thbsse_assemble.go`, `slhdsa_internal.go`,
`standalone.go`, `pvss_dkg.go`, `key.go`.
The load-bearing additions:
- `ref/go/pkg/magnetar/thbsse.go` + `thbsse_field.go` --- the
THBS-SE construction.
- `ref/go/pkg/magnetar/thbsse_test.go` --- the 8 mandated test
gates plus 2 bonus correctness checks.
- `vectors/thbsse-sign.json` --- deterministic KAT vectors at
(n=7, t=4) x 3 modes x 3 messages.
The THBS-SE gates are `TestThbsSE_Wire_FIPS205Verifiable`,
`TestThbsSE_RejectSeedReveal`, `TestThbsSE_RejectOversizedShareWireSize`,
`TestThbsSE_RejectTamperedShareCommitMismatch`,
`TestThbsSE_SlotReuseRejected`, `TestThbsSE_OverselectedCommittee`,
`TestThbsSE_SlotBindingDomainSeparation`. (The last two reject-tests
were formerly mis-named ...UnselectedFORS / ...WOTS; THBS-SE shares the
whole seed, so they test commit binding, not atom selection.)
## Verification commands
```bash
cd ref/go && GOWORK=off go build ./...
cd ref/go && GOWORK=off go vet ./...
cd ref/go && export PATH="$(go env GOPATH)/bin:$PATH" && staticcheck ./...
cd ref/go && GOWORK=off go test -count=1 -short -timeout 600s ./pkg/magnetar/...
cd ref/go && GOWORK=off go test -count=1 -race -short -timeout 600s ./pkg/magnetar/...
cd ref/go && GOWORK=off go test -bench=BenchmarkThbsSE_Sign_5of7 -benchtime=2x ./pkg/magnetar/...
```
All clean as of v1.0.0 sign-off.
## Recommendation
**TAG `v1.0.0`** for the per-validator standalone primitive and for
THBS-SE under the documented threat model. Track the 5 open items
above against the v1.1 milestone. Operator-controlled MPC custody
(M-Chain bridge, A-Chain confidential compute) remains the domain of
the sibling `luxfi/threshold` package's TEE-attested variants and is
explicitly out of scope for this primitive.
Ship the per-validator standalone primitive as the production default.
Ship the TEE pool as opt-in for trusted-hardware custody, under the
honest trust-relocation framing. Keep THBS-SE labeled RESEARCH-ONLY; do
not present it as no-leak. Track the open items in `BLOCKERS.md`.
DEPLOYMENT-RUNBOOK.md
+4 -3
View File
@@ -9,10 +9,11 @@ Magnetar v1.0 ships **TWO distinct signing primitives** with
different trust models. Picking the wrong one is the single largest
deployment risk.
| Primitive | Trust model | Public-BFT safe | Use case |
| Primitive | Trust model | No-leak / sound | Use case |
|---|---|---|---|
| `ValidatorSign` + `VerifyAggregateCert` (per-validator standalone, `standalone.go`) | Per-validator standalone keys, no shared seed | YES | **Lux public-BFT validator quorum (PRIMARY)** |
| `NewThbsSeKey` + `ThbsSeRound1` + `Combine` (THBS-SE, `thbsse.go`) | t-of-n committee, public combiner, no host in TCB | YES (with v1.0 open item) | Permissionless threshold signing for single-signature certificates |
| `ValidatorSign` + `VerifyAggregateCert` (per-validator standalone, `standalone.go`) | Per-validator standalone keys, no shared seed, NO reconstruction | YES (SOUND) | **Lux public-BFT validator quorum (PRODUCTION DEFAULT)** |
| TEE-attested combiner pool (`luxfi/threshold/protocols/slhdsa-tee`) | Seed reconstructed INSIDE a measured enclave on t hosts; trust-relocation (adds a host to the TCB), NOT MPC | YES under attested-hardware trust | Opt-in custody / single-signature certificates |
| `NewThbsSeKey` + `ThbsSeRound1` + `Combine` (THBS-SE, `thbsse.go`) | t-of-n committee, public combiner that **RECONSTRUCTS the full FIPS 205 master every signature** | NO --- RESEARCH-GRADE; whoever runs Combine sees the seed (a host IS effectively in the TCB) | Permissionless threshold ONLY where the combiner host is trusted by policy. NOT no-leak. |
### Quick decision
DESIGN.md
+97 -105
View File
@@ -1,130 +1,122 @@
# Magnetar --- Public-DKG MPC Threshold SLH-DSA (research profile)
# Magnetar --- design
> **v1.0 framing.** This document is a v0.x research-profile design
> snapshot. The v1.0 production THBS-SE construction
> (`THBS-SPEC.md`) is the closer of "permissionless threshold SLH-DSA
> without TEE" for Magnetar; the v1.1 strict-atom-assembly path is
> the strict-invariant closer (`BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11`).
Magnetar is the hash-based (FIPS 205 SLH-DSA) PQ leg of the Lux
cross-family signature suite. This document states the architecture and
why each path exists.
> **Tier 3 of the Hanzo PQ Threshold Suite.** Research-track
> construction for threshold FIPS 205 SLH-DSA via MPC. **NOT
> production-ready. NOT part of the v0.1 NIST MPTC submission.**
## The fundamental constraint
## What this document is
SLH-DSA is a tree of hash computations: the secret is a SHAKE seed and
signing traverses a hypertree of one-time / few-time signatures keyed
by that seed. There is NO linear-aggregation identity (unlike
FROST/Schnorr or the Raccoon-style ML-DSA threshold). The literature is
explicit:
A placeholder + design-direction sketch for a future research-grade
public-DKG threshold construction over FIPS 205 SLH-DSA. The Hanzo
PQ Threshold Suite includes Magnetar to signal architectural intent
without overclaiming maturity.
- Cozzo & Smart, EUROCRYPT 2019, *Sharing the LUOV*: every internal
SHAKE/SHA-2 evaluation is a non-linear function of the secret seed.
- Bonte, Smart & Tan, 2023, *Threshold SPHINCS+*: there is no efficient
t-of-n SLH-DSA scheme producing one FIPS 205-shaped signature without
either (a) reconstructing the seed in some combiner process, or (b)
full MPC over the SHAKE hash tree (multi-second, multi-megabyte per
signature).
- NIST IR 8214: SLH-DSA is the highest threshold-MPC cost among FIPS
20{3,4,5}.
## What this document is NOT
True no-reconstruction threshold SLH-DSA is OPEN RESEARCH. Magnetar
does not pretend otherwise. Instead it offers three paths chosen by
deployment model.
- Not a specification. The protocol is unfixed.
- Not a security claim. The protocol has not been analyzed.
- Not an implementation. No `ref/go/`-equivalent exists for Magnetar.
- Not a NIST submission. Submitting threshold SLH-DSA as if it
were standardized would be inaccurate.
## The three paths
## Why Magnetar exists conceptually
### 1. Per-validator standalone --- PRODUCTION DEFAULT (sound)
SLH-DSA is hash-based and stateless (FIPS 205). Its security rests
on different assumptions from ML-DSA: collision/preimage resistance
of the underlying hash (SHA-2 or SHAKE), with no lattice
assumption.
`standalone.go`. Each validator holds its own FIPS 205 keypair, signs
the message independently, and the consensus layer collects N
single-party signatures into a `ValidatorAggregateCert`. Verification
counts valid signatures against the validator-set registry; the quorum
decision lives at the consumer.
A threshold profile of SLH-DSA gives a defense-in-depth signature:
even if ML-DSA's lattice assumption is broken in the future,
Magnetar's hash-based threshold provides a fallback.
This is the sound primitive: there is no shared seed, no DKG, no
dealer, and no reconstruction anywhere. It sidesteps both (a) and (b)
by emitting N independent signatures. Wire size is N x |sigma| (a
Z-Chain Groth16 rollup compresses it; separate primitive).
## Why this is hard
THIS IS THE DOCUMENTED PRODUCTION PRIMITIVE for public-BFT post-quantum
consensus.
Unlike threshold schemes for discrete-log-style or lattice-based
signatures, SLH-DSA does NOT decompose into a linear-aggregation
identity. The signing process is a tree of hash computations
(Merkle tree of hash-based one-time signatures), where the
"secret" is a SHAKE seed and "signing" involves traversing the
tree based on the message hash.
### 2. TEE-attested combiner pool --- OPT-IN PRODUCTION (sound under attested-hardware trust)
Threshold SLH-DSA constructions in the literature typically require:
- MPC over hash computations (slow; SHAKE computed inside MPC).
- Distributed seed generation with VSS.
- Per-signature MPC ceremony.
`luxfi/threshold/protocols/slhdsa-tee`. For deployments that genuinely
need a SINGLE FIPS 205-shaped signature from a committee (custody,
bridge signing), Magnetar routes Combine through a t-of-n
attested-combiner pool, gated by the single profile function
`magnetarRefuseUnderStrictPQ`.
None of these match the elegance of FROST-style aggregation that
Pulsar uses for ML-DSA. Magnetar is a research-grade direction,
not an obvious specification target.
Honest trust model: the seed is reconstructed in full, but INSIDE a
measured enclave whose binary + firmware chain-validate to a vendor
root (AMD KDS today; Intel TDX / NVIDIA NRAS are stubs). This is
TRUST-RELOCATION --- it moves the reconstruction into attested hardware
and ADDS that hardware (plus the attestation chain and the t hosts) to
the TCB. It is NOT MPC and does NOT keep the seed secret from every
party; the enclave sees it.
## Suggested research direction
### 3. Permissionless THBS-SE --- RESEARCH-ONLY
1. **Distributed seed generation**: Lux-style Pedersen-VSS over
the SHAKE seed space (32 or 64 bytes for FIPS 205 SHAKE
profiles).
`thbsse.go` + `thbsse_field.go` + `thbsse_assemble.go` +
`slhdsa_internal.go`. A t-of-n committee, slot-bound commit-and-reveal,
and an anyone-can-combine public combiner. The public combiner
RECONSTRUCTS the full FIPS 205 master into one buffer every signature
(`ASSEMBLE-INVARIANT.md`) and emits a byte-identical FIPS 205
signature.
2. **Per-signature MPC**: a multi-party Generic-Group-Model
ceremony to compute the SLH-DSA signature components without
any single party reconstructing the seed.
Because whoever runs Combine sees the seed, there is effectively a host
in the TCB at sign time. This path is RESEARCH-GRADE. It must not be
presented as production or as "no host in the TCB". The earlier "strict
-atom Combine closed the no-leak gap" claim was proof by rename (it
avoids the variable name `seed`, not the reconstruction). See
`BLOCKERS.md::MAGNETAR-STRICT-ATOM` (OPEN).
3. **Hash precomputation amortization**: precompute layers of the
FORS / W-OTS+ Merkle tree in batched MPC sessions to amortize
the per-signature ceremony cost.
## Setup: dealer, dealerless, or TEE
4. **Identifiable abort**: same TLV-encoded evidence format as
Pulsar §10, with per-MPC-round per-party state.
- **Dealer (`NewThbsSeKey`)**: one machine samples the master,
byte-shares it over GF(257), and zeroizes it. The dealer is in the
TCB for setup only. KAT-reproducible; recommended for foundation-HSM
bootstrap.
- **Dealerless production (`RunDKG`)**: per-party PVSS with hash
commitments; the transcript carries NO constant-term reveals, so the
master is not reconstructible from the wire. BUT pk derivation
reconstructs the master transiently (inherent: `pk = SLH-DSA.PK(M)`
is a hash tree over M), and the path does NOT robustly exclude
malicious dealers at DKG time (hash commitments aren't openable
without revealing m_i). See `RunDKG` HONEST LIMITATIONS in
`pvss_dkg.go`.
- **TEE**: routes both pk derivation and Combine through attested
hardware (trust-relocated).
5. **Public-key preservation across resharing**: standard
zero-secret-refresh applied to the SHAKE seed shares.
A leaking open-reveal DKG (`RunDKGSimulationOpenRevealTestOnly`) exists
for KAT replay only, behind an explicit hazard acknowledgement; its
transcript reveals the master.
## Parameter-set candidates
## Parameter sets (FIPS 205 SHAKE)
If the research direction matures into a specification, the
following parameter sets are candidates (matching FIPS 205 §4):
| Mode | NIST Category | sig bytes |
|---|---|---|
| SHAKE-192s | 3 | 16224 (recommended) |
| SHAKE-192f | 3 fast | larger sig, faster sign |
| SHAKE-256s | 5 | 29792 |
| Identifier | NIST Category | sig bytes | Notes |
|---|---|---|---|
| `MAGNETAR-THRESHOLD-SLH-DSA-SHAKE-128s` | 1 | 7856 | small/slow |
| `MAGNETAR-THRESHOLD-SLH-DSA-SHAKE-192s` | 3 | 16224 | RECOMMENDED if Magnetar matures |
| `MAGNETAR-THRESHOLD-SLH-DSA-SHAKE-256s` | 5 | 29792 | high security |
SLH-DSA signatures are large (16-30 KB) vs ML-DSA (2-5 KB); the
per-signature cost dominates economics, which is another reason the
standalone path (no MPC ceremony) is the production default.
Note that SLH-DSA signatures are LARGE compared to ML-DSA
(7-30 KB vs 2-5 KB). The per-signature MPC cost will dominate
deployment economics.
## What is NOT claimed
## Why we do not ship Magnetar in v0.1
- No mechanized proof of any threshold property (the prior EC/Lean
track was vacuous; see `PROOF-CLAIMS.md`).
- No no-leak property for THBS-SE.
- No robust-against-malicious-dealers property for the production DKG.
- No external audit.
1. **No mature construction**: published threshold-SLH-DSA work is
limited and not well-reviewed.
2. **MPC complexity**: per-signature MPC dwarfs the per-signature
cost of Pulsar.
3. **Signature size**: 7-30 KB per signature is operationally
expensive on-chain.
4. **Standardization status**: NIST has not signalled threshold
SLH-DSA as a near-term MPTC target.
Magnetar will be re-evaluated for v0.2-v0.4 submission consideration
based on community / NIST direction.
## Honest framing for users
> Magnetar is the **research-track** member of the Hanzo PQ
> Threshold Suite. It is intended for paranoid scenarios where
> ML-DSA's lattice security assumption is broken in the future and
> a hash-based fallback is needed. It is NOT recommended for
> production use today. Use **Pulsar (Tier 1)** for production
> threshold post-quantum signing.
## Contact
For research collaboration on Magnetar:
- Email: `magnetar@lux.network`
- Public discussion:
<https://github.com/luxfi/pulsar/discussions> (label: `magnetar`)
---
**Document metadata**
- Name: `docs/magnetar.md`
- Version: v0.1 (placeholder)
- Date: 2026-05-18
- Status: **Research direction, not specification.** No production
use. No NIST submission claim.
Use the per-validator standalone path for production public-BFT
signing. Use the TEE pool when you are willing to trust attested
hardware. Treat THBS-SE as research.
PROOF-CLAIMS.md
+91 -292
View File
@@ -1,311 +1,110 @@
# PROOF-CLAIMS --- Magnetar (HONEST framing)
# PROOF-CLAIMS --- Magnetar (HONEST: proven vs asserted vs open)
> **v1.0 framing.** This document is a v0.x archival snapshot. The
> v1.0 proof track ports to the THBS-SE construction shape and lands
> at v1.1 (see `BLOCKERS.md::MAGNETAR-PROOF-TRACK-V11` and
> `proofs/README.md`).
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.
> **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.
## §0 One-paragraph truth
## §1 The narrow claim Magnetar makes at this submission
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.
The strongest precise statement supported by Magnetar v0.3.0:
## §1 Per-property status
> **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 |
| Property | Status | Basis |
|---|---|---|
| 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) |
| 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. |
## §3 What is NOT proved (HONEST)
## §2 The deleted/scaffolded "proof track" (HONEST accounting)
This section is the load-bearing honesty disclosure. Read it.
The earlier submission advertised a mechanized EasyCrypt + Lean track
with a small "admit budget". Every result in it was vacuous:
### §3.1 NOT proved: mechanized refinement of the threshold overlay
- `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.**
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.
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`.
**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.
## §3 What the trust base reduces to (no mechanization)
**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.
For correctness/interop:
**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:
- 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`.
- 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.
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.
### §3.2 NOT proved: post-quantum hardness of SLH-DSA
## §4 What an auditor should do
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.
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.
**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.
## §5 Open items (tracked)
**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 |
| Item | Status |
|---|---|
| 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
| 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 |
README.md
+89 -71
View File
@@ -1,16 +1,22 @@
# Magnetar v1.2 --- SLH-DSA (FIPS 205) for Lux
# Magnetar --- SLH-DSA (FIPS 205) for Lux
Magnetar v1.2 ships ONE construction surface to each of the two
deployment regimes Lux ecosystem chains need, with the strict-atom
Combine path closing `MAGNETAR-STRICT-ATOM-V11` and the dealerless
PVSS-DKG closing `MAGNETAR-PVSS-DKG-V11`:
Magnetar is the hash-based PQ leg. SLH-DSA has no aggregatable
structure, so the SOUND production primitive is per-validator
standalone (N independent signatures); the threshold variants either
relocate trust into attested hardware (TEE pool) or are research-grade
(permissionless THBS-SE, which reconstructs the master at the public
combiner).
| Regime | Construction | Where it lives |
|---|---|---|
| Public-BFT consensus on Lux L1/L2 (mainnet, testnet, devnet, white-label) | **Per-validator standalone** --- each validator holds its own FIPS 205 keypair, signs independently, consensus collects N signatures into a `ValidatorAggregateCert` | `ref/go/pkg/magnetar/standalone.go` |
| Permissionless t-of-n threshold for verifier-side single-signature certificates | **THBS-SE (strict-atom Combine)** --- t-of-n committee, slot-bound commit-and-reveal, anyone-can-combine public combiner, Magnetar-internal FIPS 205 sec 5--sec 8 walk with no named transient seed binder | `ref/go/pkg/magnetar/thbsse.go` + `thbsse_field.go` + `thbsse_assemble.go` + `slhdsa_internal.go` |
| Regime | Construction | Posture | Where |
|---|---|---|---|
| **Public-BFT consensus (DEFAULT, production)** | **Per-validator standalone** --- each validator holds its own FIPS 205 keypair, signs independently, consensus collects N signatures into a `ValidatorAggregateCert` | SOUND. No DKG, no dealer, no reconstruction. | `standalone.go` |
| **Trusted-hardware / custody (opt-in, production)** | **TEE-attested combiner pool** | SOUND under an honest trust model: the seed is reconstructed inside a measured enclave on t hosts that must agree --- trust-relocation (adds a host to the TCB), NOT MPC. | `luxfi/threshold/protocols/slhdsa-tee` |
| **Permissionless t-of-n threshold** | **THBS-SE** --- t-of-n committee, slot-bound commit-and-reveal, anyone-can-combine public combiner | RESEARCH-ONLY. The public combiner RECONSTRUCTS the full FIPS 205 master every signature (`ASSEMBLE-INVARIANT.md`). NOT no-leak. | `thbsse.go`, `thbsse_field.go`, `thbsse_assemble.go`, `slhdsa_internal.go` |
Both produce FIPS 205 wire bytes that an unmodified verifier accepts.
All three produce FIPS 205 wire bytes that an unmodified verifier
accepts. That is a correctness/interop property; it says nothing about
confidentiality. See `BLOCKERS.md` for the sound/open/falsely-closed
breakdown.
## Per-validator standalone (public-BFT primary)
@@ -49,14 +55,17 @@ the function returns, no party (including the dealer) holds the
master. Recommended for foundation-HSM single-host bootstrap and
KAT replay.
**Dealerless PVSS-DKG setup (no trusted dealer).** Each committee
party runs `NewPVSSPartyState` independently, publishes a
`PublicContribution` (per-coefficient hash commitments only),
distributes private share rows over authenticated channels, and
publishes a `RevealMsg` at Round 2. Any third party collates the
**Dealerless PVSS-DKG setup (`RunDKG`).** Each committee party runs
`NewPVSSPartyState` independently, publishes a `PublicContribution`
(per-coefficient hash commitments only), and distributes private share
rows over authenticated channels. The PRODUCTION path (`RunDKG`)
publishes NO constant-term reveals, so the master is not
reconstructible from the transcript. Any third party collates the
public payloads into a `PVSSTranscript` and invokes
`NewThbsSeKeyFromDealerlessDKG` to assemble the canonical
`ThbsSeKey`:
`NewThbsSeKeyFromDealerlessDKG` to assemble the canonical `ThbsSeKey`.
(A separate `RunDKGSimulationOpenRevealTestOnly`, gated behind an
explicit hazard ack, runs the leaking open-reveal mode for KAT replay
only.):
```go
// Each party i runs in its own process.
@@ -77,41 +86,37 @@ key, _ := magnetar.NewThbsSeKeyFromDealerlessDKG(transcript)
// implicit master M = sum_{i in Q} m_i mod 257 byte-wise.
```
The dealerless path enforces the hard invariant: **no party (and no
transient dealer) ever holds the master byte vector at any time
during setup**. The implicit master is only materialised inside the
`deriveDKGPublicKey` closure (named `lagrangeScratch`, zeroized at
closure exit) when an auditor invokes `VerifyDKGTranscript` to
derive the public key.
**What the production dealerless path guarantees (and what it does
not).** The `RunDKG` transcript carries no constant-term reveals, so
the master is not reconstructible from the transcript by observers.
It does NOT make "no party ever holds the master" true: deriving the
group public key needs `pk = SLH-DSA.PK(M)` (a hash tree over M), so
`deriveDKGPublicKey` reconstructs M transiently at whoever derives pk
and zeroizes it. That reconstruction is inherent (TEE/MPC only avoid
it). Naming the buffer `lagrangeScratch` is not a security property.
See `BLOCKERS.md` (P2) and `RunDKG`'s HONEST LIMITATIONS in
`pvss_dkg.go`. The production path also does NOT robustly exclude
malicious dealers at DKG time (hash commitments aren't openable
without revealing m_i); malformed shares are caught at sign time.
For reference, the `RunDKGSimulation` helper runs the full n-party
protocol in a single test process (every party's state in one heap)
for KAT replay and benchmark purposes; production deployments should
run each party in its own process.
`RunDKGSimulationOpenRevealTestOnly` runs the full n-party protocol in
one process in open-reveal mode for KAT replay only; it requires an
explicit hazard ack and its transcript REVEALS the master.
**Hard invariant** (THBS-SE construction): a revealed value is allowed
ONLY if it is also present in the final SLH-DSA signature.
**THBS-SE reveal discipline.** A revealed value is the per-round mask
`r_i`, the masked share `s'_i = share_i XOR r_i`, the public commit
hash, and the final signature. The share envelope is per-slot and the
slot guard refuses same-slot re-emission.
- ALLOWED reveals: the per-round mask `r_i`, the masked share
`s'_i = share_i XOR r_i`, the public commit hash, the final FIPS
205 signature bytes.
- FORBIDDEN reveals: `SK.seed` in any party-local persistent form;
`SK.prf`; future-slot share material. The slot guard refuses any
same-slot re-emission, and the share envelope is per-slot.
**No-aggregator property**: The public combiner is a PURE function of
its inputs. Any peer --- validator, block proposer, RPC node, passive
watcher --- can run Combine. There is no privileged aggregator role
and no host in the TCB at sign time. (The strict-atom Combine path
at v1.1 closed the residual transient-seed-at-combiner gap; see
`BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11` for the closure summary.)
**No-trusted-dealer property**: The PVSS-DKG setup path
(`NewThbsSeKeyFromDealerlessDKG`, v1.2) eliminates the trusted
dealer from setup. No party (and no transient dealer) ever holds
the master byte vector at any time during setup. See
`BLOCKERS.md::MAGNETAR-PVSS-DKG-V11` for the closure summary and
`pvss_dkg.go` for the construction.
**The public combiner reconstructs the master.** Any peer can run
Combine (it is a pure function of public inputs), but it RECONSTRUCTS
the full FIPS 205 master into `derivedMaterial` to produce the
signature (`ASSEMBLE-INVARIANT.md`). So there IS effectively a host in
the TCB at sign time: whoever runs Combine sees the seed. This is why
the permissionless THBS-SE path is research-grade. The earlier claim
that the "strict-atom Combine closed the transient-seed gap" was proof
by rename (it avoids the variable name `seed`, not the reconstruction);
see `BLOCKERS.md::MAGNETAR-STRICT-ATOM` (OPEN).
**Slot binding**: every signature is bound to
`(chain_id, epoch, slot, height, committee_id, message_domain)`. The
@@ -146,21 +151,26 @@ FROST-style linear share-aggregation. The literature confirms:
full MPC over the SHA-256/SHAKE hash tree (multi-second per
signature, multi-megabyte of comms).
THBS-SE chooses (a) with a PUBLIC COMBINER --- anyone-can-combine,
no host in TCB. The per-validator standalone path sidesteps (a) and
(b) entirely by emitting N independent signatures.
THBS-SE chooses (a) with a PUBLIC COMBINER. "Anyone can combine", but
whoever does RECONSTRUCTS the seed --- so the combiner IS effectively a
host in the TCB at sign time, which is why THBS-SE is research-grade,
not production. The TEE pool chooses (a) inside attested hardware
(trust-relocated, not removed). The per-validator standalone path
sidesteps (a) and (b) entirely by emitting N independent signatures and
is the production default.
## Status
| Field | Value |
|---|---|
| Standard | FIPS 205 SLH-DSA (single-party + per-validator standalone aggregate + THBS-SE permissionless threshold) |
| Constructions | 2 (per-validator standalone, THBS-SE) |
| Standard | FIPS 205 SLH-DSA |
| Production primitive | Per-validator standalone (`standalone.go`) --- SOUND |
| Opt-in production | TEE-attested combiner pool (`luxfi/threshold/protocols/slhdsa-tee`) --- sound under attested-hardware trust |
| Research-only | THBS-SE permissionless threshold --- reconstructs the master at the public combiner |
| Reference implementation | `ref/go/pkg/magnetar/` --- pure Go, depends on `cloudflare/circl/sign/slhdsa` v1.6.3 |
| KAT vectors | `vectors/{keygen,sign,verify,thbsse-sign}.json` (deterministic regeneration) |
| Wire identity | Both Magnetar primitives emit byte-identical FIPS 205 signatures; any unmodified slhdsa verifier accepts |
| Tag | `v1.2.0` |
| Cert-profile role | Polaris profile in `luxfi/quasar` (hash-based leg of the maximum-assurance cross-family PQ profile) |
| Wire identity | All paths emit byte-identical FIPS 205 signatures; any unmodified slhdsa verifier accepts. Interop only --- not a confidentiality claim. |
| Cert-profile role | Polaris profile in `luxfi/quasar` (hash-based leg of the cross-family PQ profile) |
| Sibling primitives | Pulsar (FIPS 204 M-LWE), Corona (R-LWE) --- algorithmically distinct families |
## Headline tests
@@ -174,17 +184,22 @@ cd ref/go && GOWORK=off go test -count=1 -short -timeout 600s ./pkg/magnetar/...
`cloudflare/circl/sign/slhdsa.Verify` across all 3 SHAKE modes.
- `TestThbsSE_Wire_FIPS205Verifiable` (thbsse_test.go) --- pins the
same identity for the THBS-SE public combiner output.
- `TestThbsSE_RejectSeedReveal`, `TestThbsSE_RejectUnselectedFORS`,
`TestThbsSE_RejectUnselectedWOTS`, `TestThbsSE_SlotReuseRejected`,
`TestThbsSE_OverselectedCommittee`,
`TestThbsSE_SlotBindingDomainSeparation` --- the 6 invariant gates
for the THBS-SE construction.
- `TestPVSS_DKG_NoSinglePartyHoldsMaster`,
`TestPVSS_DKG_ByteCompatWithDealerPath`,
- `TestThbsSE_RejectSeedReveal`,
`TestThbsSE_RejectOversizedShareWireSize`,
`TestThbsSE_RejectTamperedShareCommitMismatch`,
`TestThbsSE_SlotReuseRejected`, `TestThbsSE_OverselectedCommittee`,
`TestThbsSE_SlotBindingDomainSeparation` --- the THBS-SE
commit-binding / slot-binding gates. (The last two reject-tests were
formerly mis-named ...UnselectedFORS / ...WOTS; THBS-SE shares the
whole seed, so they test commit binding, not atom selection.)
- `TestPVSS_DKG_ProductionTranscriptHidesMaster` --- the production
`RunDKG` transcript hides the master (P2 leak-fix regression gate);
the open-reveal path reveals it (contrast).
- `TestPVSS_DKG_ByteCompatWithDealerPath`,
`TestPVSS_DKG_AdversarialReveals`,
`TestPVSS_DKG_RobustnessAgainstMaliciousCommitments`,
`TestPVSS_DKG_EndToEnd_SignAndVerify` --- the 5 invariant gates
for the dealerless PVSS-DKG setup path (v1.2).
`TestPVSS_DKG_EndToEnd_SignAndVerify` --- further DKG gates
(the end-to-end test drives the production `RunDKG` path).
- `BenchmarkThbsSE_Sign_5of7/Magnetar-SHAKE-192f` --- end-to-end
per-signature wall-clock at < 100 ms/op on Apple M1.
- `TestKAT_ThbsSe` --- deterministic vector replay at (n=7, t=4) x 3
@@ -215,10 +230,12 @@ M-LWE + Corona R-LWE) with hash-based PQ (Magnetar SLH-DSA).
- `CHANGELOG.md` --- release-by-release framing.
- `DEPLOYMENT-RUNBOOK.md` --- public-BFT default + the v1.0 honest
open item (transient seed reconstruction at the public combiner).
- `BLOCKERS.md` --- the v1.1 roadmap (strict-atom-assembly path).
- `CRYPTOGRAPHER-SIGN-OFF.md` --- internal review trail.
- `BLOCKERS.md` --- sound / open / falsely-closed enumeration
(THBS-SE reconstructs the master; PVSS-DKG leak fix; TEE trust model).
- `CRYPTOGRAPHER-SIGN-OFF.md` --- internal review (standalone only).
- `TRUSTED-COMPUTING-BASE.md` --- TCB enumeration.
- `PROOF-CLAIMS.md` --- proof-roadmap inventory.
- `PROOF-CLAIMS.md` --- per-property proven/asserted/open (no
mechanized threshold proof exists).
- `AXIOM-INVENTORY.md` --- assumed-axiom enumeration.
- `FIPS-TRACEABILITY.md` --- line-by-line FIPS 205 conformance trace.
- `PATENTS.md` --- patent-status notes.
@@ -233,8 +250,9 @@ M-LWE + Corona R-LWE) with hash-based PQ (Magnetar SLH-DSA).
- `GPU-PORT-PLAN.md` --- v1.3 GPU acceleration port plan (four
batched FIPS 205 hash-tree kernels at
`lux-private/gpu-kernels/ops/crypto/slhdsa/`).
- `SECURITY.md` --- threat model + strict-PQ profile closure.
- `ASSEMBLE-INVARIANT.md` --- strict-atom Combine invariant.
- `SECURITY.md` --- threat model + strict-PQ profile.
- `ASSEMBLE-INVARIANT.md` --- what the THBS-SE Combine path actually
does (it reconstructs the master; "strict-atom" was proof-by-rename).
## Build
SPEC.md
+35 -2
View File
@@ -15,6 +15,36 @@ Companion documents:
Magnetar v1.0 ships TWO primitives. Both produce FIPS 205 wire bytes
that an unmodified verifier accepts.
### 1.0 Threshold SLH-DSA status (normative)
Magnetar does NOT claim an efficient oracle-respecting thresholdization of
SLH-DSA. Known theoretical barriers for extractable hash-based signatures
(Kondi-Kumar-Vanegas, MPTS '26) imply that, in the no-dealer / no-preprocessing
setting a public, leaderless, permissionless chain requires, threshold signing
CANNOT be achieved by merely making black-box use of the random-oracle / hash
function. A true threshold SLH-DSA signer would have to evaluate the FIPS 205
signing algorithm inside an active-secure MPC -- including the SHAKE/SHA-2/Keccak
computations that derive `R`, the FORS secrets, the WOTS+ chains, and the
authentication paths -- which is non-black-box use of the hash: research-grade
and expected to be expensive (the **T-SLH-DSA-MPC** research track).
Production Magnetar therefore implements threshold **CERTIFICATION** over
**INDEPENDENT** FIPS 205 SLH-DSA signatures -- never threshold signing:
- **Permissionless (production default):** the weighted quorum certificate in
`luxfi/consensus` (`protocol/quasar/quorum_cert.go`). A quorum-weight subset
of the validator set sign independently (1.1 below); a verifier checks the
quorum predicate directly, or via a post-quantum STARK/FRI proof of those
verifications (P3Q, `luxfi/p3q`). No key material is shared, reconstructed,
or combined.
- **Trusted-hardware / custody (opt-in production):** the TEE-attested combiner
pool -- honest trust-relocation (a host enters the TCB), NOT MPC. See
`BLOCKERS.md`.
- **THBS-SE (1.2): RESEARCH-ONLY.** It reconstructs the FIPS 205 master at the
public combiner every signature; it MUST NOT be presented as a
no-reconstruction production threshold. See
`BLOCKERS.md::MAGNETAR-STRICT-ATOM` (OPEN).
### 1.1 Per-validator standalone (public-BFT primary)
API at `ref/go/pkg/magnetar/standalone.go`:
@@ -46,8 +76,11 @@ Trust model:
- No DKG, no shared seed, no aggregator-in-TCB.
- Per-validator slashing is attributable.
- Z-Chain Groth16 rollup compresses `N x |sigma|` to ~192 bytes; the
rollup is a separate primitive (lux-zchain spec).
- A post-quantum P3Q STARK/FRI proof (`luxfi/p3q`) compresses the N
independent signatures plus the weighted-quorum predicate into one
succinct quorum certificate; the rollup is a separate primitive
(`luxfi/consensus` quorum_cert + `luxfi/p3q`). The earlier Groth16/bn254
rollup is classical (pairing-based) and is superseded for PQ finality.
### 1.2 THBS-SE (permissionless threshold)
SUBMISSION-STATUS.md
+26 -12
View File
@@ -1,17 +1,31 @@
# NIST MPTC Submission Status --- Magnetar
> **v1.0 framing.** This document is a v0.x archival snapshot. The
> v1.0 submission shape ports to the THBS-SE construction and the
> per-validator standalone primitive; the v0.x reveal-and-aggregate
> path described below has been removed from the codebase. See
> `CHANGELOG.md::[1.0.0]` for the load-bearing deletions and the
> v1.0 construction surface.
> Honest status of Magnetar's path to NIST Multi-Party Threshold
> Cryptography submission. **Tier A documentation shape complete**
> as of v0.3.0. Mechanized refinement, dudect, v0.4 lifecycle
> additions (ML-KEM envelope wrap + reshare), and external audit
> are the remaining gates to **full Tier A**.
> ## CURRENT STATUS (authoritative; supersedes the v0.x body below)
>
> - **Production primitive: per-validator standalone** (`standalone.go`)
> --- SOUND. N independent FIPS 205 signatures; no shared seed, no
> reconstruction. This is what Magnetar offers for production
> public-BFT signing.
> - **Opt-in production: TEE-attested combiner pool** --- sound under an
> attested-hardware trust model (trust-relocation, NOT MPC).
> - **Permissionless THBS-SE: RESEARCH-ONLY.** The public combiner
> reconstructs the FIPS 205 master every signature
> (`ASSEMBLE-INVARIANT.md`). NOT no-leak. Not a standardizable
> threshold-SLH-DSA claim.
> - **Mechanized proofs: NONE.** The prior EC/Lean track was vacuous and
> has been deleted/scaffolded (`PROOF-CLAIMS.md` §2).
> - **PVSS-DKG open-reveal leak: FIXED** (`RunDKG`; regression-gated).
> - The byte-identity-to-FIPS-205 property is correctness/interop, NOT a
> confidentiality claim.
>
> True no-reconstruction threshold SLH-DSA is OPEN RESEARCH. Magnetar's
> answer for production is the standalone path, which sidesteps it.
> See `BLOCKERS.md` and `CRYPTOGRAPHER-SIGN-OFF.md`.
>
> Everything below this banner is a stale v0.x archival snapshot
> (reveal-and-aggregate, "Tier A documentation shape", v0.4/v0.5
> roadmap). It is retained for provenance only and is NOT the current
> status; where it conflicts with this banner, the banner wins.
## Today (v0.3.0)
TRUSTED-COMPUTING-BASE.md
+10 -5
View File
@@ -49,7 +49,7 @@ correctness is unsound regardless of how clean the code review was.
| 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 |
| Magnetar Go reference (this repository) | Go standard-library correctness, `crypto/rand` randomness quality, transcript-hash primitives in `transcript.go` (cSHAKE256 / KMAC256), byte-wise Shamir / Lagrange in `thbsse_field.go`, THBS-SE protocol in `thbsse.go`, Combine emit in `thbsse_assemble.go` + the FIPS 205 walk in `slhdsa_internal.go`, per-validator standalone in `standalone.go`, dealerless DKG in `pvss_dkg.go` | Reviewed by code inspection; KAT replay (`vectors/*.json` regenerated byte-stably); byte-identity tests vs single-party FIPS 205. (The v0.x files `shamir.go`, `dkg.go`, `threshold.go`, `combine.go` were DELETED.) |
| `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. |
@@ -167,7 +167,7 @@ byte-equality correctness claim:
| 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. |
| Secret-buffer lifetime / coredump risk | The THBS-SE Combine path (`thbsse_assemble.go`) zeroizes the reconstructed-master buffers (`derivedExpandInput`, `derivedMaterial`) and the PRF scratch (`prfAbsorb`, `prfMsgAbsorb`) after use. This is defense-in-depth: the full FIPS 205 master IS resident in the public combiner's memory during one Sign call (the permissionless THBS-SE path is research-grade, not no-leak — see `ASSEMBLE-INVARIANT.md` and `BLOCKERS.md`). For no-resident-seed deployments use the per-validator standalone path or the TEE pool. |
## §6 Independent verification protocol
@@ -180,11 +180,16 @@ To independently verify Magnetar's claims, a reviewer should:
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)
- `standalone.go` — per-validator standalone (PRIMARY production path)
- `thbsse_field.go` — byte-wise Shamir 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
- `pvss_dkg.go` — dealerless DKG (RunDKG production + open-reveal test)
- `thbsse.go`, `thbsse_assemble.go`, `slhdsa_internal.go` — THBS-SE
threshold sign + the master-reconstructing Combine emit
(research-grade; see `ASSEMBLE-INVARIANT.md`)
- `zeroize.go` — secret-buffer wipes
(The v0.x files `shamir.go`, `dkg.go`, `threshold.go`, `combine.go`
were DELETED; ignore any doc that still references them.)
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),
ct/dudect/strict_atom_combine_ct_test.go
+45 -20
View File
@@ -4,12 +4,37 @@
//go:build ct
// +build ct
// Package dudect carries the Magnetar v1.1 strict-atom Combine CT
// harness. Run via:
// Package dudect carries a Magnetar source-hygiene LINT. Run via:
//
// go test -tags ct -run TestStrictAtom_CT ./ct/dudect/...
// go test -tags ct -run TestStrictAtom_IdentHygiene ./ct/dudect/...
//
// or via scripts/checks/dudect-smoke.sh.
//
// =====================================================================
//
// THIS IS NOT A CONSTANT-TIME TEST. IT IS A NAME LINT.
//
// =====================================================================
//
// The check below parses the Combine emit-path sources and asserts
// that no identifier whose NAME is in a hardcoded list feeds an `if`,
// a `switch`, or an index expression. That is a property of variable
// NAMES, not of timing or memory-access behavior:
//
// - It does NOT measure execution time (no dudect, no statistical
// test, no cycle counting).
// - It does NOT track data flow: a secret that flows into a branch
// under a name NOT in the list is invisible to it.
// - It does NOT establish constant-timeness of any function.
//
// More fundamentally, constant-time is the WRONG property to assert
// for this path at all: `assembleSignatureBytes` reconstructs the
// full FIPS 205 master into `derivedMaterial`. A timing side-channel
// is moot when the secret is already sitting in plaintext in the
// combiner's buffer (see BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11 and
// ASSEMBLE-INVARIANT.md). Treat this file as an identifier-style lint
// that keeps the named scratch buffers out of obvious branch/index
// positions, and nothing more.
package dudect
import (
@@ -30,16 +55,13 @@ var strictAtomSources = []string{
"../../ref/go/pkg/magnetar/slhdsa_internal.go",
}
// secretTaggedIdent patterns. The v1.1 CT discipline says: any
// identifier whose name is one of these is carrying secret bytes,
// and therefore must NOT appear in:
// - a switch / if-else condition (control flow on secret)
// - an index expression LHS (array/slice index on secret)
// - a map key (map lookup on secret)
//
// The strict-atom emit path uses these names verbatim for the buffers
// holding Lagrange-reconstructed material; the static check ensures
// they are only consumed via `append`, `copy`, and `Write` calls.
// secretTaggedIdent patterns. This is a NAME list, not a taint
// analysis. The lint flags an identifier ONLY when its spelling
// appears in this set AND it sits in a branch/index position. A
// secret carried under any other name is not detected. This catches
// nothing about timing; it is a style guard that keeps these
// specific scratch-buffer names out of obvious control-flow / index
// positions.
var secretTaggedIdents = map[string]struct{}{
"derivedMaterial": {},
"derivedExpandInput": {},
@@ -49,11 +71,14 @@ var secretTaggedIdents = map[string]struct{}{
"prfMsgAbsorb": {},
}
// TestStrictAtom_CT_NoSecretDependentBranch is the load-bearing per-push
// CT gate. It parses the strict-atom emit-path sources, walks the AST,
// and asserts no secret-tagged identifier feeds a control-flow branch,
// an index expression, or a map key.
func TestStrictAtom_CT_NoSecretDependentBranch(t *testing.T) {
// TestStrictAtom_IdentHygiene_NoNamedBufferInBranch is an
// identifier-hygiene LINT (NOT a constant-time property, NOT a
// security gate). It parses the Combine emit-path sources, walks the
// AST, and asserts no identifier whose NAME is in secretTaggedIdents
// feeds a control-flow branch or an index expression. See the package
// banner: this measures nothing about timing and proves nothing about
// confidentiality.
func TestStrictAtom_IdentHygiene_NoNamedBufferInBranch(t *testing.T) {
for _, rel := range strictAtomSources {
t.Run(filepath.Base(rel), func(t *testing.T) {
abs, err := filepath.Abs(rel)
@@ -103,9 +128,9 @@ func TestStrictAtom_CT_NoSecretDependentBranch(t *testing.T) {
if len(violations) > 0 {
for _, v := range violations {
t.Errorf("strict-atom CT violation: %s", v)
t.Errorf("strict-atom ident-hygiene lint: %s", v)
}
t.Fatalf("%d strict-atom CT violation(s) in %s",
t.Fatalf("%d strict-atom ident-hygiene lint hit(s) in %s",
len(violations), rel)
}
})
proofs/README.md
+54 -54
View File
@@ -1,70 +1,70 @@
# Magnetar --- machine-checked proof track
# Magnetar --- proof track (HONEST: there is no mechanized proof)
Magnetar v1.1 closes `MAGNETAR-STRICT-ATOM-V11` and lands the
mechanised proof track for the strict-atom Combine path. Both
primitives (per-validator standalone + THBS-SE strict-atom) are
covered.
There is currently **no mechanized proof** of any Magnetar threshold
property. This directory contains SCAFFOLDS only. Read this before
treating anything here as assurance.
## What ships at v1.1
## What is actually here
| Layer | Path |
| File | Content |
|---|---|
| EasyCrypt theory shells | `proofs/easycrypt/` |
| Lean bridge (algebraic) | `proofs/lean/Crypto/Magnetar/` |
| Bridge doc | `proofs/lean-easycrypt-bridge.md` |
| `easycrypt/Magnetar_N1_StrictAtom.ec` | SCAFFOLD. 0 mechanized content. Records that THBS-SE Combine byte-equality is NOT proven and explains why the prior "proof" (a theorem `apply`-ing an axiom that restated it) was circular. |
| `easycrypt/Magnetar_N5_PVSS_DKG.ec` | SCAFFOLD. 0 mechanized content. Records that PVSS-DKG secrecy is NOT proven, and that the prior secrecy "theorem" was both vacuous (`conclusion = true`) and false for the open-reveal code it modeled. |
| `lean/Crypto/Magnetar/StrictAtom.lean` | SCAFFOLD. 0 mechanized content. The prior `sorry`-bodied theorem and `:= True` discipline have been removed. |
The construction shape covered by the proof track:
Each file declares no `axiom`, no `admit`, no `sorry`, no `theorem`,
and no `lemma`. The only occurrences of those words are inside prose
comments that describe what was removed.
- The strict-atom emitter `assembleSignatureBytes`
(`ref/go/pkg/magnetar/thbsse_assemble.go`).
- The Magnetar-internal FIPS 205 sec 5/6/7/8 walk `slhSignAtom`
(`ref/go/pkg/magnetar/slhdsa_internal.go`).
- The byte-wise Shamir over GF(257) + Lagrange interpolation at x=0
(`ref/go/pkg/magnetar/thbsse_field.go`).
- The byte-identity claim that ties the strict-atom Combine output to
`cloudflare/circl/sign/slhdsa.SignDeterministic` on the same input.
## What was deleted, and why
## Axiom budget
The following files were deleted because every result in them was
vacuous (`X = X` by `rewrite`, or `conclusion = true` by `trivial`)
or a black-box axiom feeding nothing real. They manufactured the
appearance of a "proof track" with a nonzero theorem count and a
small "admit budget" while proving nothing about the construction:
The strict-atom theory has 5 admits across the dependency cone:
- `Magnetar_N1_SHAKE_Expand.ec` --- only non-axiom lemma was
`shake_expand m s = shake_expand m s` rewritten from `s = s`.
- `Magnetar_N1_Atom_Refinement.ec` --- a single restate-as-axiom.
- `Magnetar_N4_KeyDeriveStable.ec` --- `s = s' => f s = f s'`, i.e.
"this function is a function". Content-free.
- `lemmas/Magnetar_CT.ec` --- `strict_atom_combine_is_ct` discharged
by `admit`; the comment itself called the abstract level "vacuous".
Constant-time was also the wrong property to claim: the Combine
path reconstructs the FIPS 205 master, so there is no secret to
protect from a timing side-channel that is not already in plaintext
in the combiner's buffer.
- `lemmas/SLHDSA_Functional.ec` --- legitimate black-box FIPS 205
functional-spec axioms, but they fed only the deleted files.
| Axiom | File | Discharge mechanism |
|---|---|---|
| `combine_assemble_axiom` | `Magnetar_N1_StrictAtom.ec` | Go extraction trust boundary; audit reads `assembleSignatureBytes` line-for-line against the abstract `AssembleAbs` model. |
| `shake256_functional` | `Magnetar_N1_SHAKE_Expand.ec` | FIPS 202 functional spec. Cross-cited from Lean `Crypto.Lux.SHA3`. |
| `magnetar_internal_refines_circl` | `Magnetar_N1_Atom_Refinement.ec` | Discharged by Go test `TestSlhdsaInternal_ByteEqualToCirclSign` per SHAKE mode. |
| `slhdsa_correctness` | `lemmas/SLHDSA_Functional.ec` | FIPS 205 sec 10 NIST verification. |
| `lagrange_recovers_master` | `Magnetar_N1_StrictAtom.ec` | Algebraic; Lean-bridged to `Crypto.Magnetar.StrictAtom.byte_wise_shamir_lagrange_at_zero_identity`. |
| (CT) abstract-level vacuous | `lemmas/Magnetar_CT.ec` | Concrete CT discharged by direct audit of strict-atom Combine path Go source. |
## Honest summary of the actual evidence base
Total: 6 admits (5 substantive + 1 abstract-vacuous), corresponding to
the trust footprint enumerated in `proofs/easycrypt/README.md`. This is
the same shape as the v0.4 EC track (1 byte-walk + 1 codec + 3
protocol-level + 1 FIPS 205) but specialised to the strict-atom
construction.
Magnetar's correctness/interop evidence is empirical, not mechanized:
## v1.0 -> v1.1 delta
- Per-validator standalone (`standalone.go`) emits single-party
FIPS 205 signatures; `TestMagnetar_Wire_FIPS205Verifiable`.
- THBS-SE Combine emits FIPS 205 signatures byte-identical to
`circl/slhdsa.SignDeterministic` on the reconstructed master;
`TestSlhdsaInternal_ByteEqualToCirclSign`,
`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`.
- KAT determinism via `ref/go/cmd/genkat`.
The v0.x EC scaffolding (modelled the abandoned reveal-and-aggregate
construction) was removed at v1.0; the v1.1 track is built directly
against the strict-atom Combine path.
These are tests. They establish that the threshold output is a valid
FIPS 205 signature. They do NOT establish any confidentiality / no-leak
property, and there is no mechanized refinement.
The Lean side carries the abstract-model discipline statement
`strict_atom_discipline` (vacuous at the abstract level; the concrete
discipline is enforced by the Go test
`TestThbsSE_StrictAtom_NoTransientSeed`).
See `PROOF-CLAIMS.md` for the per-property proven/asserted/open
breakdown.
## Per-push gate
## Open work (tracked, not done)
The `scripts/check-high-assurance.sh` orchestrator runs:
A genuine mechanized result would require an abstract `slh_sign`
model (EasyCrypt or Lean) of the FIPS 205 sec 5--sec 8 hash-tree
signing walk, proven equal to the Go implementation — not to circl,
and not to a restatement of the conclusion. That is multi-week work
and is OPEN.
- `scripts/checks/go-tests.sh` (v1.0 scope; carries forward unchanged).
- `scripts/checks/strict-atom-ast.sh` (NEW at v1.1): runs the
`TestThbsSE_StrictAtom_NoTransientSeed` AST + grep invariant gate
per-push. The AST gate is a fast check that the strict-atom
discipline holds on the file.
- `scripts/checks/easycrypt.sh` (NEW at v1.1): smoke-checks the EC
theory shells for syntax / require / import consistency. Full
EasyCrypt re-run is a release-time gate, not per-push, because
EC is heavy to bring up (the per-push gate runs in <60s; full EC
takes the EC project's standard hour to run).
There is no mechanized no-leak result to target for THBS-SE, because
THBS-SE in the permissionless model reconstructs the master at the
public combiner (research-grade; see `BLOCKERS.md`).
proofs/easycrypt/Magnetar_N1_Atom_Refinement.ec
-77
View File
@@ -1,77 +0,0 @@
(* -------------------------------------------------------------------- *)
(* Magnetar v1.1 --- Internal SLH-DSA refinement to circl *)
(* -------------------------------------------------------------------- *)
(* *)
(* STATUS: 1 admit (`magnetar_internal_refines_circl`). *)
(* *)
(* The Magnetar-internal FIPS 205 sec 5/6/7/8 byte-walk implemented at *)
(* `slhdsa_internal.go::slhSignAtom` emits a byte stream that is *)
(* byte-equal to `cloudflare/circl/sign/slhdsa.SignDeterministic` on *)
(* the same parameter set + key material + msg + ctx. *)
(* *)
(* The discharge witness is the Go test *)
(* `TestSlhdsaInternal_ByteEqualToCirclSign`, which fixtures a *)
(* deterministic 4n-byte master, derives circl's (skSeed, skPrf, *)
(* pkSeed) via scheme.DeriveKey, drives the Magnetar-internal *)
(* slhSignAtom with closures over the derived material, and asserts *)
(* byte-equality across all three SHAKE modes. *)
(* *)
(* The reason this is an axiom and not a fully-discharged ProcEqv is *)
(* that the byte-walk through circl's slh_sign_internal touches: *)
(* - the FIPS 205 sec 5 WOTS+ chain compute *)
(* - the FIPS 205 sec 6 XMSS tree compute *)
(* - the FIPS 205 sec 7 hypertree dispatch *)
(* - the FIPS 205 sec 8 FORS sign + pk-from-sig *)
(* Each is a ~30-line Go function whose byte-for-byte refinement to a *)
(* hypothetical EasyCrypt port would be ~200 lines of straight-line *)
(* `byte=byte` reasoning per primitive. The audit shortcut: the *)
(* Magnetar-internal port is FIPS 205 byte-conformant by direct *)
(* comparison to circl, and circl is the audited reference. *)
(* *)
(* -------------------------------------------------------------------- *)
require import AllCore List Int IntDiv.
require import lemmas.SLHDSA_Functional.
type byte = int.
type bytes = byte list.
type mode = [ M192s | M192f | M256s ].
(* The Magnetar-internal SLH-DSA Sign engine, parametrised by the two
FIPS 205 sec 11.2 callbacks. *)
op slh_sign_atom :
mode
-> bytes
-> bytes
-> bytes
-> bytes
-> (bytes -> bytes -> bytes)
-> (bytes -> bytes -> bytes)
-> bytes.
(* The circl reference. *)
op slh_sign_deterministic : mode -> bytes -> bytes -> bytes -> bytes.
(* The packed sk layout per FIPS 205 sec 10.1 (4n bytes:
skSeed || skPrf || pkSeed || pkRoot). *)
op pack_sk : mode -> bytes -> bytes -> bytes -> bytes -> bytes.
(* The headline refinement. Discharged via the Go-side byte-identity
gate. *)
axiom magnetar_internal_refines_circl :
forall m pkSeedBytes pkRootBytes msg ctx prfFn prfMsgFn,
(forall addr secret,
prfFn addr secret =
slhdsa_prf m pkSeedBytes addr (slhdsa_prf_secret_for_atom m prfFn))
=> (forall opt_rand msg',
prfMsgFn opt_rand msg' =
slhdsa_prf_msg m (slhdsa_prf_msg_secret_for_atom m prfMsgFn) opt_rand msg')
=> slh_sign_atom m pkSeedBytes pkRootBytes msg ctx prfFn prfMsgFn
= slh_sign_deterministic m
(pack_sk m
(slhdsa_prf_secret_for_atom m prfFn)
(slhdsa_prf_msg_secret_for_atom m prfMsgFn)
pkSeedBytes
pkRootBytes)
msg ctx.
proofs/easycrypt/Magnetar_N1_SHAKE_Expand.ec
-91
View File
@@ -1,91 +0,0 @@
(* -------------------------------------------------------------------- *)
(* Magnetar v1.1 --- FIPS 205 SHAKE expansion lemmas *)
(* -------------------------------------------------------------------- *)
(* *)
(* STATUS: 1 admit (`shake256_functional`, cross-cited). *)
(* *)
(* The FIPS 205 sec 10.1 expansion of the 4n-byte master S into the *)
(* triple (skSeed, skPrf, pkSeed) is, for SHAKE families: *)
(* *)
(* expand(S) = SHAKE256(S)[:3n] *)
(* skSeed = expand(S)[0 : n] *)
(* skPrf = expand(S)[n : 2n] *)
(* pkSeed = expand(S)[2n : 3n] *)
(* *)
(* The Lagrange-shared-then-SHAKE-expand composition matches *)
(* circl/sign/slhdsa scheme.DeriveKey on the same input S; this is *)
(* established by `shake_expand_matches_circl_derive_key`. *)
(* *)
(* -------------------------------------------------------------------- *)
require import AllCore List Int IntDiv.
require import lemmas.SLHDSA_Functional.
type byte = int.
type bytes = byte list.
type mode = [ M192s | M192f | M256s ].
op n_of_mode : mode -> int.
(* FIPS 202 SHAKE-256 functional spec (variable-output). Cross-cited
from Lean Crypto.Lux.SHA3. *)
axiom shake256_functional :
forall (input : bytes) (out_len : int),
0 < out_len =>
exists (out : bytes),
size out = out_len. (* a stub stating SHAKE-256 produces an
out_len-byte stream from any input *)
op shake256 : bytes -> int -> bytes.
axiom shake256_size : forall input out_len,
0 < out_len => size (shake256 input out_len) = out_len.
op shake_expand : mode -> bytes -> bytes.
axiom shake_expand_def : forall m s,
shake_expand m s = shake256 s (3 * n_of_mode m).
(* Layout: position-based segment accessors. The strict-atom abstract
model honours the discipline that no named `seed` / `skSeed` /
`skPrf` variable exists, by exposing only positional operators. *)
op skseed_segment_pos : mode -> bytes -> bytes.
op skprf_segment_pos : mode -> bytes -> bytes.
op pkseed_segment_pos : mode -> bytes -> bytes.
axiom skseed_segment_layout : forall m s,
skseed_segment_pos m (shake_expand m s) =
take (n_of_mode m) (shake_expand m s).
axiom skprf_segment_layout : forall m s,
skprf_segment_pos m (shake_expand m s) =
take (n_of_mode m) (drop (n_of_mode m) (shake_expand m s)).
axiom pkseed_segment_layout : forall m s,
pkseed_segment_pos m (shake_expand m s) =
take (n_of_mode m) (drop (2 * n_of_mode m) (shake_expand m s)).
(* Per-byte Lagrange recovery (cross-cited from Pulsar Shamir Lean
bridge). *)
op lagrange_sum : int list -> 'a list -> bytes.
(* Round-trip: SHAKE-expand of the Lagrange-recovered master matches
SHAKE-expand of the original master. *)
lemma shake_expand_idempotent_under_lagrange :
forall (m : mode) (s : bytes) (picks : 'a list) (lambdas : int list),
lagrange_sum lambdas picks = s =>
shake_expand m (lagrange_sum lambdas picks) = shake_expand m s.
proof.
move=> m s picks lambdas Heq.
by rewrite Heq.
qed.
(* Cross-conformance: the Magnetar-internal shake_expand matches
circl's scheme.DeriveKey on the same S. Discharged transitively
through circl's own SHAKE256 invocation in scheme.go (same SHAKE
construction). *)
op circl_derive_key_inputs : mode -> bytes -> (bytes * bytes * bytes).
axiom shake_expand_matches_circl_derive_key :
forall m s,
let (skSeedDerived, skPrfDerived, pkSeedDerived) = circl_derive_key_inputs m s in
skseed_segment_pos m (shake_expand m s) = skSeedDerived
/\ skprf_segment_pos m (shake_expand m s) = skPrfDerived
/\ pkseed_segment_pos m (shake_expand m s) = pkSeedDerived.
proofs/easycrypt/Magnetar_N1_StrictAtom.ec
+54 -207
View File
@@ -1,218 +1,65 @@
(* -------------------------------------------------------------------- *)
(* Magnetar v1.1 --- Class N1-analog strict-atom byte-equality *)
(* Magnetar --- THBS-SE Combine byte-equality *)
(* SCAFFOLD: 0 mechanized content. This file proves NOTHING. *)
(* -------------------------------------------------------------------- *)
(* *)
(* STATUS: 1 admit (the Go-extraction trust boundary *)
(* `combine_assemble_axiom`). *)
(* HONEST STATUS *)
(* ============ *)
(* *)
(* What this file gives reviewers *)
(* ----------------------------- *)
(* This file is a SCAFFOLD. It does not contain a mechanized proof of *)
(* anything. Read this banner before reading any line below it. *)
(* *)
(* 1. The strict-atom-equivalent of the v1.0 Class N1-analog theorem: *)
(* the strict-atom `assembleSignatureBytes` byte stream is *)
(* byte-equal to circl `slhdsa.SignDeterministic` on the same *)
(* Shamir-reconstructed master `S`, for every honest quorum `Q` *)
(* of size `t >= threshold`. *)
(* The earlier revision of this file claimed a headline theorem *)
(* *)
(* 2. The discipline statement: the strict-atom path's intermediate *)
(* byte material exists only as positional slices of the *)
(* SHAKE-256 expansion of `S` --- never as a free-standing named *)
(* `seed` / `skSeed` / `skPrf` variable. *)
(* magnetar_n1_strict_atom_byte_equality *)
(* *)
(* 3. The byte-identity step refinement: the Magnetar-internal *)
(* `slhSignAtom` (FIPS 205 sec 5/6/7/8 walk in pure Go) refines *)
(* circl's FIPS 205 dispatch for the SHAKE families. Discharged *)
(* against the abstract `slh_sign_deterministic` model via the *)
(* `magnetar_internal_refines_circl` axiom, whose extraction *)
(* witness is the Go test `TestSlhdsaInternal_ByteEqualToCirclSign`*)
(* executed per SHAKE mode. *)
(* 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. *)
(* *)
(* Admit accounting *)
(* ---------------- *)
(* 1 admit. The single axiom `combine_assemble_axiom` is the Go- *)
(* extraction trust boundary: the extracted `assembleSignatureBytes` *)
(* function refines the abstract `AssembleAbs` procedure on which the *)
(* theorem is discharged. This is the line-for-line audit obligation. *)
(* WHAT IS ACTUALLY TRUE ABOUT THE CODE THIS FILE WAS MEANT TO MODEL *)
(* ------------------------------------------------------------------ *)
(* *)
(* Cross-cited axioms *)
(* ------------------ *)
(* - `lagrange_inverse_eval` (Lean Crypto.Pulsar.Shamir). *)
(* - `shake256_functional` (Lean Crypto.Lux.SHA3). *)
(* - `slhdsa_correctness` (FIPS 205 sec 10 / NIST). *)
(* - `magnetar_internal_refines_circl` (Go *)
(* TestSlhdsaInternal_ByteEqualToCirclSign). *)
(* - `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. *)
(* -------------------------------------------------------------------- *)
require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.
require import Magnetar_N1_SHAKE_Expand.
require import Magnetar_N1_Atom_Refinement.
require import lemmas.SLHDSA_Functional.
(* ===================================================================
Types --- byte-shape vocabulary.
=================================================================== *)
type byte = int.
type bytes = byte list.
(* The Magnetar parameter set discriminator, restricted to SHAKE. *)
type mode = [ M192s | M192f | M256s ].
(* Width function. *)
op n_of_mode : mode -> int.
axiom n_of_mode_M192s : n_of_mode M192s = 24.
axiom n_of_mode_M192f : n_of_mode M192f = 24.
axiom n_of_mode_M256s : n_of_mode M256s = 32.
(* The seed size is 4n in FIPS 205 SHAKE; this is the byte-shared
width. *)
op seed_size : mode -> int.
axiom seed_size_def : forall m, seed_size m = 4 * n_of_mode m.
(* ===================================================================
Shamir share envelope.
=================================================================== *)
(* One party's byte-wise Shamir share over GF(257): an evaluation
point and the per-byte share-value vector. *)
type share = {
s_x : int;
s_y : int list; (* length = seed_size *)
}.
(* Lagrange basis at x=0 (function of public evaluation points). *)
op lagrange_basis_at_zero : share list -> int list.
(* Per-byte Lagrange sum:
lagrange_sum picks lambdas b =
sum_{i in picks} lambdas_i * picks_i.y[b] mod 257
The result is a `seed_size`-byte vector. *)
op lagrange_sum_byte : int list -> share list -> int -> int.
op lagrange_sum : int list -> share list -> bytes.
(* ===================================================================
FIPS 205 SHAKE expansion (Magnetar_N1_SHAKE_Expand.ec).
=================================================================== *)
(* The 3n-byte expansion of an `seed_size`-byte master:
shake_expand m s = SHAKE256(s)[:3 * n_of_mode m] *)
op shake_expand : mode -> bytes -> bytes.
(* Positional segment accessors. NB the abstract model says the
strict-atom path consumes these as positional slices of a single
buffer, NEVER as named `seed` / `skSeed` / `skPrf` variables; the
abstract model honours this by NOT exposing named binders for
`skSeed` / `skPrf`. Only `prf_secret_segment` and
`prf_msg_secret_segment` exist as operators. *)
op prf_secret_segment : mode -> bytes -> bytes.
op prf_msg_secret_segment : mode -> bytes -> bytes.
op pk_seed_segment : mode -> bytes -> bytes.
(* The segment-positional axioms. *)
axiom prf_secret_segment_layout : forall m s,
prf_secret_segment m (shake_expand m s) =
take (n_of_mode m) (shake_expand m s).
axiom prf_msg_secret_segment_layout : forall m s,
prf_msg_secret_segment m (shake_expand m s) =
take (n_of_mode m) (drop (n_of_mode m) (shake_expand m s)).
axiom pk_seed_segment_layout : forall m s,
pk_seed_segment m (shake_expand m s) =
take (n_of_mode m) (drop (2 * n_of_mode m) (shake_expand m s)).
(* ===================================================================
The strict-atom abstract emit procedure.
=================================================================== *)
(* The single FIPS 205 sec 5/6/7/8 walk, parametrised by the two
secret-side callbacks `prf_out` and `prf_msg`. This is what
`slhSignAtom` in slhdsa_internal.go implements. *)
op slh_sign_atom :
mode
-> bytes (* pk_seed *)
-> bytes (* pk_root *)
-> bytes (* message *)
-> bytes (* ctx *)
-> (bytes -> bytes -> bytes) (* prf_out :: (addr, secret) -> n bytes *)
-> (bytes -> bytes -> bytes) (* prf_msg :: (opt_rand, msg') -> n bytes *)
-> bytes.
(* The strict-atom Combine procedure. Notice the abstract model has NO
`seed` / `skSeed` / `skPrf` binder; the only `s` carrying secret
material is consumed positionally via the segment operators. *)
op assemble_signature_bytes
(m : mode)
(pk_seed pk_root : bytes)
(message ctx : bytes)
(picks : share list)
(lambdas : int list) : bytes =
let derived = shake_expand m (lagrange_sum lambdas picks) in
slh_sign_atom m pk_seed pk_root message ctx
(fun addr secret => slhdsa_prf m pk_seed addr (prf_secret_segment m derived))
(fun opt_rand msg' => slhdsa_prf_msg m (prf_msg_secret_segment m derived) opt_rand msg').
(* The FIPS 205 dispatch baseline (circl). *)
op slh_sign_deterministic : mode -> bytes (* sk packed *) -> bytes -> bytes -> bytes.
(* The Lagrange reconstruction of the master from picks + lambdas. The
v1.0 baseline named this `S`; the v1.1 abstract model treats it as
an opaque output of `lagrange_sum`. The next theorem ties it to
`slh_sign_deterministic`. *)
(* ===================================================================
Top-level statement.
=================================================================== *)
(* A quorum is valid iff its evaluation points are distinct, non-zero,
and the share-y vectors are honest (each is a polynomial evaluation
of the master at the party's evaluation point). The honest-quorum
condition is the standard byte-wise Shamir promise. *)
op valid_quorum : share list -> bool.
(* The honest-quorum promise: for every byte index b, the Lagrange sum
of the (lambda_i, share_i.y[b]) pairs equals the master byte at b.
Lifted from `lagrange_inverse_eval`. *)
axiom lagrange_recovers_master :
forall (lambdas : int list) (picks : share list),
valid_quorum picks =>
lagrange_basis_at_zero picks = lambdas =>
exists (master : bytes),
lagrange_sum lambdas picks = master.
(* The Go-extraction trust boundary. ADMITTED in v1.1; the audit
reads `assemble_signature_bytes` line-for-line against this
abstract model. *)
axiom combine_assemble_axiom :
forall m pk_seed pk_root message ctx picks lambdas,
valid_quorum picks =>
lagrange_basis_at_zero picks = lambdas =>
assemble_signature_bytes m pk_seed pk_root message ctx picks lambdas
= slh_sign_deterministic m
(sk_from_seed m (lagrange_sum lambdas picks)) message ctx.
(* The headline theorem. *)
theorem magnetar_n1_strict_atom_byte_equality :
forall m pk_seed pk_root message ctx picks lambdas,
valid_quorum picks =>
lagrange_basis_at_zero picks = lambdas =>
assemble_signature_bytes m pk_seed pk_root message ctx picks lambdas
= slh_sign_deterministic m
(sk_from_seed m (lagrange_sum lambdas picks)) message ctx.
proof.
move=> m pk_seed pk_root message ctx picks lambdas Hvalid Hlamb.
apply combine_assemble_axiom => //.
qed.
(* Strict-atom discipline statement. The abstract model has NO
identifier binding the byte material under the names `seed`, etc.
The proof reduces to a no-op on the abstract level --- the audit
surface that matters is the Go AST check
TestThbsSE_StrictAtom_NoTransientSeed. *)
op strict_atom_discipline_satisfied : (* in our abstract model, *)
bool = true. (* trivially --- the abstract `assemble_signature_bytes`
does not bind named seed segments. *)
lemma strict_atom_discipline : strict_atom_discipline_satisfied.
proof. by []. qed.
proofs/easycrypt/Magnetar_N4_KeyDeriveStable.ec
-51
View File
@@ -1,51 +0,0 @@
(* -------------------------------------------------------------------- *)
(* Magnetar v1.1 --- Class N4 key-derivation stability *)
(* -------------------------------------------------------------------- *)
(* *)
(* STATUS: 0 admits. *)
(* *)
(* The same-master-yields-same-pk lemma used downstream by *)
(* reshare / rotation analysis. Specifically: *)
(* *)
(* - Setup samples a master S, derives (sk, pk) = KeyFromSeed(S). *)
(* - Setup byte-shares S across the committee via byte-wise Shamir *)
(* over GF(257). *)
(* - At Combine, the strict-atom path Lagrange-recovers S' from any t *)
(* valid shares. The honest-quorum promise (lagrange_recovers_ *)
(* master) gives S = S'. *)
(* - Therefore KeyFromSeed(S) = KeyFromSeed(S'), and the strict-atom *)
(* Combine output verifies under the published pk. *)
(* *)
(* -------------------------------------------------------------------- *)
require import AllCore List Int IntDiv.
type byte = int.
type bytes = byte list.
type mode = [ M192s | M192f | M256s ].
op key_from_seed : mode -> bytes -> (bytes * bytes). (* (sk, pk) *)
(* Determinism of the key-derivation function. *)
lemma key_from_seed_deterministic :
forall m s s',
s = s' =>
key_from_seed m s = key_from_seed m s'.
proof.
move=> m s s' Heq.
by rewrite Heq.
qed.
(* The PK component is a function of the seed only. *)
op pk_of_seed : mode -> bytes -> bytes.
(* The PK extracted by Combine matches the published PK iff the
Lagrange-recovered master matches the setup master. *)
lemma pk_stability_under_lagrange :
forall m s s' lambdas picks,
s = s' =>
pk_of_seed m s = pk_of_seed m s'.
proof.
move=> m s s' lambdas picks Heq.
by rewrite Heq.
qed.
proofs/easycrypt/Magnetar_N5_PVSS_DKG.ec
+52 -269
View File
@@ -1,281 +1,64 @@
(* -------------------------------------------------------------------- *)
(* Magnetar v1.2 --- Class N5 dealerless PVSS-DKG *)
(* Magnetar --- PVSS-DKG setup *)
(* SCAFFOLD: 0 mechanized content. This file proves NOTHING. *)
(* -------------------------------------------------------------------- *)
(* *)
(* STATUS: 2 admits (Shamir info-theoretic cross-cite + Go-extraction *)
(* trust boundary). *)
(* HONEST STATUS *)
(* ============ *)
(* *)
(* Closes BLOCKERS.md::MAGNETAR-PVSS-DKG-V11. *)
(* This file is a SCAFFOLD. The earlier revision declared three *)
(* "theorems": *)
(* *)
(* What this file gives reviewers *)
(* ----------------------------- *)
(* - pvss_dkg_secrecy --- conclusion `... true`, by `trivial`. *)
(* - pvss_dkg_correctness --- by `admit`. *)
(* - pvss_dkg_wire_compat --- conclusion `X = X`, by `trivial`. *)
(* - pvss_dkg_composition... --- conclusion `true`, by `trivial`. *)
(* *)
(* 1. The Class N5 secrecy theorem: an adversary controlling *)
(* (t-1) corrupt parties learns NOTHING about the master byte *)
(* vector M = sum_{i in Q} m_i mod 257 byte-wise, conditioned on *)
(* the published Round-1 commitments and Round-2 reveals of the *)
(* corrupt parties. Reduces to the byte-wise Shamir info- *)
(* theoretic security cross-cited from Crypto.Pulsar.Shamir. *)
(* A lemma whose conclusion is `true` or `X = X` proves nothing about *)
(* the construction; `admit` discharges nothing. All have been removed. *)
(* *)
(* 2. The Class N5 correctness theorem: in a run where |Q| >= t and *)
(* every party in Q has well-formed contributions, the share *)
(* envelope emitted by NewThbsSeKeyFromDealerlessDKG byte-equals *)
(* the dealer-path NewThbsSeKey envelope for the same implicit *)
(* master M. *)
(* THE SECRECY CLAIM WAS NOT ONLY UNPROVEN --- IT WAS FALSE FOR THE *)
(* CODE AS WRITTEN *)
(* ------------------------------------------------------------------ *)
(* *)
(* 3. The Class N5 wire-compat theorem: pointwise byte-equality of *)
(* share envelopes between the dealerless and dealer paths, *)
(* pinned by Go regression test *)
(* TestPVSS_DKG_ByteCompatWithDealerPath. *)
(* The "secrecy theorem" asserted that an adversary controlling (t-1) *)
(* parties learns nothing about the master M = sum_i m_i. But the DKG *)
(* reference path (`pvss_dkg.go`) historically ran in OPEN-REVEAL mode: *)
(* `RunDKGSimulation` called `RevealMsg()` for EVERY party *)
(* unconditionally, and `RevealMsg()` publishes `PolyCoeffs[b][0] = *)
(* m_i[b]` --- the constant term, i.e. the contribution itself. With *)
(* every m_i public, M = sum_i m_i is reconstructible by ANY observer, *)
(* not merely by t-1 colluding insiders. A secrecy proof about code *)
(* that broadcasts the secret is meaningless. *)
(* *)
(* Admit accounting *)
(* ---------------- *)
(* 2 admits: *)
(* - shamir_info_theoretic_secrecy (cross-cited from *)
(* Crypto.Pulsar.Shamir; algebraic byte-wise Shamir over GF(257)) *)
(* - pvss_dkg_extraction (the Go-extraction trust boundary: the *)
(* extracted RunDKGSimulation refines the abstract PVSSDKG_Abs *)
(* model on which pvss_dkg_secrecy and pvss_dkg_correctness are *)
(* discharged). *)
(* The production DKG default has since been changed to *)
(* COMPLAINT-CONDITIONAL reveal (`RunDKG`): a party publishes its *)
(* coefficients ONLY against a recorded complaint; an honest run emits *)
(* NO constant-term reveal. The open-reveal entry point is retained *)
(* behind a loud TEST-ONLY barrier (`RunDKGSimulationOpenReveal`) that *)
(* cannot be reached from the production constructor. See *)
(* `pvss_dkg.go` and `TestPVSS_DKG_ProductionTranscriptHidesMaster`. *)
(* *)
(* Cross-cited axioms *)
(* ------------------ *)
(* - `shamir_info_theoretic_secrecy` (Lean Crypto.Pulsar.Shamir) *)
(* - `gf257_field_arithmetic` (Lean Crypto.Magnetar.GF257) *)
(* - `cshake256_collision_resistance` (FIPS 202 / SP 800-185) *)
(* Even with the code fixed, the secrecy statement remains UNPROVEN *)
(* here: it reduces to byte-wise Shamir information-theoretic secrecy *)
(* over GF(257), which is a standard textbook result but is NOT *)
(* mechanized in this file (the prior `shamir_uniform_view` axiom did *)
(* not even constrain the constant term --- its body was a vacuous *)
(* existential). Mechanizing it is OPEN; tracked in PROOF-CLAIMS.md. *)
(* *)
(* WHAT HAS EMPIRICAL SUPPORT (Go tests, NOT proofs) *)
(* ------------------------------------------------ *)
(* *)
(* - Wire-compat between the dealerless and dealer share envelopes: *)
(* `TestPVSS_DKG_ByteCompatWithDealerPath`. *)
(* - t-1 corrupt parties cannot recover the master from their *)
(* partial-sum view (complaint-conditional path): *)
(* `TestPVSS_DKG_AdversarialReveals`. *)
(* - Production transcript does not reveal sum m_i: *)
(* `TestPVSS_DKG_ProductionTranscriptHidesMaster`. *)
(* *)
(* These are tests, not mechanized theorems. *)
(* *)
(* This file intentionally declares no `theorem`, no `lemma`, and no *)
(* `axiom`; its axiom/admit count is exactly ZERO. *)
(* -------------------------------------------------------------------- *)
require import AllCore List Int IntDiv Distr DBool DInterval.
(* ===================================================================
Types --- byte-shape vocabulary.
=================================================================== *)
type byte = int.
type bytes = byte list.
(* The Magnetar parameter set discriminator, restricted to SHAKE. *)
type mode = [ M192s | M192f | M256s ].
(* seed_size_of m is the byte-length of the master vector for mode m. *)
op seed_size_of : mode -> int.
axiom seed_size_192s : seed_size_of M192s = 96.
axiom seed_size_192f : seed_size_of M192f = 96.
axiom seed_size_256s : seed_size_of M256s = 128.
(* GF(257) byte share field. Operations are mod 257. *)
op q257 : int = 257.
(* The byte-share Shamir polynomial evaluation, used inside the
abstract PVSSDKG_Abs model. f_eval coeffs x = sum_d coeffs[d] * x^d
mod 257. This is the same operator the dealer path uses for
thbsseDealRandomGF / thbsseReconstructGF; the wire-compat theorem
below shows they agree byte-for-byte. *)
op f_eval : int list -> int -> int.
(* Field axioms (cross-cited from Crypto.Magnetar.GF257). *)
axiom f_eval_in_range : forall (coeffs: int list) (x: int),
0 <= f_eval coeffs x < q257.
axiom f_eval_at_zero : forall (coeffs: int list) (m0: int),
coeffs = m0 :: [] ++ (List.behead (List.behead coeffs)) =>
f_eval coeffs 0 = m0 %% q257.
(* The byte-wise Lagrange-at-zero reconstruction. lagrange_at_zero
shares = sum_i lambda_i * shares[i].y mod 257, where lambda_i is the
Lagrange basis at x=0 over GF(257). Cross-cited from
Crypto.Pulsar.Shamir. *)
op lagrange_at_zero : (int * int) list -> int.
axiom lagrange_at_zero_in_range : forall (shares: (int * int) list),
0 <= lagrange_at_zero shares < q257.
(* ===================================================================
The PVSS-DKG abstract model.
=================================================================== *)
(* A party's contribution: (m_i, poly_coeffs[0..t)) where
poly_coeffs[0] = m_i. *)
type contribution = {
m_i : int list; (* length seed_size *)
poly_coeffs : int list list (* indexed by byte then by degree *)
}.
(* A party's share row: (x, y) where y is a per-byte vector of length
seed_size. *)
type share_row = {
party_index : int;
y_vector : int list
}.
(* The full DKG state: n contributions + n share rows per party. *)
type dkg_state = {
n : int;
threshold : int;
contributions : contribution list; (* length n *)
received_shares : share_row list list (* n x n *)
}.
(* The aggregated share at party j: aggregate over the qualified set. *)
op aggregate_share : dkg_state -> int list -> int -> int list.
(* The implicit master: sum of m_i across qualified parties. *)
op implicit_master : dkg_state -> int list -> int list.
(* Honest contribution predicate: each contribution's polynomial agrees
with its m_i (poly_coeffs[b][0] = m_i[b]). *)
op honest_contribution : contribution -> bool.
(* Well-formed state: every contribution honest, every share consistent
with its dealer's polynomial. *)
op well_formed : dkg_state -> bool.
(* ===================================================================
Class N5 secrecy theorem.
=================================================================== *)
(* The adversary's view of an honest party h consists of the (t-1)
shares row[i].y[h-1] for i in T (the corrupt set). We model the
view abstractly as a list of (h, share_to_corrupt). *)
type adv_view = (int * int list) list.
(* shamir_uniform_view captures the Shamir info-theoretic secrecy
property: given any (t-1) Shamir leaves of a degree-(t-1) polynomial
with uniform random non-constant coefficients, the constant term is
uniformly distributed over GF(257) conditioned on the leaves. *)
axiom shamir_uniform_view :
forall (h : int) (poly : int list) (corrupt_indices : int list) (b : int),
List.size poly = (List.size corrupt_indices) + 1 =>
(forall (x : int), 0 <= x < q257) =>
exists (uniform_m : int -> bool),
uniform_m (f_eval poly 0).
(* The N5 secrecy theorem: the adversary controlling (t-1) parties
learns nothing about an honest party's m_i contribution beyond the
(t-1) shares it already holds. By Shamir info-theoretic secrecy
over GF(257), the constant term f_{h,b}(0) = m_h[b] is uniform in
the adversary's view conditioned on the (t-1) shares.
Therefore the master M[b] = sum_{i in Q} m_i[b] mod 257 is uniform
in the adversary's view, since adding the unknown uniform m_h[b]
to any (possibly adversarially chosen) sum yields a uniform result
over GF(257). *)
lemma pvss_dkg_secrecy :
forall (st : dkg_state) (corrupt : int list) (qualified : int list) (h b : int),
well_formed st =>
List.size corrupt = st.`threshold - 1 =>
List.size qualified >= st.`threshold =>
!(List.mem h corrupt) =>
List.mem h qualified =>
0 <= b < (List.size (List.nth witness st.`contributions 0).`m_i) =>
(* The honest party h's contribution at byte b is uniform in the
adversary's view conditioned on the (t-1) shares released to
corrupt parties. *)
true.
proof.
move=> st corrupt qualified h b Hwf Hcsz Hqsz Hncorrupt Hqualif Hbrng.
trivial.
qed.
(* ===================================================================
Class N5 correctness theorem.
=================================================================== *)
(* In a well-formed DKG, the aggregated share envelope sigma_j[b] =
sum_{i in Q} f_{i,b}(j) mod 257 = F_b(j), where F_b is the implicit
aggregate polynomial with constant term M[b] = sum_{i in Q} m_i[b]
mod 257. *)
lemma pvss_dkg_correctness :
forall (st : dkg_state) (qualified : int list) (j : int),
well_formed st =>
List.size qualified >= st.`threshold =>
1 <= j <= st.`n =>
(* The aggregated share at party j equals F_b(j) where F_b is
the implicit aggregate polynomial. *)
aggregate_share st qualified j =
List.map (fun (b : int) =>
(* per-byte: F_b(j) mod 257 *)
List.foldl (fun (acc : int) (i : int) =>
(acc + f_eval
(List.nth witness
(List.nth witness st.`contributions i).`poly_coeffs b)
j) %% q257)
0 qualified)
(List.iota_ 0 (List.size
(List.nth witness st.`contributions 0).`m_i)).
proof.
move=> st qualified j Hwf Hqsz Hjrng.
admit. (* algebraic; expands the definition of aggregate_share. *)
qed.
(* ===================================================================
Class N5 wire-compat theorem.
=================================================================== *)
(* The dealer path emits shares y_i[b] = f_b(i) mod 257 where f_b has
constant term M[b]. The dealerless path emits aggregated shares
sigma_j[b] = sum_{i in Q} f_{i,b}(j) mod 257 = F_b(j) where F_b has
constant term M[b]. By Shamir linearity over GF(257), the two
constructions yield byte-equal share envelopes when the implicit
master M and the implicit polynomial coefficient distribution
agree.
Operationally, the agreement is enforced by the fact that the
dealerless path's aggregate polynomial F_b is a sum of n
independent random degree-(t-1) polynomials, which is itself a
uniform random degree-(t-1) polynomial with constant term M[b].
The dealer path samples an independent uniform random degree-(t-1)
polynomial with constant term M[b]. The two random variables
have the same marginal distribution. *)
lemma pvss_dkg_wire_compat :
forall (st : dkg_state) (qualified : int list) (j : int),
well_formed st =>
List.size qualified >= st.`threshold =>
1 <= j <= st.`n =>
(* The aggregated share matches the wire-format share envelope
NewThbsSeKey would produce for the same master + the same
implicit polynomial. The byte-equality is the proof obligation
discharged by the Go regression test
TestPVSS_DKG_ByteCompatWithDealerPath. *)
let dealerless_share = aggregate_share st qualified j in
let master = implicit_master st qualified in
(* Dealer path: synthesise a dealer-share by evaluating the
aggregate polynomial F_b at j. The wire-equality follows. *)
dealerless_share = aggregate_share st qualified j.
proof.
move=> st qualified j Hwf Hqsz Hjrng /=.
trivial.
qed.
(* ===================================================================
Composition with downstream THBS-SE Combine.
=================================================================== *)
(* When fed into the THBS-SE Combine path, the dealerless-DKG-produced
ThbsSeKey emits a FIPS 205 signature byte-identical to what a
dealer-path ThbsSeKey would emit for the same implicit master. The
composition follows by:
1. pvss_dkg_correctness: aggregated shares = F_b(j) at every
party j, where F_b's constant term is M[b].
2. pvss_dkg_wire_compat: byte-equal share envelopes vs. the
dealer path.
3. Magnetar_N4_KeyDeriveStable: same M yields same pk.
4. Magnetar_N1_StrictAtom: strict-atom Combine emits FIPS 205
bytes byte-equal to circl SignDeterministic on the same
master+msg+ctx.
Therefore the dealerless setup is operationally indistinguishable
from the dealer setup at the wire level, while the no-master-in-
memory invariant separates the two setups at the trust model
level. *)
lemma pvss_dkg_composition_with_combine :
forall (st : dkg_state) (qualified : int list) (msg : bytes) (ctx : bytes),
well_formed st =>
List.size qualified >= st.`threshold =>
true.
proof.
move=> st qualified msg ctx Hwf Hqsz.
trivial.
qed.
proofs/easycrypt/README.md
+21 -82
View File
@@ -1,88 +1,27 @@
# Magnetar v1.1 EasyCrypt theory track
# Magnetar EasyCrypt track (HONEST: empty)
Magnetar v1.1 closes `MAGNETAR-STRICT-ATOM-V11` by ripping out the
v1.0 transient seed reconstruction at the public combiner and routing
the Combine output through a Magnetar-internal FIPS 205 §5--§8
implementation that assembles the wire-form signature byte stream
directly from per-byte Lagrange shares. The mechanised proof track
catches up.
This directory contains **no mechanized EasyCrypt proof**. It holds
two SCAFFOLD files only:
## Theory files
| File | Content |
|---|---|
| `Magnetar_N1_StrictAtom.ec` | 0-content scaffold. Records that THBS-SE Combine byte-equality is NOT proven; explains the prior circular "proof". |
| `Magnetar_N5_PVSS_DKG.ec` | 0-content scaffold. Records that PVSS-DKG secrecy is NOT proven, and that the prior secrecy "theorem" was vacuous AND false for the open-reveal code it modeled. |
| File | Role | Admit budget |
|---|---|---|
| `Magnetar_N1_StrictAtom.ec` | Class N1-analog byte-equality for the strict-atom Combine path. Asserts byte-identity between `assembleSignatureBytes` (the Go strict-atom emitter) and `slh_sign_deterministic(sk_from_seed(S), m, ctx)`. | 1 |
| `Magnetar_N1_SHAKE_Expand.ec` | The FIPS 205 §10.1 SHAKE expansion that lifts the byte-shared master `S` into `(skSeed, skPrf, pkSeed)`. The Lagrange-sum-then-SHAKE composition is byte-equal to circl's `scheme.DeriveKey` on the same input. | 1 |
| `Magnetar_N1_Atom_Refinement.ec` | The strict-atom refinement: the FIPS 205 §5--§8 byte stream emitted by `slhSignAtom` (the Go internal engine) is byte-equal to the byte stream emitted by `circl/slhdsa.SignDeterministic` when both are fed the same `(skSeed, skPrf, pkSeed, pkRoot, msg, ctx)`. | 1 |
| `Magnetar_N4_KeyDeriveStable.ec` | The same-master-yields-same-pk lemma used downstream by reshare/rotation analysis. | 0 |
| `lemmas/SLHDSA_Functional.ec` | The FIPS 205 single-party correctness axiom and the SHAKE-256 PRF/PRF_msg/F/H/T_l/H_msg functional definitions (per FIPS 205 §11.2 SHAKE family). | 4 |
| `lemmas/Magnetar_CT.ec` | Bernstein-Garcia-Levy leakage-model CT lemmas: the strict-atom Combine path has no secret-dependent branch and emits no secret-dependent timing through the `prfAbsorb` / `prfMsgAbsorb` scratch buffers. | 1 |
Neither file declares an `axiom`, `admit`, `lemma`, or `theorem`.
## Axiom inventory (v1.1)
## Why the rest was deleted
The trust footprint:
The earlier EC track (`Magnetar_N1_SHAKE_Expand.ec`,
`Magnetar_N1_Atom_Refinement.ec`, `Magnetar_N4_KeyDeriveStable.ec`,
`lemmas/SLHDSA_Functional.ec`, `lemmas/Magnetar_CT.ec`) advertised a
small "admit budget" (5--6 admits) over a set of theorems that proved
nothing: `X = X` rewrites, `conclusion = true` discharged by
`trivial`, a CT lemma discharged by `admit`, and a headline
byte-equality theorem discharged by `apply`-ing an axiom that restated
it verbatim. A nonzero theorem count with a tidy admit budget is not
evidence when the theorems are vacuous. The files were removed rather
than left to imply a proof track exists.
1. `lagrange_inverse_eval` (algebraic; byte-wise Lagrange@0 identity in
GF(257)). Cross-cited from `Crypto.Pulsar.Shamir` Lean. Magnetar
shares the same byte-wise Shamir construction as Pulsar.
2. `shake256_functional` (FIPS 202 SHAKE-256 functional spec; the
sponge construction is treated as a black-box H : bytes -> bytes
with the absorb-then-squeeze interface). Cross-cited from
`Crypto.Lux.SHA3` Lean.
3. `slhdsa_correctness` (FIPS 205 single-party correctness; from FIPS
205 §10 / NIST verification). Treated as a black-box
functional spec.
4. `combine_assemble_axiom` (the Go extraction trust boundary: the
extracted `assembleSignatureBytes` function refines the abstract
`AssembleAbs` model on which `magnetar_n1_strict_atom_byte_equality`
is discharged). This is the single line of code the audit
reads byte-for-byte against the proof's abstract model.
5. `magnetar_internal_refines_circl` (the Magnetar-internal §5--§8
walk refines circl's FIPS 205 dispatch for the SHAKE families;
discharged via the headline byte-identity gate
`TestSlhdsaInternal_ByteEqualToCirclSign` per-mode).
## Cross-reference to Lean
The Lean side ships `Crypto.Magnetar.StrictAtom` carrying:
- The byte-wise Shamir identity (shared with Pulsar's `Shamir.lean`).
- The Lagrange-at-zero composition lemma.
- The `assembleSignatureBytes` -> `slh_sign_deterministic` abstract
refinement bridge.
See `~/work/lux/magnetar/proofs/lean/Crypto/Magnetar/` for the Lean
source.
## v1.0 -> v1.1 delta
The v1.0 (deleted) theories modeled the seed-reconstruction
`combine.go` and the `slhSignDeterministic` dispatch. The v1.1
theories model:
- `thbsse_assemble.go::assembleSignatureBytes` (the strict-atom emit
path).
- `slhdsa_internal.go::slhSignAtom` (the Magnetar-internal FIPS 205
§5--§8 walk that the strict-atom path drives).
The byte-identity claim is the SAME (Magnetar emits FIPS 205
wire-format signature bytes any unmodified verifier accepts), but the
abstract model now has the additional constraint that the FIPS 205
master byte material flows through positional slices of a single
SHAKE-output buffer, never through a free-standing named variable.
The mechanised statement of the strict-atom discipline is in
`Magnetar_N1_StrictAtom.ec`'s top-level theorem:
```
theorem magnetar_n1_strict_atom_byte_equality :
forall pkBytes msg ctx picks lambdas,
valid_quorum picks =>
lagrange_basis_at_zero picks = lambdas =>
assemble_signature_bytes pkBytes msg ctx picks lambdas
= slh_sign_deterministic (sk_from_seed (lagrange_sum picks)) msg ctx.
```
The discipline is reflected in the abstract model `AssembleAbs`,
which mediates the Lagrange reconstruction through the SHAKE absorb
buffers ONLY at the FIPS 205 §11.2 PRF and PRF_msg call sites.
See `../README.md` (proof-track overview) and `../../PROOF-CLAIMS.md`
(per-property breakdown).
proofs/easycrypt/lemmas/Magnetar_CT.ec
-74
View File
@@ -1,74 +0,0 @@
(* -------------------------------------------------------------------- *)
(* Magnetar_CT --- Constant-time leakage analysis for the strict-atom *)
(* Combine path. *)
(* -------------------------------------------------------------------- *)
(* *)
(* STATUS: 1 admit (abstract-level CT is vacuous; the concrete CT *)
(* obligation is discharged by direct audit of the Go strict-atom *)
(* Combine path). *)
(* *)
(* The Bernstein-Garcia-Levy leakage model: a procedure is *)
(* constant-time iff for every pair of secret inputs that agree on the *)
(* public projection, the execution trace (control flow + memory *)
(* access pattern) is identical. *)
(* *)
(* For the strict-atom Combine path: *)
(* *)
(* - The Lagrange basis (`lambdas`) is a function of PUBLIC *)
(* evaluation points; no branch on secret bytes. *)
(* - The per-byte Lagrange sum is straight-line modular arithmetic: *)
(* `acc = (acc + lambda_i * y_i) mod 257`. No branch on `y_i`. *)
(* - The 257 reduction is one branchless modulo on a `uint32`. *)
(* - The SHAKE expansion is constant-time per FIPS 202 SHAKE-256. *)
(* - The PRF / PRF_msg absorb buffers are constructed by *)
(* `append`-positional copies; no branch on input bytes. *)
(* - The Magnetar-internal FIPS 205 walk in `slh_sign_atom` performs *)
(* control flow based on PUBLIC inputs (FORS index bits derived *)
(* from the message digest; WOTS+ chain step counts derived from *)
(* the message digits; XMSS auth path layer index). No control *)
(* flow depends on the secret-segment bytes carried through *)
(* `prfFn` / `prfMsgFn`. *)
(* *)
(* These five obligations are discharged by direct inspection of the *)
(* Go source. The Bernstein-Garcia-Levy obligation reduces to: *)
(* *)
(* forall (s1 s2 : secret_state), *)
(* public_projection s1 = public_projection s2 *)
(* => trace(combine s1) = trace(combine s2). *)
(* *)
(* The trace function is the Go runtime's branch + memory-access *)
(* sequence; in the Magnetar strict-atom path the only secret- *)
(* dependent memory access is the READ from `derivedMaterial` at the *)
(* positional segment offsets, which is BRANCHLESS by construction. *)
(* *)
(* -------------------------------------------------------------------- *)
require import AllCore List Int IntDiv.
type byte = int.
type bytes = byte list.
(* The strict-atom Combine path's trace function (abstract). *)
op combine_trace : bytes -> bytes.
(* The public projection of a secret state (the share envelopes' wire
bytes are public --- they're broadcast in Round 2 --- so the
public projection is the identity on the share-envelope half and
zero-erases the lambda/derived bytes). *)
op public_projection : bytes -> bytes.
(* The CT obligation: traces depend only on the public projection. *)
op ct_safe (f : bytes -> bytes) : bool =
forall s1 s2, public_projection s1 = public_projection s2 =>
f s1 = f s2.
(* The strict-atom Combine path satisfies CT. ADMITTED-free at the
abstract level; the audit reads the Go source to discharge. *)
lemma strict_atom_combine_is_ct : ct_safe combine_trace.
proof.
rewrite /ct_safe.
move=> s1 s2 _.
(* In the abstract model both traces collapse to a constant value;
the real CT obligation is on the Go source. *)
admit. (* abstract-level vacuous; concrete CT discharged by audit *)
qed.
proofs/easycrypt/lemmas/SLHDSA_Functional.ec
-74
View File
@@ -1,74 +0,0 @@
(* -------------------------------------------------------------------- *)
(* SLHDSA_Functional --- FIPS 205 SHAKE functional spec *)
(* -------------------------------------------------------------------- *)
(* *)
(* STATUS: 4 admits (FIPS 205 sec 11.2 SHAKE primitive definitions *)
(* lifted as black-box ops; the FIPS 205 sec 10 correctness axiom is *)
(* a black-box claim from NIST verification). *)
(* *)
(* The FIPS 205 sec 11.2 SHAKE primitives: *)
(* *)
(* PRF(PK.seed, ADRS, SK.seed) = SHAKE256(PK.seed || ADRS || SK.seed)[:n] *)
(* PRF_msg(SK.prf, optRand, M) = SHAKE256(SK.prf || optRand || M)[:n] *)
(* F(PK.seed, ADRS, M_1) = SHAKE256(PK.seed || ADRS || M_1)[:n] *)
(* H(PK.seed, ADRS, M_1||M_2) = SHAKE256(PK.seed || ADRS || M_1 || M_2)[:n] *)
(* T_l(PK.seed, ADRS, M) = SHAKE256(PK.seed || ADRS || M)[:n] *)
(* H_msg(R, PK.seed, PK.root, M) = SHAKE256(R || PK.seed || PK.root || M)[:m] *)
(* *)
(* The single-party correctness of FIPS 205 SLH-DSA SignDeterministic *)
(* is the standard "if SignDeterministic returns sig, then Verify(pk, *)
(* msg, sig) accepts" claim, modulo the FIPS 205 sec 10 well-formedness *)
(* conditions on inputs. *)
(* *)
(* -------------------------------------------------------------------- *)
require import AllCore List Int IntDiv.
type byte = int.
type bytes = byte list.
type mode = [ M192s | M192f | M256s ].
op n_of_mode : mode -> int.
(* FIPS 205 sec 11.2 SHAKE family --- PRF (FORS leaf / WOTS+ chain
base derivation). *)
op slhdsa_prf :
mode -> bytes (* pk_seed *) -> bytes (* addr *) -> bytes (* sk_seed *) -> bytes.
axiom slhdsa_prf_size : forall m pkSeed addr skSeed,
size (slhdsa_prf m pkSeed addr skSeed) = n_of_mode m.
(* FIPS 205 sec 11.2 SHAKE family --- PRF_msg (signature randomizer). *)
op slhdsa_prf_msg :
mode -> bytes (* sk_prf *) -> bytes (* opt_rand *) -> bytes (* msg' *) -> bytes.
axiom slhdsa_prf_msg_size : forall m skPrf optRand msg,
size (slhdsa_prf_msg m skPrf optRand msg) = n_of_mode m.
(* The packed sk byte layout: 4n bytes.
sk = skSeed || skPrf || pkSeed || pkRoot. *)
op pack_sk : mode -> bytes -> bytes -> bytes -> bytes -> bytes.
(* The FIPS 205 sk_from_seed driver: derive (skSeed, skPrf, pkSeed) via
SHAKE256 expansion, compute pkRoot via the inner setup primitive,
pack the result. *)
op sk_from_seed : mode -> bytes -> bytes.
(* The two "secret-segment extractors" used in
Magnetar_N1_Atom_Refinement to discharge the closure-equivalence.
These are abstract values that capture "the n-byte secret material
the closure feeds at every PRF / PRF_msg call". *)
op slhdsa_prf_secret_for_atom : mode -> (bytes -> bytes -> bytes) -> bytes.
op slhdsa_prf_msg_secret_for_atom : mode -> (bytes -> bytes -> bytes) -> bytes.
(* FIPS 205 sec 10 correctness: SignDeterministic produces a verifiable
signature for any well-formed sk. Black-box from NIST. *)
op slh_sign_deterministic : mode -> bytes -> bytes -> bytes -> bytes.
op slh_verify : mode -> bytes (* pk *) -> bytes -> bytes -> bytes -> bool.
op pk_from_sk : mode -> bytes -> bytes.
axiom slhdsa_correctness :
forall m sk msg ctx,
slh_verify m (pk_from_sk m sk) msg
(slh_sign_deterministic m sk msg ctx) ctx
= true.
proofs/lean-easycrypt-bridge.md
+19 -58
View File
@@ -1,64 +1,25 @@
# Lean -- EasyCrypt bridge (Magnetar v1.1)
# Lean -- EasyCrypt bridge (HONEST: there is no bridge)
This document is the cross-reference table between the Magnetar
EasyCrypt theories and the Lean theorems they cite. The bridge lets
the EasyCrypt side treat algebraic / hash-functional content as
black-box axioms while the Lean side carries the corresponding
proofs (or proof statements) in a dependent type theory.
There is **no Lean<->EasyCrypt proof bridge** for Magnetar. This
document previously presented a cross-reference table mapping
EasyCrypt axioms to Lean theorems, but:
## Direction
- The EasyCrypt "theorems" it pointed at were vacuous (a theorem
whose proof was `apply` of an axiom restating it; lemmas of the
form `X = X`) and have been deleted or reduced to scaffolds.
- The Lean "theorems" it pointed at (`strict_atom_byte_equality`,
`strictAtomDisciplineSatisfied`) were a `sorry`-bodied theorem and
a `Prop := True` definition. Both have been removed.
- The EasyCrypt theory shells are AUTHORITATIVE for the protocol-level
byte-equality statement (the strict-atom Combine output equals the
FIPS 205 SignDeterministic dispatch).
- The Lean theories are AUTHORITATIVE for the algebraic content
(byte-wise Shamir over GF(257), Lagrange interpolation at x=0,
SHAKE-256 functional spec).
- Cross-references are explicit at the axiom-declaration site in
EasyCrypt.
A "bridge" between two sides that each prove nothing is not a bridge.
## Cross-cited axioms
## What would a real bridge be
| EasyCrypt axiom | Lean theorem | Lean location |
|---|---|---|
| `lagrange_recovers_master` (Magnetar_N1_StrictAtom.ec) | `byte_wise_shamir_lagrange_at_zero_identity` | `Crypto/Magnetar/StrictAtom.lean` (+ shared with `Crypto/Pulsar/Shamir.lean`) |
| `shake256_functional` (Magnetar_N1_SHAKE_Expand.ec) | `shake256_functional` | `Crypto/Magnetar/StrictAtom.lean` (+ shared with `Crypto/Lux/SHA3.lean`) |
| `slhdsa_correctness` (lemmas/SLHDSA_Functional.ec) | NIST FIPS 205 sec 10 (external reference) | n/a |
| `combine_assemble_axiom` (Magnetar_N1_StrictAtom.ec) | n/a (Go extraction trust boundary) | n/a |
| `magnetar_internal_refines_circl` (Magnetar_N1_Atom_Refinement.ec) | n/a (discharged by Go test `TestSlhdsaInternal_ByteEqualToCirclSign`) | n/a |
If Magnetar's GF(257) byte-wise Shamir / Lagrange-at-zero algebra
were mechanized in Lean (as Pulsar's reportedly is under
`Crypto.Pulsar.Shamir`), an EasyCrypt protocol proof could cite those
Lean lemmas as discharged algebraic facts. That cross-citation does
NOT exist for Magnetar today: there is no EasyCrypt protocol proof to
cite into, and the cross-citation was never machine-checked.
## What is shared with Pulsar
Magnetar's byte-wise Shamir over GF(257) is ALGEBRAICALLY IDENTICAL
to Pulsar's; the difference is only what is shared. Magnetar shares
the SLH-DSA scheme seed; Pulsar shares the ML-DSA private key
vector. The Shamir polynomial machinery, the GF(257) modular
arithmetic, the Lagrange basis at x=0, and the Lagrange-recovers-
master identity are the SAME and live in Lean under
`Crypto.Pulsar.Shamir`. Magnetar cross-cites those theorems.
## What is unique to Magnetar v1.1
The strict-atom discipline statement is unique to Magnetar v1.1:
- `strict_atom_byte_equality` (Lean) corresponds to
`magnetar_n1_strict_atom_byte_equality` (EasyCrypt) corresponds to
`TestThbsSE_StrictAtom_NoTransientSeed` + `TestSlhdsaInternal_
ByteEqualToCirclSign` + `TestThbsSE_StrictAtom_Combine_ByteIdentity
ToCircl` (Go test suite).
- The abstract-model discipline statement
`strict_atom_discipline_satisfied` (EC) corresponds to
`strictAtomDisciplineSatisfied` (Lean) corresponds to the AST grep
check in `TestThbsSE_StrictAtom_NoTransientSeed`.
## v1.0 -> v1.1 delta
- v0.x bridges modelled the abandoned reveal-and-aggregate
construction; removed at v1.0.
- v1.0 ship state: no proof bridge in repo (the bridge re-lands at
v1.1 alongside the strict-atom construction; this is the present
document).
- v1.1: 2 Magnetar-specific cross-cites + 1 shared Pulsar Shamir
cross-cite + 1 shared Lux SHA3 cross-cite + 2 NIST/Go-extraction
external references.
See `proofs/README.md` and `PROOF-CLAIMS.md` for the honest state.
proofs/lean/Crypto/Magnetar/StrictAtom.lean
+32 -108
View File
@@ -6,124 +6,48 @@ Released under the same license as the rest of Magnetar.
/-!
# Crypto.Magnetar.StrictAtom
Lean bridge for the Magnetar v1.1 strict-atom Combine path. This file
states the algebraic invariants that the EasyCrypt theory shells
(`proofs/easycrypt/Magnetar_N1_StrictAtom.ec` etc.) cross-cite.
SCAFFOLD: 0 mechanized content. This file proves NOTHING.
## Top-level claims
## Honest status
The Lean side carries three load-bearing claims:
The earlier revision of this file declared a theorem
`strict_atom_byte_equality` whose proof body was `sorry`, and a
definition `strictAtomDisciplineSatisfied : Prop := True` with a
companion `theorem strict_atom_discipline := trivial`. A `sorry`
discharges nothing, and a `True`-valued "discipline" proves nothing
about the code. Both have been removed.
1. `byte_wise_shamir_lagrange_at_zero_identity`: the byte-wise Shamir
construction over GF(257) with Lagrange interpolation at x=0 is
the left inverse of polynomial evaluation at distinct non-zero
evaluation points. This is the shared lemma with Pulsar's
`Crypto.Pulsar.Shamir`.
## What the code actually does
2. `shake256_expansion_is_a_function`: SHAKE-256 with a given input
and a fixed output length is a function (the FIPS 202 functional
spec). Cross-cited from `Crypto.Lux.SHA3`.
The THBS-SE Combine path
(`ref/go/pkg/magnetar/thbsse_assemble.go::assembleSignatureBytes`)
Lagrange-reconstructs the FIPS 205 master byte vector, SHAKE-expands
it into a single buffer holding `skSeed || skPrf || pkSeed`, and
emits a FIPS 205 signature. The full master is present in the public
combiner's memory for the duration of one Sign call. Renaming the
buffer to avoid the identifier `seed` does NOT establish any no-leak
property. There is nothing here for Lean to certify as confidential.
3. `assemble_signature_bytes_strict_atom_invariant`: the abstract-
model statement that the strict-atom emitter's intermediate byte
material exists only as positional slices of the SHAKE expansion
buffer, never as a free-standing named variable. The Go-side
enforcement is `TestThbsSE_StrictAtom_NoTransientSeed`; the Lean
side carries the abstract-model counterpart.
The only empirically supported property is byte-IDENTITY of the
emitted signature to `circl/slhdsa.SignDeterministic` on the
reconstructed master (a correctness/interop property), witnessed by
the Go tests `TestSlhdsaInternal_ByteEqualToCirclSign` and
`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`. No Lean theorem
backs it.
## Cross-reference
EasyCrypt counterparts live at:
- `proofs/easycrypt/Magnetar_N1_StrictAtom.ec`
- `proofs/easycrypt/Magnetar_N1_SHAKE_Expand.ec`
- `proofs/easycrypt/Magnetar_N1_Atom_Refinement.ec`
The headline theorem ties the algebraic Lagrange identity (lemma 1)
+ the SHAKE-256 functional spec (lemma 2) into the byte-equality
claim that the strict-atom Combine emits FIPS 205 wire bytes accepted
by any unmodified verifier.
A genuine result would require an abstract Lean model of the FIPS 205
hash-tree signing walk proven equal to the Go implementation — not a
`sorry`, and not a `True`. That work is OPEN and is tracked in
`PROOF-CLAIMS.md`.
This file intentionally declares no `theorem`, no `axiom`, no `sorry`,
and no `def`. It is a documentation stub only.
-/
namespace Crypto.Magnetar.StrictAtom
/-- GF(p) for the byte-wise Shamir prime p=257. -/
abbrev SharePrime : Nat := 257
/-- One party's byte-wise Shamir share. -/
structure Share where
/-- Shamir evaluation point in [1, 257). -/
x : Nat
/-- Per-byte share values, each in [0, 257). Length = seed_size. -/
y : List Nat
/-- The Lagrange basis at zero over GF(257), as a function of evaluation
points only. Implementation matches `lagrangeBasisAtZero` in
`thbsse_assemble.go`. -/
opaque lagrangeBasisAtZero : List Share → List Nat
/-- Per-byte Lagrange sum over GF(257). -/
opaque lagrangeSum : List Nat → List Share → List Nat
/-- The honest-share predicate: every party's share is an honest
polynomial evaluation of the master at the party's evaluation point,
with distinct non-zero evaluation points across the quorum. -/
opaque ValidQuorum : List Share → Prop
/-- The byte-wise Shamir + Lagrange-at-zero identity over GF(257). -/
axiom byte_wise_shamir_lagrange_at_zero_identity :
∀ (master : List Nat) (picks : List Share) (lambdas : List Nat),
ValidQuorum picks →
lagrangeBasisAtZero picks = lambdas →
-- Honest quorum recovers the master byte-by-byte.
lagrangeSum lambdas picks = master
/-- The FIPS 202 SHAKE-256 expansion. Cross-cited from
`Crypto.Lux.SHA3`. -/
opaque shake256 : List Nat → Nat → List Nat
/-- SHAKE-256 is functional: same input + length yields the same
output. -/
axiom shake256_functional :
∀ (s : List Nat) (len : Nat), shake256 s len = shake256 s len
/-- The strict-atom Combine abstract emitter. -/
opaque assembleSignatureBytes :
List Nat → -- pkSeed
List Nat → -- pkRoot
List Nat → -- message
List Nat → -- ctx
List Share → -- picks
List Nat → -- lambdas
List Nat
/-- The circl FIPS 205 SignDeterministic reference. -/
opaque slhSignDeterministic : List Nat → List Nat → List Nat → List Nat
/-- The packed sk constructor from a 4n-byte master. -/
opaque skFromSeed : List Nat → List Nat
/-- The strict-atom byte-equality claim (the Class N1-analog theorem
of the v1.1 EasyCrypt theory). -/
theorem strict_atom_byte_equality :
∀ (pkSeed pkRoot message ctx : List Nat)
(picks : List Share) (lambdas : List Nat),
ValidQuorum picks →
lagrangeBasisAtZero picks = lambdas →
assembleSignatureBytes pkSeed pkRoot message ctx picks lambdas
= slhSignDeterministic (skFromSeed (lagrangeSum lambdas picks)) message ctx := by
intros pkSeed pkRoot message ctx picks lambdas _ _
-- Discharged in EasyCrypt via combine_assemble_axiom (the
-- Go-extraction trust boundary). Lean-side this is a stub.
sorry
/-- The strict-atom discipline statement: at the ABSTRACT model level
the FIPS 205 master byte material is only addressable via positional
operators of the SHAKE-expansion output. No `seed` / `skSeed` /
`skPrf` Lean binder exists in scope of `assembleSignatureBytes`. -/
def strictAtomDisciplineSatisfied : Prop := True
theorem strict_atom_discipline : strictAtomDisciplineSatisfied := trivial
-- Intentionally empty. See the module banner: this is a 0-content
-- scaffold. It exists only to record, in the proof tree, that the
-- THBS-SE strict-atom byte-equality is NOT mechanized.
end Crypto.Magnetar.StrictAtom
proofs/lean/README.md
+15 -31
View File
@@ -1,36 +1,20 @@
# Magnetar v1.1 Lean bridge
# Magnetar Lean bridge (HONEST: empty)
The Lean bridge carries the algebraic invariants that the EasyCrypt
theories cross-cite. Two top-level claims live here:
This directory contains **no mechanized Lean proof** for Magnetar.
1. `byte_wise_shamir_lagrange_at_zero_identity` --- byte-wise Shamir
+ Lagrange-at-zero over GF(257) is the left inverse of polynomial
evaluation at distinct non-zero points. Shared with
`Crypto.Pulsar.Shamir`.
`Crypto/Magnetar/StrictAtom.lean` is a 0-content scaffold. Its prior
`strict_atom_byte_equality` theorem had a `sorry` body, and its
`strictAtomDisciplineSatisfied : Prop := True` proved nothing about
the code; both were removed.
2. `shake256_functional` --- the FIPS 202 SHAKE-256 functional spec
(same input + output length yields the same byte stream). Shared
with `Crypto.Lux.SHA3`.
The file now declares no `theorem`, no `axiom`, no `def`, and no
`sorry`. It exists only to record, in the proof tree, that THBS-SE
strict-atom byte-equality is NOT mechanized in Lean.
## Files
There is no Magnetar-specific Lean algebra here. If the GF(257)
byte-wise Shamir / Lagrange-at-zero identity were needed as a
discharged fact, it would have to be cited from a real
`Crypto.Pulsar.Shamir` development; no such cross-citation is
machine-checked for Magnetar today.
| File | Role |
|---|---|
| `Crypto/Magnetar/StrictAtom.lean` | The strict-atom byte-equality theorem statement + the discipline statement (abstract-level no-op). |
## Build
The Lean bridge requires Lean 4 (>= v4.5.0). It is intended to be
loaded as part of the broader `Crypto.Lux` Lean library; build
configuration in this checkout is minimal (the bridge is text-only
verification surface, not an executable). Cross-citations to
`Crypto.Pulsar.Shamir` and `Crypto.Lux.SHA3` are RESOLVED in the
sibling `~/work/lux/proofs/lean/Crypto/` checkout.
## v1.0 -> v1.1 delta
The v1.0 Lean bridge modeled the byte-wise Shamir layer shared with
Pulsar. v1.1 adds the strict-atom byte-equality theorem with the
abstract-model discipline statement. The shared Shamir layer is
unchanged (the byte-wise GF(257) construction is algebraically
identical between Magnetar and Pulsar).
See `../README.md` and `../../PROOF-CLAIMS.md` for the honest state.
ref/go/cmd/genkat/main.go
+2 -2
View File
@@ -265,10 +265,10 @@ func main() {
Round2: r2s,
})
if err != nil {
fail(fmt.Errorf("Combine mode=%s msg=%d: %w", mode, msgIdx, err))
fail(fmt.Errorf("combine mode=%s msg=%d: %w", mode, msgIdx, err))
}
if len(evidences) != 0 {
fail(fmt.Errorf("Combine emitted evidences on honest KAT mode=%s msg=%d: %+v",
fail(fmt.Errorf("combine emitted evidences on honest KAT mode=%s msg=%d: %+v",
mode, msgIdx, evidences))
}
ref/go/pkg/magnetar/pvss_dkg.go
+424 -208
View File
@@ -3,47 +3,50 @@
package magnetar
// pvss_dkg.go --- Dealerless PVSS-DKG for the THBS-SE setup.
//
// Closes BLOCKERS.md::MAGNETAR-PVSS-DKG-V11.
// pvss_dkg.go --- PVSS-DKG for the THBS-SE setup.
//
// =====================================================================
// WHAT THIS FILE GIVES YOU
// HONEST SUMMARY: TWO PATHS, ONE HARD BARRIER
// =====================================================================
//
// A pure-Go runDKG that takes a sorted committee, the FIPS 205 mode,
// the (n, t) threshold pair, and a slice of per-party rng readers, and
// emits a wire-compatible *ThbsSeKey whose Shares field is byte-shaped
// identically to what NewThbsSeKey produces, but where:
// This file provides a dealerless setup for THBS-SE share material.
// There are TWO entry points, and they differ in exactly one property:
// whether the transcript reveals the master.
//
// - NO PARTY HOLDS THE MASTER. The master byte vector M[b] is the
// mod-257 sum of n per-party contributions m_i[b]. Honest parties
// keep their m_i memory-local; corrupted parties release m_i to
// the adversary; the master itself is never assembled in any
// party's heap, ever.
// - RunDKG (PRODUCTION): the transcript carries NO constant-term
// reveals (Reveals == nil; tr.RevealsMaster() == false). An
// observer of the transcript CANNOT reconstruct M = sum_i m_i from
// polynomial reveals. This is the no-leak setup path.
//
// - NO TRUSTED DEALER. There is no privileged setup machine. The
// protocol runs symmetrically across all n parties.
// - RunDKGSimulationOpenRevealTestOnly (TEST/KAT): every party
// publishes its full RevealMsg, so the transcript REVEALS the
// master. It exists for deterministic KAT replay and for
// exercising the verification logic in tests. It requires an
// explicit hazard acknowledgement and MUST NOT run in production.
//
// - PUBLICLY VERIFIABLE. Every party publishes a hash-based
// commitment to each polynomial coefficient at Round 1, and at
// Round 2 reveals blinding randomness alongside Reed-Solomon
// consistency tags any peer uses to verify a party's shares
// against the published commitments without learning the
// contribution.
// THE HARD BARRIER (read before trusting the no-leak claim):
//
// - WIRE-COMPATIBLE. The emitted *ThbsSeKey is byte-shape identical
// to the dealer-path output. Specifically:
// * key.Shares[i].EvalPoint = committee_index + 1 (1-indexed,
// matching the dealer path's EvalPointFromCommitteeIndex).
// * key.Shares[i].Share = bigEndianU16 lanes of party_i's
// aggregated Shamir share over GF(257), same wire as
// thbsseShareToBytes(thbsseShare{X, Y}).
// * key.SetupTranscript = the same cSHAKE256(pk_bytes || n
// || t || committee[i]_serialized...) digest the dealer path
// emits, so any auditor's transcript hash matches.
// The wire equality is enforced by
// TestPVSS_DKG_ByteCompatWithDealerPath.
// Deriving the SLH-DSA group public key needs the master.
// pk = SLH-DSA.PK(M) is a hash tree over M; there is no way to
// compute it from shares without reconstructing M at some party (or
// full MPC over the SHAKE hash tree --- open research). So
// deriveDKGPublicKey RECONSTRUCTS M transiently to compute pk and
// zeroizes it. That reconstruction is the inherent cost of producing
// any SLH-DSA-shaped artifact from a shared seed. It is NOT
// published, but it does mean SOME party (whoever derives pk) holds M
// for an instant. "No party EVER holds M" is achievable only via the
// TEE path or the dealer path. Do not over-claim it.
//
// The earlier banner here claimed "NO PARTY HOLDS THE MASTER ... ever"
// and described a "NO-MASTER-IN-MEMORY DISCIPLINE" whose only content
// was naming a buffer `lagrangeScratch` instead of `seed`. That was
// the same proof-by-rename used on the SIGN side: a variable name is
// not a security property, and the pk-derivation reconstruction is
// real. Both claims are corrected here and in BLOCKERS.md.
//
// Wire compatibility: the emitted *ThbsSeKey is byte-shape identical to
// the dealer-path output (TestPVSS_DKG_ByteCompatWithDealerPath uses
// the open-reveal path because it inspects the polynomial reveals).
//
// =====================================================================
// CONSTRUCTION
@@ -56,12 +59,13 @@ package magnetar
// re-cast the same algebraic shape over GF(257) using a hash-based
// commitment construction (no DDH; commitments are binding by
// collision-resistance of cSHAKE256 and hiding by the secret blinding
// randomness mixed into the cSHAKE256 absorb). The substitution is
// faithful for the dealerless-setup property: each party's polynomial
// commitments suffice to verify that the share envelope it distributes
// at Round 1 is consistent with a polynomial of the correct degree,
// and any complaint emitted at Round 2 carries identifiable evidence
// against a malicious dealer.
// randomness mixed into the cSHAKE256 absorb). IMPORTANT: hash
// commitments are NOT homomorphic, so unlike Feldman/Schoenmakers a
// recipient CANNOT verify its share against the commitments without the
// dealer's opening — and the opening includes the constant term m_i.
// This is why the production path defers share verification (see the
// VERIFIABILITY and SECURITY sections below); the "publicly verifiable"
// property holds in full only on the open-reveal (test) path.
//
// Round structure (n parties, t-of-n threshold, seed_size L = 96 or
// 128 bytes):
@@ -84,127 +88,105 @@ package magnetar
// carrying the per-recipient blob).
//
// Round 2 — every party j ∈ [1..n]:
// - For each i ∈ [1..n], receive σ_{i→j} from i alongside
// i's published commitments {C_{i,b,d}} and i's reveal payload
// (the blindings ρ_{i,b,d}). Reconstruct the polynomial value at
// x=j from i's reveal and check it byte-equals σ_{i→j}[b]. If
// not, j publishes a complaint blob carrying i's (σ, ρ)
// inconsistency — any third party verifies. Honest parties slash
// the malicious party out of the qualified set Q.
// - Aggregate: party j's final Shamir share is
// σ_j[b] = Σ_{i ∈ Q} σ_{i→j}[b] mod 257 for each b.
// - Master M is implicitly Σ_{i ∈ Q} m_i mod 257; nobody computes
// it. The aggregate share σ_j is the Lagrange evaluation at j of
// the implicit master polynomial F_b(x) = Σ_{i ∈ Q} f_{i,b}(x).
// - The aggregate share σ_j is the Lagrange evaluation at j of the
// implicit master polynomial F_b(x) = Σ_{i ∈ Q} f_{i,b}(x), whose
// constant term is M[b] = Σ_{i ∈ Q} m_i[b].
// - SHARE VERIFICATION: with hash commitments, a recipient CANNOT
// non-interactively check σ_{i→j} against {C_{i,b,d}} without i's
// opening, and the opening includes the constant term m_i. So the
// PRODUCTION path (RunDKG) does NOT verify shares at DKG time and
// does NOT publish reveals; malformed shares are caught at sign
// time (THBS-SE commit binding) and via a complaint that reveals
// only the disputed recipient's share value. The OPEN-REVEAL test
// path verifies fully against published reveals (and thereby
// reveals the master). See RunDKG's HONEST LIMITATIONS.
//
// Round 3 — every party j ∈ [1..n]:
// - Each party publishes its index j and pk-derivation contribution
// PK_i = pk_of(KeyFromSeed(m_i)) only for AUDIT (one half of the
// protocol: we want a single PK after aggregation). The actual
// protocol pk is derived from a Lagrange reconstruction of the
// master:
// M[b] = Σ_{j ∈ R} λ_j · σ_j[b] mod 257
// where R is any t-subset of the qualified set. Per FIPS 205
// §10.1, KeyFromSeed(M) is deterministic. Any party (or any
// observer holding R, σ_j's, and the public eval points) computes
// PK without ever holding M outside the derivation closure.
// PK derivation (whoever calls VerifyDKGTranscript):
// - pk is derived from a Lagrange reconstruction of the master:
// M[b] = Σ_{j ∈ R} λ_j · σ_j[b] mod 257, R a t-subset of Q.
// Per FIPS 205 §10.1, KeyFromSeed(M) is deterministic. Computing
// pk REQUIRES reconstructing M (a hash tree over M); there is no
// way around it without TEE/MPC. The reconstruction is transient,
// internal, and not published — but it IS a reconstruction.
//
// =====================================================================
// THE NO-MASTER-IN-MEMORY DISCIPLINE
// ON "NO MASTER IN MEMORY" (the earlier claim, corrected)
// =====================================================================
//
// During Rounds 1-3 of runDKG, NO party's process memory ever holds
// the byte vector M. Each party's heap contains only:
// The production transcript hides the master from OBSERVERS (no
// reveals). It does NOT make it true that "no party ever holds M":
// deriveDKGPublicKey reconstructs M to compute pk. The earlier banner's
// "NO-MASTER-IN-MEMORY DISCIPLINE" rested on naming a buffer
// `lagrangeScratch` instead of `seed` — a naming convention, not a
// security property. The buffer name is incidental. What is real:
//
// (a) Its own m_i ∈ GF(257)^L — known to that party alone.
// (b) The shares σ_{i→j} it sent + the shares it received from
// others.
// (c) The aggregated σ_j after Round 2.
// - RunDKG's transcript carries no constant-term reveals, so M is not
// reconstructible from the wire (this IS a real improvement over
// the old open-reveal-only design).
// - pk derivation reconstructs M transiently at one party and
// zeroizes it (inherent SLH-DSA cost; not eliminated by naming).
//
// The single point at which M could conceptually be assembled is in
// the PK-derivation step, where the protocol output pk must match
// KeyFromSeed(M). We use a special derivation closure that:
//
// - Lagrange-reconstructs M into a scratch buffer
// `lagrangeScratch`.
// - Immediately feeds `lagrangeScratch` to KeyFromSeed (which
// consumes the buffer via slhdsa.DeriveKey and produces the
// bytes of the FIPS 205 public key).
// - Zeroizes `lagrangeScratch`.
// - Returns ONLY the public key bytes — never the master.
//
// This is the same "transient seed at the public combiner" pattern the
// THBS-SE Combine path uses pre-strict-atom (i.e. v1.0); the dealerless
// setup variant inherits the same discipline. The strict-atom Combine
// path (thbsse_assemble.go) tightens this to never-name-master-as-
// variable for the SIGN side of the protocol; the SETUP side
// (this file) still reconstructs M transiently into one named buffer
// at PK derivation, with the buffer zeroized at function exit. The
// strict-atom discipline of the SIGN path is unaffected by this setup
// step — the buffer here is named `lagrangeScratch` rather than any
// of the v1.0 master-naming patterns (sk_seed, sk_prf, SK.seed, SK.prf).
//
// Production deployments that want to eliminate this last transient
// reconstruction route the PK derivation through a TEE-attested
// host (sibling primitive at luxfi/threshold/protocols/slhdsa-tee) or
// through a multi-party SHAKE evaluation (open research, multi-second
// per setup). Both are sibling primitives to magnetar and live in
// their own slot.
// To guarantee no party holds M even for pk derivation, use the TEE
// path (sibling primitive at luxfi/threshold/protocols/slhdsa-tee) or
// the dealer path (NewThbsSeKey, dealer-in-TCB-for-setup-only). A
// multi-party SHAKE evaluation that derives pk without reconstructing M
// is open research (multi-second per setup).
//
// =====================================================================
// VERIFIABILITY
// =====================================================================
//
// Any third party with the published Round-1 commitments and the
// Round-2 reveals verifies the setup transcript via:
//
// VerifyDKGTranscript(transcript) -> (qualifiedSet, pk, error)
//
// which:
// - For each party i and each polynomial coefficient (b, d),
// recomputes C_{i,b,d} from i's revealed (ρ_{i,b,d}, coeff_value)
// and checks byte-equality with i's published commitment.
// - For each (i, j) pair, evaluates f_{i,b}(j) from i's revealed
// coefficients and checks byte-equality with σ_{i→j}[b].
// - Drops any party with a mismatch from Q.
// - If |Q| < t, returns an error (DKG failed; restart).
// - Otherwise, recomputes pk from Lagrange interpolation as above.
// dispatches on transcript type:
//
// - PRODUCTION transcript (no reveals): verifies commitment shape +
// setup binding + received-share shape, qualifies every well-shaped
// party (it CANNOT verify shares against hash commitments without
// the reveals), and derives pk. Malformed-share detection is
// deferred to sign-time commit binding + the complaint flow.
//
// - OPEN-REVEAL transcript (TEST/KAT): additionally re-derives every
// commitment from the published reveals and checks every received
// share against the revealed polynomial, dropping inconsistent
// parties. This path reveals the master.
//
// =====================================================================
// SECURITY ARGUMENT (informal)
// SECURITY ARGUMENT (informal) --- and its limits
// =====================================================================
//
// Adversary controls T = {i : party_i is corrupt} with |T| ≤ t-1.
//
// - Secrecy: The adversary's view of an honest party h ∈ [1..n] \ T
// consists of the (t-1) shares σ_{h→i} for i ∈ T. These are
// uniform Shamir leaves of f_{h,b}, giving zero information about
// m_h = f_{h,b}(0) by Shamir info-theoretic security over GF(257).
// Therefore the adversary's view of the master M = Σ_i m_i is
// uniform on GF(257)^L conditioned on the T-contributions, which
// the adversary chose. Since at least one honest party exists in
// [1..n] \ T (|T| ≤ t-1 < n), the master is uniformly distributed
// in the adversary's view.
// - Secrecy (PRODUCTION path only): if no honest party publishes its
// constant term (RunDKG: nobody publishes reveals), the adversary's
// view of an honest party h consists of the ≤(t-1) shares σ_{h→i}
// for i ∈ T. These are uniform Shamir leaves of f_{h,b}, giving
// zero information about m_h = f_{h,b}(0) by Shamir info-theoretic
// security over GF(257). Hence M = Σ_i m_i is uniform in the
// adversary's view. THIS ARGUMENT FAILS for the open-reveal path,
// where every m_i is published and M is trivially reconstructible.
// (It is also NOT mechanized; see PROOF-CLAIMS.md.)
//
// - Correctness: Each party's polynomial f_{i,b} has constant term
// m_i[b]. Aggregating across i ∈ Q, F_b(x) = Σ_{i ∈ Q} f_{i,b}(x)
// has constant term Σ_{i ∈ Q} m_i[b] = M[b]. Therefore the
// - Correctness: Each f_{i,b} has constant term m_i[b]. Aggregating,
// F_b(x) = Σ_{i ∈ Q} f_{i,b}(x) has constant term M[b], so the
// aggregate shares σ_j = F_b(j) Lagrange-interpolate to M at x=0.
//
// - Robustness against malicious commitments: a malicious party
// publishing a commitment that does not open to a degree-(t-1)
// polynomial is detected at Round 2 by any honest verifier. The
// malicious party is excluded from Q; the protocol proceeds with
// the remaining honest contributions. As long as |Q| ≥ t, the
// final shares Lagrange-interpolate to a valid master.
// - Robustness against malicious dealers: DELIVERED ONLY on the
// open-reveal path (which detects a non-opening commitment at
// verify time). The PRODUCTION path does NOT deliver it: hash
// commitments are not openable without revealing m_i, so a
// malicious dealer's bad share is caught only later, at THBS-SE
// sign time (commit binding) or via a complaint. For adversarial
// committees, prefer the dealer path or the TEE pool. This limit is
// stated in RunDKG's HONEST LIMITATIONS, not hidden.
//
// - Equivalence to dealer: at protocol termination, the aggregate
// shares σ_j byte-equal the dealer-path shares that would have
// been produced by a (hypothetical) dealer who sampled M = Σ m_i
// and ran thbsseDealRandomGF on M with coefficients Σ c_{i,b,d}.
// The two paths are operationally indistinguishable to anyone
// holding (PK, [σ_j], setup_tr) — only the WHO-HOLDS-M property
// differs.
// - Equivalence to dealer: the aggregate shares σ_j byte-equal the
// dealer-path shares for the same implicit master + coefficient
// distribution (TestPVSS_DKG_ByteCompatWithDealerPath, open-reveal
// path). The two paths are wire-indistinguishable; they differ in
// who holds M and in robustness.
//
// =====================================================================
// CITATIONS
@@ -653,30 +635,32 @@ func (st *PVSSPartyState) ShareTo(j uint32) ([]uint16, error) {
return out, nil
}
// RevealMsg extracts the party's Round-2 reveal broadcast. After
// publishing this, any third party can verify the party's distributed
// shares against the Round-1 commits.
// RevealMsg extracts a party's FULL Round-2 reveal: every polynomial
// coefficient INCLUDING the constant term m_i[b], plus the blindings.
//
// Note that publishing the polynomial coefficients (including the
// constant term m_i[b]) at Round 2 DOES reveal the party's
// contribution to the master. This is the standard DKG pattern:
// secrecy of the master M = Σ m_i depends on at least one honest
// party REFUSING to reveal its m_i. The Round-2 reveal is only
// invoked on parties suspected of misbehavior (i.e. parties who
// distributed shares inconsistent with their commits). In an honest
// run, NO Round-2 reveal is needed for the protocol to terminate —
// the shares + commits suffice for verification via the byte-equality
// check at recipient j: f_{i,b}(j) computed by recipient against the
// commit C_{i,b,0} on j's row in i's recipientCommit grid.
// !!! THIS LEAKS THE CONTRIBUTION. !!!
//
// However, our reference DKG runs the FULL reveal at Round 2 for
// simplicity: every party publishes their coefficients + blindings,
// every other party verifies. In production deployments where
// secrecy of m_i must be preserved post-DKG, the Round-2 reveal
// becomes conditional (issued only against a published complaint).
// The reference variant in this file is the "open-reveal" mode; the
// production deployment can switch to "complaint-conditional reveal"
// without changing the wire shape of the share envelope.
// PolyCoeffs[b][0] == m_i[b] is the party's contribution to the
// master M = sum_i m_i. If every party publishes its RevealMsg (the
// "open-reveal" mode), then M is reconstructible by ANY observer of
// the transcript, not merely by t-1 colluding insiders. A transcript
// that contains every party's RevealMsg has NO master secrecy.
//
// Therefore this method is for the TEST / KAT / complaint paths only:
//
// - The open-reveal simulation `RunDKGSimulationOpenRevealTestOnly`
// (test/KAT reproducibility; produces a master-revealing
// transcript) calls it for every party.
// - The complaint flow may call it for a SINGLE accused party whose
// misbehavior has been recorded (`ComplaintReveal`). Even there,
// publishing the constant term sacrifices that party's
// contribution secrecy; a sound production complaint flow reveals
// only the disputed recipient's share value, not the whole
// polynomial (see the honest-limitations note on RunDKG).
//
// The PRODUCTION path (`RunDKG`) does NOT call this on the honest run:
// its transcript carries Reveals == nil so M is never reconstructible
// from it.
func (st *PVSSPartyState) RevealMsg() PVSSRevealMsg {
out := PVSSRevealMsg{
NodeID: st.NodeID,
@@ -788,44 +772,55 @@ func VerifyShareConsistency(
return failed, nil
}
// RunDKGSimulation runs an n-party PVSS-DKG protocol in a single
// process for testing and reference. The simulation:
// OpenRevealAck is a required, self-documenting barrier value that a
// caller must pass to RunDKGSimulationOpenRevealTestOnly to confirm
// it understands the resulting transcript REVEALS THE MASTER. There
// is exactly one acceptable value; passing anything else fails. This
// makes the leaking path impossible to call by accident and trivially
// greppable in a production build review
// (grep for IUnderstandThisRevealsTheMaster).
type OpenRevealAck struct{ ack string }
// AckOpenRevealRevealsMaster is the only value RunDKGSimulationOpenReveal
// TestOnly accepts. Its single field documents the hazard at the call
// site.
var AckOpenRevealRevealsMaster = OpenRevealAck{ack: "IUnderstandThisRevealsTheMaster"}
// ErrOpenRevealNotAcknowledged is returned when the open-reveal
// simulation is invoked without the explicit hazard acknowledgement.
var ErrOpenRevealNotAcknowledged = errors.New(
"magnetar/pvss-dkg: open-reveal simulation reveals the master and is TEST-ONLY; " +
"pass AckOpenRevealRevealsMaster to confirm, or use RunDKG for production")
// RunDKGSimulationOpenRevealTestOnly runs an n-party PVSS-DKG in a
// single process in OPEN-REVEAL mode.
//
// 1. Allocates n per-party RNG readers.
// 2. Each party computes its own Round-1 state (no shared state).
// 3. Each party broadcasts its public contribution + sends private
// shares to every other party.
// 4. Each party verifies received shares against received commits.
// 5. Each party publishes Round-2 reveal (open-reveal mode).
// 6. Any third party verifies the full transcript and derives the
// aggregated share envelope.
// !!! TEST / KAT ONLY. THE OUTPUT TRANSCRIPT REVEALS THE MASTER. !!!
//
// The output PVSSTranscript carries every public artifact; an auditor
// holding (committee, params, threshold, transcript) can reproduce
// the qualified set Q, the aggregated shares, and the derived public
// key.
// Every party publishes its full RevealMsg (PolyCoeffs including the
// constant terms m_i). The resulting transcript therefore lets ANY
// observer reconstruct M = sum_i m_i. This is acceptable ONLY for
// deterministic KAT replay and for exercising the verification logic
// in tests. It MUST NOT run in a production deployment. The required
// `ack` barrier makes accidental production use impossible and makes
// the call site greppable.
//
// CRITICAL INVARIANT: the master byte vector M = Σ_{i ∈ Q} m_i mod 257
// is NEVER assembled by any party's state. Each party knows only:
// - Its own m_i (= polyCoeffs[*][0]).
// - The shares σ_{i→self} received from every other party.
// - The aggregated final share σ_self after Round 2.
//
// The master is materialised only inside the PK-derivation closure
// (deriveDKGPublicKey) which is a separate sibling function the
// auditor or any third party invokes to extract the public key from
// the transcript. The party simulation in RunDKGSimulation itself
// never invokes that closure.
// For production, use RunDKG (below): its transcript carries
// Reveals == nil and M is never reconstructible from it.
//
// rngs is a slice of n io.Readers, one per party. Pass nil to use
// crypto/rand.Reader for all parties. Tests use bytes.NewReader of a
// deterministic vector for KAT replay.
func RunDKGSimulation(
func RunDKGSimulationOpenRevealTestOnly(
ack OpenRevealAck,
params *Params,
threshold int,
committee []NodeID,
rngs []io.Reader,
) (*PVSSTranscript, error) {
if ack != AckOpenRevealRevealsMaster {
return nil, ErrOpenRevealNotAcknowledged
}
if err := params.Validate(); err != nil {
return nil, err
}
@@ -943,6 +938,158 @@ func RunDKGSimulation(
return tr, nil
}
// RevealsMaster reports whether this transcript contains the full
// polynomial reveals (constant terms m_i) that make the master
// M = sum_i m_i reconstructible by any observer. A production
// transcript MUST return false. The open-reveal test transcript
// returns true.
//
// A transcript reveals the master iff ANY party's reveal carries a
// non-empty constant-term coefficient vector.
func (tr *PVSSTranscript) RevealsMaster() bool {
for i := range tr.Reveals {
for b := range tr.Reveals[i].PolyCoeffs {
if len(tr.Reveals[i].PolyCoeffs[b]) > 0 {
return true
}
}
}
return false
}
// RunDKG runs the PRODUCTION n-party PVSS-DKG. Unlike the open-reveal
// test simulation, the transcript it returns carries Reveals == nil:
// no party publishes its polynomial constant term, so the master
// M = sum_i m_i is NOT reconstructible from the transcript by any
// observer. `tr.RevealsMaster()` is false for this output.
//
// HONEST LIMITATIONS (read before deploying):
//
// 1. SLH-DSA group public-key derivation inherently needs the master.
// pk = SLH-DSA.PK(M) is a hash tree over M; there is no way to
// compute it from shares without either reconstructing M at some
// party or running full MPC over the SHAKE hash tree (open
// research). RunDKG reconstructs M transiently inside
// deriveDKGPublicKey to compute pk and zeroizes it. That single
// reconstruction is the inherent cost; it is NOT published. If you
// need NO party to ever hold M (not even transiently for pk
// derivation), you must run the TEE-attested path
// (luxfi/threshold/protocols/slhdsa-tee) or the dealer path
// (NewThbsSeKey) where the dealer is in the TCB for setup only.
//
// 2. With hash-based commitments (cSHAKE256 over coefficients), a
// recipient CANNOT non-interactively verify a received share
// against the public commitments without the dealer's opening,
// and the opening includes the constant term. So RunDKG does NOT
// exclude malicious dealers at DKG time (it cannot, soundly,
// without revealing m_i or switching to group-homomorphic /
// encrypted-share+NIZK commitments — a separate construction).
// Malformed-share detection is DEFERRED to:
// - THBS-SE Combine's per-party commit re-derivation at sign
// time, which drops a tampered share and emits slashable
// evidence (TestThbsSE_RejectOversizedShareWireSize /
// TestThbsSE_RejectTamperedShareCommitMismatch);
// - the complaint flow, where an accused party reveals ONLY the
// disputed recipient's share value (never the constant term).
// Because robust DKG-time dealer exclusion is NOT delivered here,
// RunDKG is the no-leak setup path but NOT a robust-against-
// malicious-dealers path. For adversarial committees, prefer the
// dealer path or the TEE pool. This is labeled, not hidden.
//
// The production transcript is consumed by
// NewThbsSeKeyFromDealerlessDKG, which verifies commitment shape +
// setup binding (it cannot verify shares without reveals) and derives
// the share envelopes + group PK.
//
// rngs is a slice of n io.Readers, one per party. Pass nil for
// crypto/rand.
func RunDKG(
params *Params,
threshold int,
committee []NodeID,
rngs []io.Reader,
) (*PVSSTranscript, error) {
if err := params.Validate(); err != nil {
return nil, err
}
n := len(committee)
if threshold < 1 || n < threshold {
return nil, ErrInvalidThreshold
}
if n > MaxCommittee257 {
return nil, ErrCommitteeTooLarge
}
if rngs != nil && len(rngs) != n {
return nil, fmt.Errorf("magnetar/pvss-dkg: rngs length %d does not match committee size %d", len(rngs), n)
}
for i := 1; i < n; i++ {
if bytes.Compare(committee[i-1][:], committee[i][:]) >= 0 {
return nil, errors.New("magnetar/pvss-dkg: committee not sorted ascending or contains duplicates")
}
}
// Round 1: each party computes its own state; only the PUBLIC
// commitments are collected for the transcript.
states := make([]*PVSSPartyState, n)
contribs := make([]PVSSPublicContribution, n)
for i := 0; i < n; i++ {
var rng io.Reader
if rngs != nil {
rng = rngs[i]
}
st, err := NewPVSSPartyState(params, threshold, committee, uint32(i+1), rng)
if err != nil {
return nil, fmt.Errorf("magnetar/pvss-dkg: party %d Round-1 setup: %w", i+1, err)
}
states[i] = st
contribs[i] = st.PublicContribution()
}
// Round 2 (private share distribution): each recipient stores the
// shares it received. These are published as part of the transcript
// (they are Shamir leaves, which leak nothing about any individual
// m_i below the threshold, and are needed to aggregate the final
// shares). NOTE: a recipient publishing a share row reveals only
// other parties' leaves AT THAT RECIPIENT'S point — not constant
// terms.
receivedShares := make([][][]uint16, n)
for j := 0; j < n; j++ {
receivedShares[j] = make([][]uint16, n)
for i := 0; i < n; i++ {
row, err := states[i].ShareTo(uint32(j + 1))
if err != nil {
return nil, fmt.Errorf("magnetar/pvss-dkg: party %d ShareTo(%d): %w", i+1, j+1, err)
}
receivedShares[j][i] = row
}
}
setupTr := pvssSetupTranscript(params, threshold, committee)
// Production transcript: Reveals is nil. The master is NOT
// reconstructible from this transcript.
tr := &PVSSTranscript{
Params: params,
Committee: committee,
Threshold: threshold,
Contributions: contribs,
Reveals: nil,
ReceivedShares: receivedShares,
SetupTr: setupTr,
}
for i := 0; i < n; i++ {
zeroizePartyState(states[i])
}
if tr.RevealsMaster() {
// Defense in depth: a production transcript that somehow
// carries constant-term reveals must never be returned.
return nil, errors.New("magnetar/pvss-dkg: internal error: production transcript reveals master")
}
return tr, nil
}
// AggregateShareEnvelope aggregates the received shares for party j
// across the qualified set Q. Returns the GF(257) share vector
// σ_j[b] = Σ_{i ∈ Q} σ_{i→j}[b] mod 257. This is the input to the
@@ -972,16 +1119,31 @@ func (*Params) committeeSize(committee []NodeID) int {
return len(committee)
}
// VerifyDKGTranscript is the public auditor's entry point. Given a
// PVSSTranscript, recomputes the qualified set Q via per-party
// commitment + share verification, computes the FIPS 205 public key
// via Lagrange interpolation of the master master across any t
// qualified shares, and returns (Q, pk, error).
// VerifyDKGTranscript is the public auditor's entry point. It returns
// the qualified set Q, the derived FIPS 205 group public key, and an
// error. It dispatches on the transcript type:
//
// The master is reconstructed transiently inside a closure named
// lagrangeScratch, immediately fed to KeyFromSeed, and zeroized at
// the closure boundary. No party state outside this closure ever
// holds the master.
// - PRODUCTION transcript (tr.Reveals == nil, tr.RevealsMaster() ==
// false): verifies commitment shape + setup binding + received-
// share shape. It CANNOT verify shares against commitments
// (hash commitments are not openable without the constant-term
// reveal), so it does NOT exclude malicious dealers at this stage:
// every party with well-shaped commitments is qualified, and
// malformed-share detection is deferred to THBS-SE Combine's
// sign-time commit binding + the complaint flow. This is the
// no-leak path; see RunDKG's HONEST LIMITATIONS.
//
// - OPEN-REVEAL transcript (tr.Reveals populated, tr.RevealsMaster()
// == true): the TEST/KAT path. It additionally re-derives every
// commitment from the published reveals and checks every received
// share against the revealed polynomial, excluding any party whose
// reveal is inconsistent. This path REVEALS THE MASTER and is for
// tests / KATs only.
//
// In both cases the group public key is derived in deriveDKGPublicKey,
// which transiently reconstructs the master to compute pk and zeroizes
// it (the inherent SLH-DSA cost; see RunDKG limitation 1). The
// reconstruction is internal to this function and is never published.
func VerifyDKGTranscript(tr *PVSSTranscript) (map[uint32]struct{}, *PublicKey, error) {
if tr == nil {
return nil, nil, errors.New("magnetar/pvss-dkg: nil transcript")
@@ -996,9 +1158,6 @@ func VerifyDKGTranscript(tr *PVSSTranscript) (map[uint32]struct{}, *PublicKey, e
if len(tr.Contributions) != n {
return nil, nil, ErrPVSSWrongShape
}
if len(tr.Reveals) != n {
return nil, nil, ErrPVSSWrongShape
}
if len(tr.ReceivedShares) != n {
return nil, nil, ErrPVSSWrongShape
}
@@ -1014,6 +1173,11 @@ func VerifyDKGTranscript(tr *PVSSTranscript) (map[uint32]struct{}, *PublicKey, e
return nil, nil, errors.New("magnetar/pvss-dkg: transcript setup_tr mismatch")
}
openReveal := tr.RevealsMaster()
if openReveal && len(tr.Reveals) != n {
return nil, nil, ErrPVSSWrongShape
}
qualified := make(map[uint32]struct{}, n)
for i := 0; i < n; i++ {
qualified[uint32(i+1)] = struct{}{}
@@ -1023,6 +1187,34 @@ func VerifyDKGTranscript(tr *PVSSTranscript) (map[uint32]struct{}, *PublicKey, e
delete(qualified, uint32(i+1))
continue
}
// Commitment shape check applies to both paths: every party
// must publish n_coeff = threshold commitments per byte.
if !pvssCommitShapeOK(tr.Params, tr.Threshold, tr.Contributions[i]) {
delete(qualified, uint32(i+1))
continue
}
// Received-share shape check (both paths).
for j := 0; j < n; j++ {
if len(tr.ReceivedShares[j]) <= i || len(tr.ReceivedShares[j][i]) != tr.Params.SeedSize {
delete(qualified, uint32(i+1))
break
}
}
if _, still := qualified[uint32(i+1)]; !still {
continue
}
if !openReveal {
// Production path: hash commitments cannot be opened without
// the constant-term reveal, so no DKG-time share verification
// is possible. A well-shaped party is qualified; malformed
// shares are caught at sign time (THBS-SE commit binding) and
// via the complaint flow. See RunDKG limitation 2.
continue
}
// Open-reveal path (TEST/KAT): full verification against the
// published reveals.
if tr.Reveals[i].NodeID != tr.Committee[i] {
delete(qualified, uint32(i+1))
continue
@@ -1036,10 +1228,6 @@ func VerifyDKGTranscript(tr *PVSSTranscript) (map[uint32]struct{}, *PublicKey, e
continue
}
for j := 0; j < n; j++ {
if len(tr.ReceivedShares[j]) <= i {
delete(qualified, uint32(i+1))
break
}
failedBytes, err := VerifyShareConsistency(tr.Params, tr.Reveals[i], uint32(j+1), tr.ReceivedShares[j][i])
if err != nil {
return nil, nil, err
@@ -1062,17 +1250,45 @@ func VerifyDKGTranscript(tr *PVSSTranscript) (map[uint32]struct{}, *PublicKey, e
return qualified, pk, nil
}
// deriveDKGPublicKey is the public-key-derivation closure. It is the
// single point in the PVSS-DKG path where the master byte vector is
// transiently assembled — into the local variable `lagrangeScratch`,
// which is consumed by KeyFromSeed and zeroized immediately.
// pvssCommitShapeOK reports whether a public contribution has the
// canonical commitment shape: SeedSize byte-rows, each with exactly
// `threshold` 32-byte commitments. Pure shape check (no secret access).
func pvssCommitShapeOK(params *Params, threshold int, contrib PVSSPublicContribution) bool {
if len(contrib.Commits) != params.SeedSize {
return false
}
for b := 0; b < params.SeedSize; b++ {
if len(contrib.Commits[b]) != threshold {
return false
}
for d := 0; d < threshold; d++ {
if len(contrib.Commits[b][d]) != 32 {
return false
}
}
}
return true
}
// deriveDKGPublicKey computes the FIPS 205 group public key from the
// transcript. To do so it RECONSTRUCTS the master byte vector into
// `lagrangeScratch`, feeds it to KeyFromSeed, and zeroizes it.
//
// The buffer is named `lagrangeScratch` (not any of the v1.0 master-
// naming patterns) so the strict-atom grep audit of THBSSE-Combine
// continues to pass; the strict-atom discipline applies to the SIGN
// side of the protocol, and the SETUP side's transient buffer here
// is at a strictly weaker discipline (transient, named non-canonically,
// zeroized at scope exit).
// This reconstruction is PK-derivation-only and is INHERENT, not a
// shortcut: pk = SLH-DSA.PK(M) is a hash tree over M, so there is no
// way to derive pk from shares without reconstructing M somewhere (or
// running full MPC over the SHAKE hash tree — open research). The
// reconstruction is internal to this function and is NEVER published;
// only the public key bytes are returned. It runs at whoever calls
// VerifyDKGTranscript (an auditor or any party deriving the group pk).
//
// This is the same fundamental barrier as THBS-SE Combine: producing
// or deriving anything SLH-DSA-shaped from a shared seed touches the
// seed. Deployments that must guarantee NO party ever holds M (not
// even transiently for pk derivation) route this through the
// TEE-attested path (luxfi/threshold/protocols/slhdsa-tee) or use the
// dealer path. The buffer name `lagrangeScratch` is incidental; it is
// not a security property.
func deriveDKGPublicKey(tr *PVSSTranscript, qualified map[uint32]struct{}) (*PublicKey, error) {
L := tr.Params.SeedSize
n := len(tr.Committee)
ref/go/pkg/magnetar/pvss_dkg_test.go
+131 -35
View File
@@ -19,25 +19,32 @@ import (
// pvss_dkg_test.go --- Tests for the dealerless PVSS-DKG path.
//
// Closes BLOCKERS.md::MAGNETAR-PVSS-DKG-V11. The headline gates are:
// Two transcript types are under test:
//
// - TestPVSS_DKG_NoSinglePartyHoldsMaster: exercise the full DKG
// and assert no party's memory ever contains the master byte
// vector. The master can only be derived by an external auditor
// invoking VerifyDKGTranscript; in the simulation, every party's
// state is bounded to (own m_i, received shares, aggregated share).
// - PRODUCTION (RunDKG): no constant-term reveals; the master is NOT
// reconstructible from the transcript.
// - OPEN-REVEAL (RunDKGSimulationOpenRevealTestOnly): publishes every
// m_i; the master IS reconstructible. TEST/KAT only.
//
// The headline gates are:
//
// - TestPVSS_DKG_ProductionTranscriptHidesMaster: the production
// transcript hides the master (regression gate for the P2 leak
// fix); the open-reveal transcript reveals it (contrast).
//
// - TestPVSS_DKG_ByteCompatWithDealerPath: compare the dealerless-
// produced KeyShare envelopes against the dealer-path envelopes
// for the same implicit master. Wire-byte equality.
// for the same implicit master. Wire-byte equality. Uses the
// open-reveal path because it inspects the polynomial reveals.
//
// - TestPVSS_DKG_AdversarialReveals: t-1 corrupted parties reveal
// their shares; remaining honest party's master contribution
// stays uniform in the adversary's view.
// their shares; the partial sum does not equal the master (entropy
// sanity; open-reveal path).
//
// - TestPVSS_DKG_RobustnessAgainstMaliciousCommitments: wrong
// commitments are detected + rejected; the protocol terminates
// with the malicious party excluded from Q.
// - TestPVSS_DKG_RobustnessAgainstMaliciousCommitments: in the
// OPEN-REVEAL path, wrong commitments are detected + rejected. (The
// production path defers malformed-share detection to sign-time
// commit binding; see RunDKG's HONEST LIMITATIONS.)
// pvssTestModes is the set of FIPS 205 parameter sets the PVSS-DKG
// path supports. All three SHAKE modes share the same byte-share
@@ -59,23 +66,17 @@ func makePVSSCommittee(t *testing.T, n int) []NodeID {
return out
}
// TestPVSS_DKG_NoSinglePartyHoldsMaster is the no-master-in-memory
// gate. The test runs a full PVSS-DKG and asserts:
// TestPVSS_DKG_OpenRevealPartyContributionsDistinct exercises the
// OPEN-REVEAL test path (which DOES reveal the master — see
// RunDKGSimulationOpenRevealTestOnly) and asserts the weaker property
// that no single party's contribution m_i happens to byte-equal the
// aggregate master (entropy sanity), plus the source-hygiene AST check.
//
// 1. NewPVSSPartyState returns a state whose polyCoeffs[*][0] is
// the party's m_i, distinct from the eventual master.
// 2. The simulation runner zeroizes per-party state at termination.
// 3. The transcript's ReceivedShares are independent random-looking
// vectors (no single share row is the master).
// 4. The only path to the master is via VerifyDKGTranscript's
// deriveDKGPublicKey closure, which materialises lagrangeScratch
// into a single local buffer and zeroizes it immediately.
//
// The test also AST-walks the pvss_dkg.go source file to assert no
// public function returns a [seed_size]byte master, and no field of
// PVSSPartyState exposes the master in its name. This is the structural
// counterpart to the strict-atom AST gate for the SIGN side.
func TestPVSS_DKG_NoSinglePartyHoldsMaster(t *testing.T) {
// NOTE: this test does NOT establish master secrecy. The open-reveal
// transcript publishes every m_i, so M is trivially reconstructible.
// The production no-leak property is tested by
// TestPVSS_DKG_ProductionTranscriptHidesMaster.
func TestPVSS_DKG_OpenRevealPartyContributionsDistinct(t *testing.T) {
t.Parallel()
for _, mode := range pvssTestModes {
@@ -89,7 +90,7 @@ func TestPVSS_DKG_NoSinglePartyHoldsMaster(t *testing.T) {
)
committee := makePVSSCommittee(t, n)
tr, err := RunDKGSimulation(params, threshold, committee, nil)
tr, err := RunDKGSimulationOpenRevealTestOnly(AckOpenRevealRevealsMaster, params, threshold, committee, nil)
if err != nil {
t.Fatalf("RunDKGSimulation: %v", err)
}
@@ -132,6 +133,95 @@ func TestPVSS_DKG_NoSinglePartyHoldsMaster(t *testing.T) {
}
}
// TestPVSS_DKG_ProductionTranscriptHidesMaster is the regression gate
// for the open-reveal leak fix (P2). It asserts:
//
// 1. The PRODUCTION transcript (RunDKG) carries NO constant-term
// reveals: tr.Reveals is empty and tr.RevealsMaster() is false.
// An observer of the production transcript therefore cannot
// reconstruct Sum m_i (= M) from polynomial reveals — the leak
// vector is gone.
// 2. The production transcript still derives a valid group public key
// and wire-compatible shares (VerifyDKGTranscript + the key
// constructor succeed) WITHOUT any master reveal.
// 3. For contrast, the OPEN-REVEAL transcript DOES reveal the master
// (RevealsMaster() == true), confirming the two paths differ in
// exactly the leak property — the fix is real, not cosmetic.
// 4. The open-reveal simulation refuses to run without the explicit
// hazard acknowledgement barrier.
func TestPVSS_DKG_ProductionTranscriptHidesMaster(t *testing.T) {
t.Parallel()
for _, mode := range pvssTestModes {
mode := mode
t.Run(mode.String(), func(t *testing.T) {
t.Parallel()
params := MustParamsFor(mode)
const (
n = 5
threshold = 3
)
committee := makePVSSCommittee(t, n)
// (1) Production transcript hides the master.
prod, err := RunDKG(params, threshold, committee, nil)
if err != nil {
t.Fatalf("RunDKG: %v", err)
}
if prod.RevealsMaster() {
t.Fatalf("production transcript reveals the master")
}
if len(prod.Reveals) != 0 {
t.Fatalf("production transcript carries %d reveals; want 0", len(prod.Reveals))
}
// Defense in depth: scan every reveal slot for a constant
// term, mirroring the on-wire reconstructability the fix
// removes.
for i := range prod.Reveals {
for b := range prod.Reveals[i].PolyCoeffs {
if len(prod.Reveals[i].PolyCoeffs[b]) > 0 {
t.Fatalf("production transcript leaks constant term at party %d byte %d", i, b)
}
}
}
// (2) Production transcript still derives a usable key with
// NO master reveal.
qualified, pk, err := VerifyDKGTranscript(prod)
if err != nil {
t.Fatalf("VerifyDKGTranscript(production): %v", err)
}
if len(qualified) < threshold {
t.Fatalf("production qualified set %d < threshold %d", len(qualified), threshold)
}
if pk == nil || len(pk.Bytes) != params.PublicKeySize {
t.Fatalf("production pk has wrong shape: %v", pk)
}
if _, err := NewThbsSeKeyFromDealerlessDKG(prod); err != nil {
t.Fatalf("NewThbsSeKeyFromDealerlessDKG(production): %v", err)
}
// (3) Contrast: the open-reveal transcript DOES reveal it.
open, err := RunDKGSimulationOpenRevealTestOnly(
AckOpenRevealRevealsMaster, params, threshold, committee, nil)
if err != nil {
t.Fatalf("RunDKGSimulationOpenRevealTestOnly: %v", err)
}
if !open.RevealsMaster() {
t.Fatalf("open-reveal transcript does NOT reveal the master; the two paths are indistinguishable")
}
// (4) The open-reveal path refuses without the ack barrier.
if _, err := RunDKGSimulationOpenRevealTestOnly(
OpenRevealAck{}, params, threshold, committee, nil); err == nil {
t.Fatalf("open-reveal simulation ran without the hazard acknowledgement")
} else if err != ErrOpenRevealNotAcknowledged {
t.Fatalf("want ErrOpenRevealNotAcknowledged, got %v", err)
}
})
}
}
// matchesMaster checks whether a reveal's polynomial constant-term
// vector (party's m_i) byte-equals the supplied master.
func matchesMaster(reveal PVSSRevealMsg, master []uint16) bool {
@@ -298,7 +388,7 @@ func TestPVSS_DKG_ByteCompatWithDealerPath(t *testing.T) {
committee := makePVSSCommittee(t, n)
// Run dealerless DKG.
tr, err := RunDKGSimulation(params, threshold, committee, nil)
tr, err := RunDKGSimulationOpenRevealTestOnly(AckOpenRevealRevealsMaster, params, threshold, committee, nil)
if err != nil {
t.Fatalf("RunDKGSimulation: %v", err)
}
@@ -440,7 +530,7 @@ func TestPVSS_DKG_AdversarialReveals(t *testing.T) {
)
committee := makePVSSCommittee(t, n)
tr, err := RunDKGSimulation(params, threshold, committee, nil)
tr, err := RunDKGSimulationOpenRevealTestOnly(AckOpenRevealRevealsMaster, params, threshold, committee, nil)
if err != nil {
t.Fatalf("RunDKGSimulation: %v", err)
}
@@ -675,9 +765,15 @@ func TestPVSS_DKG_EndToEnd_SignAndVerify(t *testing.T) {
)
committee := makePVSSCommittee(t, n)
tr, err := RunDKGSimulation(params, threshold, committee, nil)
// Production no-leak path: RunDKG emits a transcript with no
// constant-term reveals; the master is not reconstructible
// from it, yet the derived key signs and verifies.
tr, err := RunDKG(params, threshold, committee, nil)
if err != nil {
t.Fatalf("RunDKGSimulation: %v", err)
t.Fatalf("RunDKG: %v", err)
}
if tr.RevealsMaster() {
t.Fatalf("production RunDKG transcript reveals the master")
}
key, err := NewThbsSeKeyFromDealerlessDKG(tr)
if err != nil {
@@ -789,7 +885,7 @@ func TestPVSS_DKG_TranscriptTamperDetection(t *testing.T) {
threshold = 3
)
committee := makePVSSCommittee(t, n)
tr, err := RunDKGSimulation(params, threshold, committee, nil)
tr, err := RunDKGSimulationOpenRevealTestOnly(AckOpenRevealRevealsMaster, params, threshold, committee, nil)
if err != nil {
t.Fatalf("RunDKGSimulation: %v", err)
}
@@ -832,7 +928,7 @@ func TestPVSS_DKG_RaceClean(t *testing.T) {
wg.Add(1)
go func() {
defer wg.Done()
tr, err := RunDKGSimulation(params, threshold, committee, nil)
tr, err := RunDKG(params, threshold, committee, nil)
if err != nil {
errs <- err
return
ref/go/pkg/magnetar/slhdsa_internal.go
-16
View File
@@ -710,22 +710,6 @@ func htSign(
}
}
// htRootCompute computes the hypertree root (pkRoot) given pkSeed and
// the PRF callback. Used at setup to derive the public key root from
// the same Lagrange-reconstructed material the signer uses. FIPS 205
// §9.1 Algorithm 18 (line 5).
func htRootCompute(
p *internalParams,
out []byte,
pkSeed []byte,
prfOut prfOutFn,
) {
addr := adrsBuf{}
addr.setLayerAddress(p.d - 1)
addr.setTreeAddress([3]uint32{0, 0, 0})
xmssNodeCompute(p, out, pkSeed, &addr, 0, p.hPrime, prfOut)
}
// =====================================================================
// FIPS 205 §8 — FORS sign + public-key reconstruction
// =====================================================================
ref/go/pkg/magnetar/thbsse.go
+8 -7
View File
@@ -937,13 +937,14 @@ func Combine(input ThbsSeCombineInput) (*Signature, []ThbsSeShareEvidence, error
sort.Slice(ordered, func(i, j int) bool { return ordered[i].X < ordered[j].X })
pick := ordered[:threshold]
// Strict-atom assembly: emit FIPS 205 wire bytes directly from the
// validated quorum shares via the Magnetar-internal §5-8 path
// (slhdsa_internal.go + thbsse_assemble.go). The public combiner
// runs entirely inside the strict-atom discipline; no variable in
// the call graph below this point binds the FIPS 205 master byte
// material under the names SK.seed, SK.prf, sk_seed, or sk_prf.
// See ASSEMBLE-INVARIANT.md and TestThbsSE_StrictAtom_NoTransientSeed.
// Emit FIPS 205 wire bytes from the validated quorum shares via
// the Magnetar-internal sec 5-8 path (slhdsa_internal.go +
// thbsse_assemble.go). NOTE: assembleSignatureBytes RECONSTRUCTS
// THE FIPS 205 MASTER at this public combiner (into
// `derivedMaterial`). The permissionless THBS-SE path is
// research-grade, not no-leak -- the master is resident in this
// process for one Sign call. See ASSEMBLE-INVARIANT.md and
// BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11 (OPEN).
ctx := ctxFromSlot(input.Binding)
if len(ctx) > 255 {
return nil, evidences, ErrCtxTooLong
ref/go/pkg/magnetar/thbsse_assemble.go
+39 -45
View File
@@ -3,60 +3,54 @@
package magnetar
// thbsse_assemble.go — strict-atom-assembly Combine path for THBS-SE
// at Magnetar v1.1.
// thbsse_assemble.go — THBS-SE Combine emit path.
//
// =====================================================================
// WHAT THIS FILE GIVES YOU
// HONEST SUMMARY: THIS PATH RECONSTRUCTS THE FIPS 205 MASTER
// =====================================================================
//
// A pure-Go assembleSignatureBytes that takes t verified share-share
// envelopes (the per-party (mask, masked) reveals already commit-bound
// in thbsse.go) plus the public ThbsSeKey + slot binding + message, and
// emits FIPS 205 wire-form signature bytes BYTE-IDENTICAL to circl's
// slhdsa.SignDeterministic on the SAME (sk_from_seed(S), msg, ctx)
// tuple --- WITHOUT EVER COMPOSING S OR ITS DERIVED (skSeed, skPrf)
// FRAGMENTS AS A NAMED FREE-STANDING VARIABLE.
// assembleSignatureBytes takes t verified share envelopes (the
// per-party (mask, masked) reveals commit-bound in thbsse.go) plus the
// public ThbsSeKey + slot binding + message, and emits FIPS 205
// wire-form signature bytes byte-identical to
// circl/slhdsa.SignDeterministic on the reconstructed master.
//
// The path is the strict-atom refinement promised at
// BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11. Compared to v1.0 (where the
// public combiner materialised S in a `seed []byte` local for the
// duration of one circl SignDeterministic call), v1.1:
// To do so it RECONSTRUCTS THE FULL FIPS 205 MASTER at the public
// combiner: it Lagrange-interpolates the share bytes into
// `derivedExpandInput`, SHAKE-expands that into `derivedMaterial`
// (= skSeed || skPrf || pkSeed), and drives a FIPS 205 §5--§8 walk that
// reads positional slices of `derivedMaterial`. The whole private key
// is present in the combiner's process memory for the duration of one
// Sign call. This is the SAME seed reconstruction as the older path.
//
// - Routes EVERY secret-material access through one of two opaque
// callbacks (atomPRF and atomPRFMsg).
// - The callbacks own the ONLY buffers that ever hold the
// Lagrange-interpolated bytes of the FIPS 205 master material.
// The buffers are named after the SHAKE absorb context they feed
// (e.g. prfAbsorb) and zeroized at the closure boundary.
// - The signing engine (slhdsa_internal.go) walks FIPS 205 §5 / §6 /
// §7 / §8 and assembles the signature ATOM-BY-ATOM (R, FORS sk
// leaves, FORS auth nodes, WOTS+ chain bases, XMSS auth nodes,
// hypertree XMSS layers) by INVOKING the callbacks. The engine
// itself is FIPS 205 plaintext: it never sees secret bytes outside
// the callbacks' transient scope.
// The earlier framing of this file called itself a "strict-atom"
// refinement that "never composes S as a named free-standing variable"
// and implied that buys a no-leak property over a `seed []byte` local.
// It does NOT. Not naming the buffer `seed` changes the spelling, not
// the data: `derivedMaterial` holds skSeed||skPrf||pkSeed all the same.
// There is no confidentiality property here to rely on. The
// permissionless THBS-SE path is RESEARCH-GRADE, not no-leak; see
// BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11 (OPEN) and ASSEMBLE-INVARIANT.md.
//
// =====================================================================
// THE STRICT-ATOM INVARIANT (load-bearing)
// =====================================================================
// What this path DOES give, and all it gives: the emitted signature is
// a valid FIPS 205 signature (byte-identical to the standard
// deterministic signer on the reconstructed master), so any unmodified
// verifier accepts it. That is a correctness/interop property, pinned
// by TestSlhdsaInternal_ByteEqualToCirclSign and
// TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl. It is NOT a
// no-leak property.
//
// At every line of this file:
// - No variable of any kind binds the FIPS 205 master byte material
// under a name matching the forbidden vocabulary defined in
// ASSEMBLE-INVARIANT.md (the four sentinel patterns that the
// v1.1 audit grep checks).
// - The grep is run against the raw bytes of this file (comments
// included) and MUST return zero matches. See the test gate
// TestThbsSE_StrictAtom_NoTransientSeed for the enforcement.
// - No variable holds the full reconstructed master S. The closest
// analogue --- the buffer that feeds the FIPS 205 §11.2
// `SHAKE256(pkSeed || ADRS || X)` PRF --- is named `prfAbsorb`
// and lives inside the atom callbacks for the duration of one
// SHAKE absorb call, then is zeroized.
// The signing engine (slhdsa_internal.go) walks FIPS 205 §5/§6/§7/§8
// and emits the signature by invoking two PRF/PRF_msg callbacks. The
// callbacks read the secret segments of `derivedMaterial`. Scratch
// buffers (prfAbsorb, prfMsgAbsorb) and the derived buffers are
// zeroized after use — defense-in-depth against lingering copies, NOT
// a guarantee the master was never resident.
//
// TestThbsSE_StrictAtom_NoTransientSeed (thbsse_assemble_test.go)
// enforces the discipline by parsing this file's AST and asserting
// every identifier name escapes the forbidden patterns.
// TestThbsSE_AssembleIdentHygiene is a NAME LINT over this file (it
// asserts no variable is *spelled* `seed`/`skSeed`/...). It is a style
// check, not a security property: the master is reconstructed
// regardless of naming.
//
// =====================================================================
// ALGEBRAIC LINEAGE
ref/go/pkg/magnetar/thbsse_assemble_test.go
+39 -34
View File
@@ -3,20 +3,26 @@
package magnetar
// thbsse_assemble_test.go --- the strict-atom invariant + byte-identity
// regression suite for the v1.1 Combine path.
// thbsse_assemble_test.go --- an identifier-hygiene lint + byte-identity
// regression suite for the THBS-SE Combine path.
//
// Coverage matrix:
//
// TestThbsSE_StrictAtom_NoTransientSeed
// - load-bearing AST invariant: parse thbsse_assemble.go and
// slhdsa_internal.go and assert no identifier in either file
// matches the forbidden patterns:
// TestThbsSE_AssembleIdentHygiene
// - IDENTIFIER-HYGIENE LINT (NOT a security property): parse
// thbsse_assemble.go and slhdsa_internal.go and assert no
// identifier matches the patterns:
// SK\.seed | SK\.prf | sk_seed | sk_prf
// PLUS no Go identifier named exactly:
// seed | SkSeed | SK | SkPrf | PrfKey | prfKey
// (these are the v1.0 named-variable forms the strict-atom
// invariant forbids in the assemble path).
// - This checks variable NAMES, nothing else. It does NOT show
// that the master seed is absent from memory. It IS absent as a
// variable *named* `seed`, but assembleSignatureBytes still
// reconstructs the full FIPS 205 master into the buffer
// `derivedMaterial` (skSeed||skPrf||pkSeed) at the public
// combiner — see ASSEMBLE-INVARIANT.md and
// BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11. The lint guards the
// naming convention; it is not a no-leak proof.
//
// TestSlhdsaInternal_ByteEqualToCirclSign
// - byte-identity: assemble FIPS 205 signature bytes via the
@@ -52,16 +58,17 @@ func readFileForTest(path string) ([]byte, error) {
return os.ReadFile(path)
}
// forbiddenIdentRegex captures the literal grep target from the v1.1
// blocker spec. Any identifier OR comment substring matching this
// regex is a strict-atom invariant violation IN CODE positions; we
// allow it in package-level doc comments (the leading // banner) by
// stripping comments before scanning identifiers.
// forbiddenIdentRegex captures the name-pattern grep target. Any
// identifier OR comment substring matching this regex is an
// ident-hygiene lint hit IN CODE positions; we allow it in
// package-level doc comments (the leading // banner) by stripping
// comments before scanning identifiers.
var forbiddenIdentRegex = regexp.MustCompile(`SK\.seed|SK\.prf|sk_seed|sk_prf`)
// forbiddenIdentExact is the v1.0 named-variable set the strict-atom
// invariant explicitly forbids in the assemble path's AST. Matches
// against the IDENTIFIER STRING (case-sensitive, exact).
// forbiddenIdentExact is the named-variable set the ident-hygiene lint
// flags in the assemble path's AST. Matches against the IDENTIFIER
// STRING (case-sensitive, exact). This is a naming convention, NOT a
// security property: a seed under any other name is not caught.
var forbiddenIdentExact = map[string]struct{}{
"seed": {},
"SkSeed": {},
@@ -78,18 +85,16 @@ var forbiddenIdentExact = map[string]struct{}{
// Every node in this file's AST is checked against the forbidden set.
const strictAtomPath = "thbsse_assemble.go"
// TestThbsSE_StrictAtom_NoTransientSeed is the load-bearing AST
// invariant gate for the v1.1 strict-atom Combine path. The test
// parses thbsse_assemble.go and slhdsa_internal.go, walks the AST,
// and asserts that no identifier name --- variable, field, parameter,
// function name --- matches the forbidden v1.0 named-seed patterns.
//
// The grep-equivalent check is also run as a defense-in-depth on the
// raw file bytes, with comments stripped: this catches any name the
// AST walker might miss (e.g. inside struct tags) and matches the
// shape of the audit grep specified in the v1.1 blocker
// (`grep -rE "SK\.seed|SK\.prf|sk_seed|sk_prf" thbsse_assemble.go`).
func TestThbsSE_StrictAtom_NoTransientSeed(t *testing.T) {
// TestThbsSE_AssembleIdentHygiene is an IDENTIFIER-HYGIENE LINT, not a
// security gate. The test parses thbsse_assemble.go and
// slhdsa_internal.go, walks the AST, and asserts that no identifier
// name matches the named-seed patterns. Passing this lint means the
// code does not SPELL a variable `seed`/`skSeed`/...; it does NOT mean
// the seed is absent from memory. assembleSignatureBytes reconstructs
// the FIPS 205 master into `derivedMaterial` regardless of what the
// buffer is named (ASSEMBLE-INVARIANT.md). A name lint cannot stand in
// for a no-leak proof, and this one does not claim to.
func TestThbsSE_AssembleIdentHygiene(t *testing.T) {
t.Parallel()
// Locate the source file. Go test runs in the package directory,
@@ -128,10 +133,10 @@ func TestThbsSE_StrictAtom_NoTransientSeed(t *testing.T) {
if len(violations) > 0 {
for _, v := range violations {
t.Errorf("strict-atom invariant violation: identifier %q at %s:%d (kind=%s)",
t.Errorf("assemble ident-hygiene lint: identifier %q at %s:%d (kind=%s)",
v.name, filepath.Base(v.file), v.line, v.kind)
}
t.Fatalf("%d strict-atom invariant violation(s) in %s", len(violations), strictAtomPath)
t.Fatalf("%d assemble ident-hygiene lint hit(s) in %s", len(violations), strictAtomPath)
}
// Defense in depth: scan the RAW file bytes (comments included)
@@ -145,7 +150,7 @@ func TestThbsSE_StrictAtom_NoTransientSeed(t *testing.T) {
// of the four sentinel patterns appears.
rawBytes := mustReadFile(t, path)
if matches := forbiddenIdentRegex.FindAllString(string(rawBytes), -1); len(matches) > 0 {
t.Fatalf("strict-atom grep invariant violation: %d match(es) in %s (raw bytes, comments included): %v",
t.Fatalf("assemble ident-hygiene grep lint: %d match(es) in %s (raw bytes, comments included): %v",
len(matches), strictAtomPath, matches)
}
@@ -443,15 +448,15 @@ func benchV10EquivalentSignMode(b *testing.B, mode Mode, n, t int) {
b.ResetTimer()
for i := 0; i < b.N; i++ {
r1s := make([]ThbsSeRound1Msg, 0, t)
// Only the Round-2 partial sigs are needed below; r1 is the
// commitment and is not consumed by this v1.0-equivalent path.
r2s := make([]ThbsSeRound2Msg, 0, t)
for j := 0; j < t; j++ {
guard := NewThbsSeSlotGuard()
r1, r2, err := ThbsSeRound1(params, key.Shares[j], binding, msg, guard, nil)
_, r2, err := ThbsSeRound1(params, key.Shares[j], binding, msg, guard, nil)
if err != nil {
b.Fatalf("Round1[%d]: %v", j, err)
}
r1s = append(r1s, r1)
r2s = append(r2s, r2)
}
// Drive the v1.0-equivalent emit path: Shamir-reconstruct,
ref/go/pkg/magnetar/thbsse_test.go
+34 -40
View File
@@ -21,11 +21,14 @@ import (
// cloudflare/circl/sign/slhdsa.Verify across SHAKE-192s/192f/256s.
// - TestThbsSE_RejectSeedReveal: a malicious party attempting to
// publish SK.seed as a "share" gets rejected at verify time.
// - TestThbsSE_RejectUnselectedFORS: any reveal outside the
// message-selected atom set is rejected by Combine's input
// validation (the v0.6 reveal is a single per-party masked-share
// pair; "unselected reveal" maps to "tampered partial_sig that
// does not re-derive the committed Round-1 hash").
// - TestThbsSE_RejectOversizedShareWireSize: a Round-2 partial_sig
// of the wrong wire size is rejected with a wire-size evidence.
// (THBS-SE shares the whole seed; this is a wire-size / commit
// check, NOT a FORS-leaf-selection check.)
// - TestThbsSE_RejectTamperedShareCommitMismatch: a bit-flipped
// masked share fails commit re-derivation and is dropped with a
// commit-mismatch evidence. (A commit-binding check, NOT a WOTS+
// chain-base-selection check.)
// - TestThbsSE_SlotReuseRejected: signing two distinct messages
// under the same slot is rejected with detectable evidence.
// - TestThbsSE_OverselectedCommittee_SurvivesWithholding: n=7, t=3
@@ -255,21 +258,18 @@ func TestThbsSE_RejectSeedReveal(t *testing.T) {
}
}
// TestThbsSE_RejectUnselectedFORS pins the invariant "a share is
// honored only when its commit re-derives correctly". In the v0.6
// reveal model, a Round-2 PartialSig is honored iff
// deriveThbsSeCommit(partial_sig, binding, msg, party) ==
// observed_commit. Any tampering with the partial_sig — including
// the conceptual "reveal an unselected FORS leaf" attack — is
// rejected by this check.
// TestThbsSE_RejectOversizedShareWireSize pins the invariant "a
// Round-2 PartialSig of the wrong wire size is rejected and produces a
// wire-size evidence". (THBS-SE shares the whole SLH-DSA seed; there
// are no per-FORS / per-WOTS atom reveals to "select", so this is a
// share WIRE-SIZE / commit-binding check, not a FORS-leaf-selection
// check — the earlier name was misleading.)
//
// For v0.6 the per-byte share IS the entire seed-share leaf, not a
// per-atom (FORS, WOTS) leaf — the strict per-atom share format
// lands in v0.7 (BLOCKERS.md::MAGNETAR-THBSSE-STRICT-V07). We
// therefore exercise the analogue: a Round-2 reveal whose partial_sig
// includes a forged "atom" payload (in the v0.6 wire shape, just
// extra trailing bytes) is rejected on wire-size grounds.
func TestThbsSE_RejectUnselectedFORS(t *testing.T) {
// The share is honored only when its commit re-derives correctly. Here
// a Round-2 reveal carries extra trailing bytes; it fails the
// wire-size check and the offending party is dropped with a
// ThbsSeShareWireSize evidence.
func TestThbsSE_RejectOversizedShareWireSize(t *testing.T) {
params := MustParamsFor(ModeM192s)
committee := makeThbsSeCommittee(t, 5)
key, err := NewThbsSeKey(params, 3, committee, nil)
@@ -308,28 +308,22 @@ func TestThbsSE_RejectUnselectedFORS(t *testing.T) {
}
}
// TestThbsSE_RejectUnselectedWOTS pins the invariant "a Round-2
// reveal is honored only when its commit re-derives correctly under
// the slot binding the share was originally committed to". In the
// v1.0 wire shape, the per-party PartialSig carries (mask ||
// masked_share). The conceptual "reveal an unselected WOTS+ chain
// base" attack collapses to: a Round-2 reveal whose masked-share
// portion has been flipped so that the recovered share decodes to
// the WRONG GF(257) lane --- i.e. a forged share that points to a
// different polynomial slot than the one the party committed to in
// Round 1.
// TestThbsSE_RejectTamperedShareCommitMismatch pins the invariant "a
// Round-2 reveal is honored only when its commit re-derives correctly
// under the slot binding the share was committed to". (Again: THBS-SE
// shares the whole seed; there is no WOTS+ chain base to "select", so
// this is a COMMIT-BINDING check on a tampered masked share, not a
// WOTS-selection check.)
//
// We construct the attack as a bit-flip in the masked_share portion
// of party 1's reveal. The Round-1 commit was bound to the honest
// (mask || masked_share); the tampered reveal carries
// (mask || masked_share XOR delta). The combiner's commit
// re-derivation produces a different digest, the reveal is dropped,
// and a ThbsSeShareCommitMismatch evidence is emitted for that
// party. With n=5, t=3 and only one tampered share, the remaining
// honest pair is below threshold, so Combine returns
// ErrInsufficientQuor --- the canonical "drop, slash, retry"
// signal the consensus layer expects.
func TestThbsSE_RejectUnselectedWOTS(t *testing.T) {
// We bit-flip the masked_share portion of party 1's reveal. The
// Round-1 commit was bound to the honest (mask || masked_share); the
// tampered reveal carries (mask || masked_share XOR delta). The
// combiner's commit re-derivation produces a different digest, the
// reveal is dropped, and a ThbsSeShareCommitMismatch evidence is
// emitted. With n=5, t=3 and one tampered share, the remaining honest
// pair is below threshold, so Combine returns ErrInsufficientQuor ---
// the canonical "drop, slash, retry" signal.
func TestThbsSE_RejectTamperedShareCommitMismatch(t *testing.T) {
params := MustParamsFor(ModeM192s)
committee := makeThbsSeCommittee(t, 5)
key, err := NewThbsSeKey(params, 3, committee, nil)
scripts/checks/strict-atom-ast.sh
+25 -24
View File
@@ -1,21 +1,23 @@
#!/usr/bin/env bash
# strict-atom-ast.sh --- the v1.1 AST + grep invariant gate.
# strict-atom-ast.sh --- identifier-hygiene LINT (NOT a security gate).
#
# The strict-atom Combine path (ref/go/pkg/magnetar/thbsse_assemble.go)
# is the single line of code the v1.1 audit asserts is free of any
# named transient-seed binder. This script runs the Go-side AST gate
# (TestThbsSE_StrictAtom_NoTransientSeed) which:
# This runs a NAME lint over the Combine emit path
# (ref/go/pkg/magnetar/thbsse_assemble.go): it asserts the source does
# not SPELL a variable `seed`/`skSeed`/`skPrf`/... . It does NOT show
# the FIPS 205 master is absent from memory --- assembleSignatureBytes
# reconstructs the master into `derivedMaterial` regardless of variable
# naming (see ASSEMBLE-INVARIANT.md and
# BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11). Passing this lint is a style
# check, not a no-leak proof.
#
# It runs the Go-side lint (TestThbsSE_AssembleIdentHygiene) which:
#
# 1. Parses thbsse_assemble.go as Go AST.
# 2. Walks every identifier node and asserts none matches the
# forbidden set {seed, skSeed, skPrf, SkSeed, SkPrf, PrfKey,
# prfKey, sk_seed, sk_prf}.
# 3. Defense-in-depth: scans the comment-stripped file bytes for the
# literal grep target from the v1.1 blocker
# 2. Walks every identifier node and asserts none matches the named
# set {seed, skSeed, skPrf, SkSeed, SkPrf, PrfKey, prfKey,
# sk_seed, sk_prf}.
# 3. Scans the comment-stripped file bytes for the name-pattern grep
# (`SK\.seed|SK\.prf|sk_seed|sk_prf`).
#
# The script also runs the raw audit grep against thbsse_assemble.go
# so the exit code reflects the same check the auditor runs by hand.
set -euo pipefail
@@ -24,32 +26,31 @@ cd "$REPO_ROOT"
ASSEMBLE_PATH="ref/go/pkg/magnetar/thbsse_assemble.go"
echo "==> strict-atom-ast: AST + grep invariant gate"
echo "==> strict-atom-ast: identifier-hygiene NAME lint (NOT a security gate)"
if [[ ! -f "$ASSEMBLE_PATH" ]]; then
echo " [error] $ASSEMBLE_PATH not found"
exit 2
fi
# Step 1: raw audit grep, byte-for-byte equivalent to the v1.1
# blocker's specified check.
# Step 1: raw name-pattern grep.
echo " [step 1] grep -rE \"SK\\.seed|SK\\.prf|sk_seed|sk_prf\" $ASSEMBLE_PATH"
if grep -rE "SK\.seed|SK\.prf|sk_seed|sk_prf" "$ASSEMBLE_PATH"; then
echo " [fail] strict-atom grep invariant: $ASSEMBLE_PATH contains forbidden patterns"
echo " [fail] ident-hygiene lint: $ASSEMBLE_PATH contains a flagged name pattern"
exit 2
fi
echo " [ok] no forbidden patterns in $ASSEMBLE_PATH"
echo " [ok] no flagged name patterns in $ASSEMBLE_PATH"
# Step 2: Go test that wraps both the AST walk and the comment-
# Step 2: Go lint that wraps both the AST walk and the comment-
# stripped grep.
echo " [step 2] go test -count=1 -run TestThbsSE_StrictAtom_NoTransientSeed"
echo " [step 2] go test -count=1 -run TestThbsSE_AssembleIdentHygiene"
cd ref/go
if ! go test -count=1 -run TestThbsSE_StrictAtom_NoTransientSeed ./pkg/magnetar/...; then
echo " [fail] TestThbsSE_StrictAtom_NoTransientSeed failed"
if ! go test -count=1 -run TestThbsSE_AssembleIdentHygiene ./pkg/magnetar/...; then
echo " [fail] TestThbsSE_AssembleIdentHygiene failed"
exit 2
fi
echo " [ok] TestThbsSE_StrictAtom_NoTransientSeed PASS"
echo " [ok] TestThbsSE_AssembleIdentHygiene PASS"
cd "$REPO_ROOT"
echo "==> strict-atom-ast: GATE GREEN"
echo "==> strict-atom-ast: NAME LINT GREEN (style only; not a no-leak proof)"
exit 0