From df4c537c1618b24aaec194c5fab60720bc03ad4a Mon Sep 17 00:00:00 2001 From: Antje Worring Date: Sun, 21 Jun 2026 13:06:57 -0700 Subject: [PATCH] magnetar: remove proof-by-rename + circular proofs; honest threshold status 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 `; 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. --- ASSEMBLE-INVARIANT.md | 175 ++--- AXIOM-INVENTORY.md | 113 ++-- BLOCKERS.md | 397 +++++------ CRYPTOGRAPHER-SIGN-OFF.md | 165 ++--- DEPLOYMENT-RUNBOOK.md | 7 +- DESIGN.md | 202 +++--- PROOF-CLAIMS.md | 383 +++-------- README.md | 160 +++-- SPEC.md | 37 +- SUBMISSION-STATUS.md | 38 +- TRUSTED-COMPUTING-BASE.md | 15 +- ct/dudect/strict_atom_combine_ct_test.go | 65 +- proofs/README.md | 108 +-- .../easycrypt/Magnetar_N1_Atom_Refinement.ec | 77 --- proofs/easycrypt/Magnetar_N1_SHAKE_Expand.ec | 91 --- proofs/easycrypt/Magnetar_N1_StrictAtom.ec | 261 ++------ .../easycrypt/Magnetar_N4_KeyDeriveStable.ec | 51 -- proofs/easycrypt/Magnetar_N5_PVSS_DKG.ec | 321 ++------- proofs/easycrypt/README.md | 103 +-- proofs/easycrypt/lemmas/Magnetar_CT.ec | 74 -- proofs/easycrypt/lemmas/SLHDSA_Functional.ec | 74 -- proofs/lean-easycrypt-bridge.md | 77 +-- proofs/lean/Crypto/Magnetar/StrictAtom.lean | 140 +--- proofs/lean/README.md | 46 +- ref/go/cmd/genkat/main.go | 4 +- ref/go/pkg/magnetar/pvss_dkg.go | 632 ++++++++++++------ ref/go/pkg/magnetar/pvss_dkg_test.go | 166 ++++- ref/go/pkg/magnetar/slhdsa_internal.go | 16 - ref/go/pkg/magnetar/thbsse.go | 15 +- ref/go/pkg/magnetar/thbsse_assemble.go | 84 ++- ref/go/pkg/magnetar/thbsse_assemble_test.go | 73 +- ref/go/pkg/magnetar/thbsse_test.go | 74 +- scripts/checks/strict-atom-ast.sh | 49 +- 33 files changed, 1685 insertions(+), 2608 deletions(-) delete mode 100644 proofs/easycrypt/Magnetar_N1_Atom_Refinement.ec delete mode 100644 proofs/easycrypt/Magnetar_N1_SHAKE_Expand.ec delete mode 100644 proofs/easycrypt/Magnetar_N4_KeyDeriveStable.ec delete mode 100644 proofs/easycrypt/lemmas/Magnetar_CT.ec delete mode 100644 proofs/easycrypt/lemmas/SLHDSA_Functional.ec diff --git a/ASSEMBLE-INVARIANT.md b/ASSEMBLE-INVARIANT.md index 31ac81c..095d3e3 100644 --- a/ASSEMBLE-INVARIANT.md +++ b/ASSEMBLE-INVARIANT.md @@ -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. diff --git a/AXIOM-INVENTORY.md b/AXIOM-INVENTORY.md index 75e0149..77591cb 100644 --- a/AXIOM-INVENTORY.md +++ b/AXIOM-INVENTORY.md @@ -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) --- diff --git a/BLOCKERS.md b/BLOCKERS.md index 7113470..f28fe8f 100644 --- a/BLOCKERS.md +++ b/BLOCKERS.md @@ -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. diff --git a/CRYPTOGRAPHER-SIGN-OFF.md b/CRYPTOGRAPHER-SIGN-OFF.md index d360ec6..d14a8ae 100644 --- a/CRYPTOGRAPHER-SIGN-OFF.md +++ b/CRYPTOGRAPHER-SIGN-OFF.md @@ -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`. diff --git a/DEPLOYMENT-RUNBOOK.md b/DEPLOYMENT-RUNBOOK.md index 7aa71a0..d3fd82c 100644 --- a/DEPLOYMENT-RUNBOOK.md +++ b/DEPLOYMENT-RUNBOOK.md @@ -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 diff --git a/DESIGN.md b/DESIGN.md index b5ff8f9..12c7866 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -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: - (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. diff --git a/PROOF-CLAIMS.md b/PROOF-CLAIMS.md index 51c93f8..0a49766 100644 --- a/PROOF-CLAIMS.md +++ b/PROOF-CLAIMS.md @@ -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 | diff --git a/README.md b/README.md index 1335e69..3742948 100644 --- a/README.md +++ b/README.md @@ -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 diff --git a/SPEC.md b/SPEC.md index b092be7..fac7690 100644 --- a/SPEC.md +++ b/SPEC.md @@ -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) diff --git a/SUBMISSION-STATUS.md b/SUBMISSION-STATUS.md index 86261c9..b0a6168 100644 --- a/SUBMISSION-STATUS.md +++ b/SUBMISSION-STATUS.md @@ -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) diff --git a/TRUSTED-COMPUTING-BASE.md b/TRUSTED-COMPUTING-BASE.md index 1ba2a65..ac68e29 100644 --- a/TRUSTED-COMPUTING-BASE.md +++ b/TRUSTED-COMPUTING-BASE.md @@ -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), diff --git a/ct/dudect/strict_atom_combine_ct_test.go b/ct/dudect/strict_atom_combine_ct_test.go index 03cc640..787c096 100644 --- a/ct/dudect/strict_atom_combine_ct_test.go +++ b/ct/dudect/strict_atom_combine_ct_test.go @@ -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) } }) diff --git a/proofs/README.md b/proofs/README.md index 1983f89..d3369ec 100644 --- a/proofs/README.md +++ b/proofs/README.md @@ -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`). diff --git a/proofs/easycrypt/Magnetar_N1_Atom_Refinement.ec b/proofs/easycrypt/Magnetar_N1_Atom_Refinement.ec deleted file mode 100644 index 14c18ce..0000000 --- a/proofs/easycrypt/Magnetar_N1_Atom_Refinement.ec +++ /dev/null @@ -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. diff --git a/proofs/easycrypt/Magnetar_N1_SHAKE_Expand.ec b/proofs/easycrypt/Magnetar_N1_SHAKE_Expand.ec deleted file mode 100644 index 8b3a754..0000000 --- a/proofs/easycrypt/Magnetar_N1_SHAKE_Expand.ec +++ /dev/null @@ -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. diff --git a/proofs/easycrypt/Magnetar_N1_StrictAtom.ec b/proofs/easycrypt/Magnetar_N1_StrictAtom.ec index 86f292d..7bdf717 100644 --- a/proofs/easycrypt/Magnetar_N1_StrictAtom.ec +++ b/proofs/easycrypt/Magnetar_N1_StrictAtom.ec @@ -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. diff --git a/proofs/easycrypt/Magnetar_N4_KeyDeriveStable.ec b/proofs/easycrypt/Magnetar_N4_KeyDeriveStable.ec deleted file mode 100644 index 59b9c89..0000000 --- a/proofs/easycrypt/Magnetar_N4_KeyDeriveStable.ec +++ /dev/null @@ -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. diff --git a/proofs/easycrypt/Magnetar_N5_PVSS_DKG.ec b/proofs/easycrypt/Magnetar_N5_PVSS_DKG.ec index e8d2432..4a3b6cf 100644 --- a/proofs/easycrypt/Magnetar_N5_PVSS_DKG.ec +++ b/proofs/easycrypt/Magnetar_N5_PVSS_DKG.ec @@ -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. diff --git a/proofs/easycrypt/README.md b/proofs/easycrypt/README.md index f653830..48ca5cf 100644 --- a/proofs/easycrypt/README.md +++ b/proofs/easycrypt/README.md @@ -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). diff --git a/proofs/easycrypt/lemmas/Magnetar_CT.ec b/proofs/easycrypt/lemmas/Magnetar_CT.ec deleted file mode 100644 index d7751ce..0000000 --- a/proofs/easycrypt/lemmas/Magnetar_CT.ec +++ /dev/null @@ -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. diff --git a/proofs/easycrypt/lemmas/SLHDSA_Functional.ec b/proofs/easycrypt/lemmas/SLHDSA_Functional.ec deleted file mode 100644 index d774ba0..0000000 --- a/proofs/easycrypt/lemmas/SLHDSA_Functional.ec +++ /dev/null @@ -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. diff --git a/proofs/lean-easycrypt-bridge.md b/proofs/lean-easycrypt-bridge.md index e7ea927..9649a6f 100644 --- a/proofs/lean-easycrypt-bridge.md +++ b/proofs/lean-easycrypt-bridge.md @@ -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. diff --git a/proofs/lean/Crypto/Magnetar/StrictAtom.lean b/proofs/lean/Crypto/Magnetar/StrictAtom.lean index 73c4e35..1372e30 100644 --- a/proofs/lean/Crypto/Magnetar/StrictAtom.lean +++ b/proofs/lean/Crypto/Magnetar/StrictAtom.lean @@ -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 diff --git a/proofs/lean/README.md b/proofs/lean/README.md index 807469b..dfe5ce1 100644 --- a/proofs/lean/README.md +++ b/proofs/lean/README.md @@ -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. diff --git a/ref/go/cmd/genkat/main.go b/ref/go/cmd/genkat/main.go index c349cd4..dd79653 100644 --- a/ref/go/cmd/genkat/main.go +++ b/ref/go/cmd/genkat/main.go @@ -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)) } diff --git a/ref/go/pkg/magnetar/pvss_dkg.go b/ref/go/pkg/magnetar/pvss_dkg.go index a16891c..9a53d37 100644 --- a/ref/go/pkg/magnetar/pvss_dkg.go +++ b/ref/go/pkg/magnetar/pvss_dkg.go @@ -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) diff --git a/ref/go/pkg/magnetar/pvss_dkg_test.go b/ref/go/pkg/magnetar/pvss_dkg_test.go index 2247880..6daf3ef 100644 --- a/ref/go/pkg/magnetar/pvss_dkg_test.go +++ b/ref/go/pkg/magnetar/pvss_dkg_test.go @@ -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 diff --git a/ref/go/pkg/magnetar/slhdsa_internal.go b/ref/go/pkg/magnetar/slhdsa_internal.go index f859203..57cb7d5 100644 --- a/ref/go/pkg/magnetar/slhdsa_internal.go +++ b/ref/go/pkg/magnetar/slhdsa_internal.go @@ -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 // ===================================================================== diff --git a/ref/go/pkg/magnetar/thbsse.go b/ref/go/pkg/magnetar/thbsse.go index 42c3718..111c53a 100644 --- a/ref/go/pkg/magnetar/thbsse.go +++ b/ref/go/pkg/magnetar/thbsse.go @@ -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 diff --git a/ref/go/pkg/magnetar/thbsse_assemble.go b/ref/go/pkg/magnetar/thbsse_assemble.go index 3e22713..6221122 100644 --- a/ref/go/pkg/magnetar/thbsse_assemble.go +++ b/ref/go/pkg/magnetar/thbsse_assemble.go @@ -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 diff --git a/ref/go/pkg/magnetar/thbsse_assemble_test.go b/ref/go/pkg/magnetar/thbsse_assemble_test.go index 49bcca9..5fcbb91 100644 --- a/ref/go/pkg/magnetar/thbsse_assemble_test.go +++ b/ref/go/pkg/magnetar/thbsse_assemble_test.go @@ -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, diff --git a/ref/go/pkg/magnetar/thbsse_test.go b/ref/go/pkg/magnetar/thbsse_test.go index e0848f1..29d780e 100644 --- a/ref/go/pkg/magnetar/thbsse_test.go +++ b/ref/go/pkg/magnetar/thbsse_test.go @@ -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) diff --git a/scripts/checks/strict-atom-ast.sh b/scripts/checks/strict-atom-ast.sh index 5b63708..fe319e0 100755 --- a/scripts/checks/strict-atom-ast.sh +++ b/scripts/checks/strict-atom-ast.sh @@ -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