mirror of
https://github.com/luxfi/pulsar.git
synced 2026-09-24 00:25:52 +00:00
docs(pulsar): bring PULSAR.md + DKG-PROOF-BOUNDARY.md current to v0.6.3
Updates the certificate-layer spec and the DKG proof-boundary spec/vectors from their v0.5.0 grounding (docs/pulsar-final, 24 commits behind) to the real v0.6.3 tree (885f691). DOCS ONLY — no code touched. Every implementation claim re-grounded file:line in ref/go/pkg/pulsar/ at v0.6.3. The load-bearing change: the keygen residual is CLOSED for Claim (A). v0.6.0+ ships DEALERLESS RSS keygen (mithril_rss.go MithrilRSSKeygen — Mithril short Replicated Secret Sharing, ia.cr/2026/013; the dealer is dead at keygen too), whose threshold signatures verify byte-for-byte under stock circl mldsa65.Verify (mithril_rss_test.go:38 all 15 committees N<=6; mithril_rss_n8_test.go:16 T==N at n=8,n=16). The v0.6.3 accumulateSubset per-subset mod-q reduction (mithril_rss.go :122) fixes a uint32 overflow that wrapped the key once C(N,N-T+1)>=512, unblocking large committees (n=16,t=14, C(16,3)=560; reconstructed ||s2||inf~205 << gamma2). The Mithril 3-round HYPERBALL no-reconstruct signer (mithril_rss_hyperball.go SignHyperball, gates 5/6) signs the RSS key with NO party/coordinator ever forming the full s1/s2/y/w0/sk: each party emits only z_j = y_j + c*s1_(j); the summed z is a standard FIPS-204 response; the secret mask y is never serialised (commit 6a17e74). Verifies under stock circl (mithril_rss_hyperball_test.go:41). PULSAR.md: full v0.6.3 architecture (dealerless RSS keygen, hyperball no-reconstruct signer, BCC/CSCP v0.4, malicious hardening v0.5, mlwe de-dup v0.6.1/.2, overflow fix v0.6.3); the version lineage (v0.3 algebraic-broadcast REMOVED -> ... -> v0.6.3 + hyperball); and the Avalanche-native sampled-cert committee math — sample MANY small dealerless RSS committees, r-of-m binomial tail, default Pulsar-HYBRID-PQ-v1 n=8,t=7,m=12,r=8 (one-committee p~2^-8.6, P_fail~2^-59.8; NOT n=64/t=5), unbiasable stake-weighted VRF sortition seeded by the prev finalized block, committeePlanHash bound into the Quasar subject, three tiers FAST/HYBRID_PQ/PQ_ROOT. DKG-PROOF-BOUNDARY.md + vectors: keygen residual restated (CLOSED via dealerless RSS for Claim A; full FIPS-204 KeyGen-distribution-equivalence is the labelled open-research residual). Keeps the 7 deliverables; adds RSS keygen + hyperball to the transcript spec, DST table, share-commitment format, vectors (3 new positive, 5 new negative), and the proof checklist (18 rows). Line numbers refreshed v0.5.0 -> v0.6.3 throughout. Claim discipline held: (A) standard-verifier-compatible is PROVEN (circl accepts; tests cited); (B) full FIPS-204 KeyGen-distribution-equivalence + malicious-secure CSCP/identifiable-abort are labelled residuals. Never claims FIPS/NIST-certified threshold ML-DSA, fully-malicious-secure-proven, or global-1000-validator DKG.
This commit is contained in:
@@ -0,0 +1,479 @@
|
||||
# Pulsar — DKG Proof-Boundary Specification
|
||||
|
||||
> **Purpose.** This document fixes the *proof boundary* of the Pulsar DKG and
|
||||
> threshold-signing protocols: the exact bytes, domain separators, binding rules,
|
||||
> commitment formats, test vectors, cross-version KATs, and the test→property
|
||||
> map. It is the auditable contract between "what the protocol hashes/signs" and
|
||||
> "what a security claim is allowed to say."
|
||||
>
|
||||
> **Grounded in v0.6.3** (`git log` → commit `0650729`, `origin/main`). Every
|
||||
> implementation claim cites `ref/go/pkg/pulsar/<file>:<line>`. Companion
|
||||
> documents: `PROOF-CLAIMS.md` (assurance vocabulary — the gate-read file),
|
||||
> `ref/go/pkg/pulsar/VERSIONS.md` (version/track ledger), `BLOCKERS.md` (open
|
||||
> residuals), `PULSAR.md` (the certificate-layer architecture this kernel sits
|
||||
> under).
|
||||
|
||||
---
|
||||
|
||||
## §0. Claim discipline (read first — this is the whole point)
|
||||
|
||||
Two claims are made, and they are **never** conflated:
|
||||
|
||||
- **Claim (A) — standard-verifier compatibility (PROVEN).** A Pulsar threshold
|
||||
signature `(c̃, z, h)` is byte-for-byte a FIPS-204 ML-DSA signature: the
|
||||
*unmodified* `cloudflare/circl` `mldsa65.Verify` / `mldsa87.Verify` accepts it
|
||||
with **no Pulsar code in the verify path**. This is proven, today, in **three**
|
||||
independent settings:
|
||||
|
||||
| Setting | Test | Site |
|
||||
|---|---|---|
|
||||
| No-reconstruct BCC/CEF over a single group key | `TestBCCSignRoundTripVerifiesCIRCL` | `bcc_sign_test.go:86` |
|
||||
| **Dealerless RSS** key (all 15 committees N ≤ 6) | `TestMithrilRSSStockCirclVerify` | `mithril_rss_test.go:38` |
|
||||
| **Dealerless RSS** key (T = N at N > 6: n=8,t=8; n=16,t=16) | `TestMithrilRSS_LargeN_StockCircl` | `mithril_rss_n8_test.go:16` |
|
||||
| **No-reconstruct hyperball** over the RSS key | `TestHyperballStockCirclVerify` | `mithril_rss_hyperball_test.go:41` |
|
||||
|
||||
All carry tamper / wrong-message / wrong-context **negatives** (verifier
|
||||
non-vacuous). Assurance tag: **interop-tested**.
|
||||
|
||||
- **Claim (B) — DKG / threshold-protocol construction soundness (Lux-authored,
|
||||
SCOPED).** The dealerless key generation (RSS / Mithril) and the threshold
|
||||
signing protocols (BCC/CEF/CSCP + hyperball) are a Lux construction. Their
|
||||
security is the **scoped claim** in `PROOF-CLAIMS.md §0` and `PULSAR.md §0`:
|
||||
|
||||
> *Dealerless committee key generation (RSS / Mithril) + no-reconstruct signing
|
||||
> (BCC/CSCP + Mithril hyperball) + standard-ML-DSA-verifier output,
|
||||
> malicious-hardened; the full FIPS-204 KeyGen-distribution-equivalence proof
|
||||
> and the malicious-secure CSCP/identifiable-abort layer are labelled
|
||||
> residuals.*
|
||||
|
||||
**Never claimed** (`PROOF-CLAIMS.md §0`): FIPS/NIST-certified threshold ML-DSA ·
|
||||
fully-malicious-secure-*proven* (mechanized) · global-1000-validator DKG. NIST
|
||||
FIPS-204 standardises *single-party* ML-DSA only; Claim (A) is about the *output
|
||||
bytes*, Claim (B) is *our* theorem.
|
||||
|
||||
### §0.1 The keygen residual — restated for v0.6.3 (the dealer is dead at keygen)
|
||||
|
||||
Pre-v0.6, keygen was the open half: signing was no-reconstruct, but the key was
|
||||
either trusted-dealer (`DealAlgShares`) or dealerless-but-seed-reconstruct
|
||||
(`dkg.go`). **v0.6.0+ closes the dealerless-keygen gap for Claim (A)** with
|
||||
Mithril short Replicated Secret Sharing (RSS):
|
||||
|
||||
- **`MithrilRSSKeygen`** (`mithril_rss.go:133`) generates the FIPS-204 group key
|
||||
with **no trusted dealer**: each `M`-subset's short secret `(s1^(S), s2^(S)) ∈ S_η`
|
||||
is sampled by that subset's *leader* from the leader's contributed entropy
|
||||
(`mithrilSubsetSeed`, `:84`) and replicated to the subset's members; the key is
|
||||
`s1 = Σ_S s1^(S)`, `s2 = Σ_S s2^(S)`, with `‖s2‖∞ ≤ C(N,N−T+1)·η` **genuinely
|
||||
small** (it sidesteps the naive-additive `N·η` blow-up of §1.4). No party holds
|
||||
all subsets (`TestMithrilRSSDealerless`, `mithril_rss_test.go:91`); any T
|
||||
parties reconstruct via the balanced partition, fewer than T cannot.
|
||||
- **The signature verifies under stock circl** for every viable committee N ≤ 6
|
||||
(`mithril_rss_test.go:70`) and T = N at n=8 / n=16 (`mithril_rss_n8_test.go:40`)
|
||||
— the **gold proof** of dealerless stock-FIPS-204 signability.
|
||||
|
||||
So the lineage table is now:
|
||||
|
||||
| Lineage | Keygen | Sign | Status |
|
||||
|---|---|---|---|
|
||||
| **RSS short-replicated** (`mithril_rss.go`) | **DEALERLESS** — no dealer, no party holds the whole `(s1,s2)`, `‖s2‖∞ ≤ C·η` small | quorum-reconstruct (`MithrilKey.Sign`, `:266`) **OR no-reconstruct** (`SignHyperball`, `mithril_rss_hyperball.go:780`) | **the v0.6 dealerless path; stock-circl-verifiable** |
|
||||
| `s1` poly-share (`DealAlgShares`) | trusted dealer (bootstrap) | no-reconstruct (`AggregateBCCWithBlame`) | keygen **quarantined to `bootstrap_dealer_test.go`** — test/bootstrap only |
|
||||
| Seed-share (`dkg.go` GF(257); `large_dkg.go` GF(q)) | dealerless ceremony, but **forms `sk` at keygen** | reconstruct-at-sign | `large_dkg.go` **quarantined** behind `//go:build legacy_trusted_dealer` |
|
||||
|
||||
**What is STILL a residual (the precise statement — do not round this off).** RSS
|
||||
gives Claim (A): the dealerless `GroupPK` is a real FIPS-204 key whose threshold
|
||||
signatures the stock verifier accepts. It does **not** by itself give Claim (B)'s
|
||||
*distributional* statement: **full FIPS-204 KeyGen-distribution-equivalence** —
|
||||
that the dealerless composite `GroupPK` is distributed identically to a single
|
||||
honest `KeyGen`, with (i) an unbiased composite secret, (ii) hiding against `< t`
|
||||
corruptions, and (iii) abort-bias resistance — needs a separate
|
||||
simulation/hiding/abort-bias proof. The structural facts (no party holds the key;
|
||||
`‖s2‖∞ ≤ C·η`; stock-circl-verifiable) are proven; the distributional equivalence
|
||||
is **open-research** (§7 row 15). The *naive-additive byte-FIPS DKG* remains
|
||||
correctly **fail-closed** (`ErrDealerlessByteFIPSUnreachable`, §1.4, §7 row 14) —
|
||||
RSS is the named escape it always pointed to, not a weakening of it.
|
||||
|
||||
**Therefore:** SIGNING = no-reconstruct (BCC/CSCP and hyperball) +
|
||||
malicious-hardened (v0.5); KEYGEN = **dealerless RSS** (no dealer, no party holds
|
||||
the key), stock-FIPS-204-verifiable. The remaining (B) gap is the *distributional
|
||||
equivalence proof*, not the existence of a dealerless committee key. Permissionless
|
||||
dealerless *safety* is additionally carried by the **Corona** leg of the Quasar
|
||||
AND-mode dual-PQ cert (`naive_additive_seta_obstruction.go:107`).
|
||||
|
||||
### §0.2 Consensus-native framing
|
||||
|
||||
Pulsar is **not** an all-`N`-sign protocol. Lux Avalanche-family subsampling
|
||||
carries chain *safety*; Pulsar produces **compact post-quantum certificates over
|
||||
consensus-finalised digests** — and it scales by **sampling many small dealerless
|
||||
committees and accumulating confidence by repetition** (`PULSAR.md §7`), not by
|
||||
one large committee. The default profile `Pulsar-HYBRID-PQ-v1` samples `m = 12`
|
||||
committees of `n = 8` (`t = 7`), requiring `r = 8` legs: one-committee capture
|
||||
`p = Pr[X ≥ 7], X ~ Binom(8, ⅓) ≈ 2⁻⁸·⁶`, certificate `P_fail ≈ 2⁻⁵⁹·⁸`. The DKG
|
||||
below is therefore a **per-committee, per-epoch** ceremony, and the binding rules
|
||||
(§3) pin each share/cert to its committee, epoch, and key.
|
||||
|
||||
---
|
||||
|
||||
## §1. Deliverable 1 — Protocol transcript spec (byte layout & ordering)
|
||||
|
||||
All Pulsar hashing routes through `transcript.go` (FIPS-202 / SP 800-185), now
|
||||
backed by `github.com/luxfi/mlwe/transcript` (v0.6.1, byte-preserving). The two
|
||||
framing primitives:
|
||||
|
||||
- **`cshake256(input, outLen, S)`** = cSHAKE256 with function-name `N = "Pulsar"`
|
||||
(`transcript.go:73`, `:79`). Pinning `N="Pulsar"` makes a cross-suite mix-up a
|
||||
deterministic mismatch.
|
||||
- **`transcriptHash(S, parts…)`** → 48-byte digest, SP 800-185 TupleHash256-style;
|
||||
**`transcriptHash32`** is the 32-byte counterpart (`transcript.go:103`, `:116`).
|
||||
Length-prefixed parts ⇒ unambiguous boundaries.
|
||||
|
||||
### §1.1 Dealerless RSS keygen (`mithril_rss.go`)
|
||||
|
||||
Driven by one contributed 32-byte seed per party; deterministic in
|
||||
`(mode, t, n, partySeeds)`. Fail-closed outside the Mithril viability bound
|
||||
`2 ≤ T ≤ N ≤ 63` ∧ `τ·C(N,N−T+1)·η < γ2` (`rss.ValidateCommittee`).
|
||||
|
||||
```
|
||||
rho = SHAKE256( "pulsar.mithril.rss.rho.v1" ‖ partySeed_0 ‖ … ) # mithril_rss.go:99
|
||||
A = ExpandA(rho) # mithril_rss.go:163
|
||||
for each M-subset S (M = N−T+1): # mithril_rss.go:169
|
||||
leaderSeed = partySeeds[ leader(S) ]
|
||||
subSeed = SHAKE256( "pulsar.mithril.rss.subset.v1" ‖ leaderSeed ‖ le64(maskS), 64 ) # :84
|
||||
(s1^(S), s2^(S)) = expandS(subSeed) ∈ S_η # :173
|
||||
replicate (s1^(S), s2^(S)) to every member of S # :175
|
||||
s1 += s1^(S); s2 += s2^(S) (REDUCE mod q PER SUBSET — accumulateSubset) # :180, :122
|
||||
t = A·s1 + s2; (t0, t1) = Power2Round(t) # computePublicKey :192
|
||||
pub = rho ‖ PackT1(t1); tr = SHAKE256(pub) # :208–:215
|
||||
```
|
||||
|
||||
**The v0.6.3 per-subset reduction (`accumulateSubset`, `:122`).** Every `χ_η`
|
||||
coefficient is stored ≈ q ≈ 2²³ and `poly.add` is a raw uint32 add; reducing mod q
|
||||
*per subset* keeps every accumulator < 2q ≪ 2³², so summing all `C(N,M)` subsets
|
||||
never overflows (the wall at `C ≥ ⌊2³²/q⌋ = 512`, e.g. n=16,t=14 with
|
||||
`C(16,3)=560`). Mod-q is additively homomorphic ⇒ small committees (n ≤ 8) are
|
||||
byte-unchanged.
|
||||
|
||||
**Reconstruction** (`ReconstructKeyMaterial`, `:223`) sums each subset secret
|
||||
exactly once via the balanced partition `rss.RSSRecover` — the threshold-gated act
|
||||
a T-quorum performs to sign; the dealerless keygen never performs it.
|
||||
|
||||
### §1.2 No-reconstruct hyperball signing (`mithril_rss_hyperball.go`)
|
||||
|
||||
`SignHyperball(active, msg, ctx, rng, maxRounds)` (`:780`). Each active party holds
|
||||
only its balanced-partition share `s1_(j)` (`partyShareS1`, `:870` — never summed
|
||||
across parties); the party object is constructed from `mk.holdings[id]` alone
|
||||
(`newHyperballParty`, `:261`, the structural no-reconstruct boundary). **μ** is the
|
||||
FIPS-204 message representative `deriveMuCtx(tr, ctx, msg)`. Three rounds:
|
||||
|
||||
```
|
||||
Round 1 (round1, :294): for K=kReps slots, y_{j,k} ← uniform B(0,r1); # sampleHyperballInBall :895
|
||||
w_{j,k} = A·y_{j,k}; broadcast CommitW (hash) + CommitT(T_j)
|
||||
Round 2 (round2 :321 / aggregateCommitments :430):
|
||||
reveal w_{j,k}; verify vs CommitW (equivocation gate :466);
|
||||
w_k = Σ_j w_{j,k}; c_k = H(μ ‖ packW1(HighBits(w_k))) # boundary-clear slots only
|
||||
Round 3 (round3 :333): z_{j,k} = y_{j,k} + c_k·s1_(j); Excess gate (hyperballExcess :966)
|
||||
REJECTS (never reveals) if z leaves B(0,r)
|
||||
Finalize (finalize :518): require all-accepted slot; z_k = Σ_j z_{j,k};
|
||||
‖z‖∞ < γ1−β; w' = A·z − c·t1·2^d (PUBLIC); h = FindHint(w', w1)
|
||||
sigEncode(c̃, z, h); FAIL-CLOSED VerifyCtx before emit (:613)
|
||||
```
|
||||
|
||||
The **only** data crossing the wire (`HyperballRound{1,2,3}`, `:206`–`:226`) is
|
||||
commitment hashes, the public `w_{j,k}` (recovering `y` is Module-SIS), and the
|
||||
public `z_{j,k}`. No share `s1_(j)`, no mask `y`, no low-bits quantity is ever
|
||||
serialised — asserted by `publicBytes()` (`:732`) and the no-leak oracle
|
||||
(`TestHyperballNoReconstructStructural` `:100`, `TestHyperballMaskNeverOnWire`
|
||||
`:529`).
|
||||
|
||||
### §1.3 No-reconstruct BCC/CEF signing (single group key, `distributed_bcc.go`)
|
||||
|
||||
Per-party key custody is **one** `AlgShare` — a poly-vector Shamir share of the
|
||||
*expanded* `s1` (length `L`) over GF(q), `s1` only, never `s2`/`t0`/seed. One
|
||||
online round over an offline nonce:
|
||||
|
||||
```
|
||||
μ = SHAKE256( tr ‖ 0x00 ‖ |ctx| ‖ ctx ‖ msg ) # FIPS-204 §5.4 (deriveMuCtx)
|
||||
c̃ = SHAKE256( μ ‖ packW1(w1) ) # deriveCTilde, distributed_bcc.go:586
|
||||
c = SampleInBall(c̃)
|
||||
Round1 (:560): bind NonceCert; reserve single-use material keyed on w1
|
||||
Round2 (:603): reserve nonce BEFORE the secret is touched, then
|
||||
z_i = partialLinearMap(λ_i, ĉ, y_i, s1_i) (:645) = λ_i·y_i + c·λ_i·s1_i
|
||||
Finalize (AggregateBCCWithBlame, :875), fail-closed in order:
|
||||
1. authenticate origin (drop forged/unsigned partials, no blame against owner) :883
|
||||
2. verify+attribute each sigma proof bound to (λ_p,c,z_p,session,nonce,party)
|
||||
3. canonical signer subset of exactly `threshold` distinct signers (CanonicalSignerSet)
|
||||
4. z = Σ z_p (Lagrange-linear → ȳ + c·s1; s1 NEVER formed)
|
||||
5. ‖z‖∞ < γ1−β
|
||||
6. w' = A·z − c·t1·2^d (PUBLIC); h = FindHint(w', w1)
|
||||
7. sigEncode(c̃, z, h)
|
||||
```
|
||||
|
||||
`auth == nil` is **refused fail-closed** (`ErrOriginAuthRequired`,
|
||||
`distributed_bcc.go:813`); the unauthenticated path is reachable only via the
|
||||
explicit `UnauthenticatedAggregation` opt-out (`:836`). No share, sk, or seed
|
||||
enters `AggregateBCC`'s parameter list — the load-bearing no-reconstruct boundary.
|
||||
|
||||
---
|
||||
|
||||
## §2. Deliverable 2 — Domain separators (every DST, from code)
|
||||
|
||||
All tags are version-pinned; rotating one invalidates every vector pinned at it.
|
||||
Three encodings coexist, all the *implemented reality*:
|
||||
**`PULSAR-…-V1`** (cSHAKE customisation strings, `transcript.go`),
|
||||
**`PULSAR/…/v1`** (literal prefixes, ledger/auth), and
|
||||
**`pulsar.mithril.*.v1`** (the RSS/hyperball SHAKE-prefix tags). The
|
||||
certificate-layer `pulsar:v1:*` namespace (`PULSAR.md §14`) is the *proposed*
|
||||
consensus binding, kept distinct on purpose.
|
||||
|
||||
### §2.1 cSHAKE256 customisation tags (`transcript.go:40`–`:66`)
|
||||
|
||||
| Constant | Value | Purpose | Site |
|
||||
|---|---|---|---|
|
||||
| `functionName` | `Pulsar` | cSHAKE `N` param (all calls) | `transcript.go:73` |
|
||||
| `tagDKGCommit` | `PULSAR-DKG-COMMIT-V1` | DKG Round-2 digest + committeeRoot | `transcript.go:40` |
|
||||
| `tagDKGTranscript` | `PULSAR-DKG-TRANSCRIPT-V1` | DKG transcript / finalization hash | `transcript.go:41` |
|
||||
| `tagSignR1` | `PULSAR-SIGN-R1-V1` | Round-1 binding | `transcript.go:42` |
|
||||
| `tagSignR2` | *(reserved, undefined)* | Round-2 MAC (intentionally undefined so a stale rebase fails to compile) | `transcript.go:44` |
|
||||
| `tagReshareCommit` | `PULSAR-RESHARE-COMMIT-V1` | reshare commit | `transcript.go:61` |
|
||||
| `tagExpandB` | `PULSAR-EXPANDB-V1` | matrix `B` expansion | `transcript.go:64` |
|
||||
| `tagComplaint` | `PULSAR-COMPLAINT-V1` | complaint hashing | `transcript.go:65` |
|
||||
| `tagSeedShare` | `PULSAR-SEED-SHARE-V1` | Shamir coeff stream + master-seed mix | `transcript.go:66` |
|
||||
|
||||
### §2.2 RSS / hyperball SHAKE-prefix DSTs
|
||||
|
||||
| String | Purpose | Site |
|
||||
|---|---|---|
|
||||
| `pulsar.mithril.rss.rho.v1` | RSS joint public seed `rho` | `mithril_rss.go:101` |
|
||||
| `pulsar.mithril.rss.subset.v1` | RSS per-subset sampling seed (leader entropy ‖ mask) | `mithril_rss.go:86` |
|
||||
| `pulsar.mithril.hyperball.nonce.v1` | hyperball per-round, per-slot nonce seed | `mithril_rss_hyperball.go:993` |
|
||||
| `pulsar.mithril.hyperball.commitW.v1` | hyperball `w`-commitment binding (anti-equivocation) | `mithril_rss_hyperball.go:1006` |
|
||||
| `pulsar.mithril.hyperball.commitT.v1` | hyperball `T_j = A·s1_(j)` commitment (blame-only) | `mithril_rss_hyperball.go:1021` |
|
||||
| `pulsar.mithril.hyperball.sid.v1` | hyperball session id = H(pub ‖ active ‖ μ) | `mithril_rss_hyperball.go:1032` |
|
||||
|
||||
### §2.3 Literal-prefix DSTs (`PULSAR/…/v1` and friends)
|
||||
|
||||
| String | Purpose | Site |
|
||||
|---|---|---|
|
||||
| `PULSAR-DKG-DEALER-V1` | seed-share DKG Shamir coeff-stream key material | `dkg.go:225` |
|
||||
| `PULSAR-DKG-ENCAPSEED-V1` | per-recipient ML-KEM-768 encap seed | `dkg.go:268` |
|
||||
| `PULSAR-COMMITTEE-V1` | committee-root prefix | `dkg.go:516` |
|
||||
| `PULSAR/nonce-single-use/v1` | nonce dedup key (`w1` alone) | `nonce_ledger.go:395` |
|
||||
| `PULSAR/share-ledger-identity/v1` | committee-independent share identity | `nonce_ledger.go:303` |
|
||||
| `PULSAR/committee-id/v1` | committee id = H(jointPKID ‖ quorum) | `nonce_ledger.go:407` |
|
||||
| `PULSAR/nonce-binding-digest/v1` | `(ctx,msg)` digest in a reservation | `nonce_ledger.go:423` |
|
||||
| `PULSAR-BCC-CEF/joint-pk-id/v1` | stable group-PK id (`JointPKID`) | `distributed_bcc.go:1096` |
|
||||
| `PULSAR/protocol-msg/v1` | authenticated-protocol-message TBS | `protocol_auth.go:61` |
|
||||
| `PULSAR-TESTRAND-V1` | deterministic test RNG (tests only) | `dkg_test.go` |
|
||||
|
||||
---
|
||||
|
||||
## §3. Deliverable 3 — Participant / key-epoch binding rules
|
||||
|
||||
A share or certificate is bound to its context by the following identities. Each
|
||||
row states **what is hashed**, the **site**, and — honestly — **where binding is
|
||||
NOT yet at the kernel** (cert-layer or implicit).
|
||||
|
||||
| Bound to | Mechanism (what is hashed) | Site | Honest note |
|
||||
|---|---|---|---|
|
||||
| **group / key (RSS)** | `rho = SHAKE256("pulsar.mithril.rss.rho.v1" ‖ Σ partySeeds)`; `pub = rho ‖ PackT1(t1)`; `tr = SHAKE256(pub)` | `mithril_rss.go:99`, `:208`–`:215` | the dealerless key-identity root |
|
||||
| **group / key (BCC)** | `JointPKID = SHAKE256("PULSAR-BCC-CEF/joint-pk-id/v1" ‖ mode ‖ pub.Bytes)` | `distributed_bcc.go:1096` | the BCC key-identity root |
|
||||
| **committee / participant set (RSS)** | per-subset secret keyed by `(leaderSeed, maskS)`; holdings indexed by party; session id `= H(pub ‖ active ‖ μ)` | `mithril_rss.go:84`, `mithril_rss_hyperball.go:1032` | binds the run to (pub, exact active set, message) |
|
||||
| **participant set (BCC)** | `committeeID = SHAKE256("PULSAR/committee-id/v1" ‖ JointPKID ‖ sorted quorum)`; DKG: `committeeRoot` | `nonce_ledger.go`; `dkg.go:516` | binds the exact sorted quorum + key |
|
||||
| **threshold `t`** | enforced by `CanonicalSignerSet(valid, threshold)` (BCC) / `validateActive` (hyperball, `:1054`) — exactly `t` distinct signers | `distributed_bcc.go`; `mithril_rss_hyperball.go:1054` | `t` is *enforced* at aggregation but not hashed into the committee id — bind `t` at the cert layer (`PULSAR.md §11`) |
|
||||
| **policy id** | `Policy [32]byte` in `NonceBinding`, canonical-encoded | `nonce_ledger.go` | auditable domain tag (block-cert vs warp-msg, …) |
|
||||
| **message** | `μ = deriveMuCtx(tr, ctx, msg)` folded into `c̃`/session id; BCC reservation `Digest = SHAKE256("PULSAR/nonce-binding-digest/v1" ‖ mode ‖ μ)` | `mithril_rss_hyperball.go:799`; `nonce_ledger.go` | binds the run to exactly what is signed |
|
||||
| **chain / network** | via FIPS-204 `ctx` string + `Policy` | `distributed_bcc.go:586` | full `chain_id` + `committee_plan_hash` binding is the **cert-layer target** (`PULSAR.md §8`, §13) |
|
||||
|
||||
### §3.1 Nonce single-use binding (anti key-recovery)
|
||||
- **BCC.** Dedup key `nonceMaterialKey(w1) = SHAKE256("PULSAR/nonce-single-use/v1"
|
||||
‖ w1)` — **`w1` ALONE** (`nonce_ledger.go:395`): dropping the label defeats
|
||||
relabel-bypass; dropping `committeeID` closes cross-committee reuse. Reuse ⇒
|
||||
`ErrNonceReused` (`:80`), fail-closed, before any secret is emitted. Defends
|
||||
against `z_A − z_B = (c_A − c_B)·s1`.
|
||||
- **Hyperball.** Per-round, per-slot nonce seed
|
||||
`hyperballNonceSeed(roundEntropy, sid, id, slot)` (`mithril_rss_hyperball.go:991`)
|
||||
is fresh per round (distinct entropy ⇒ distinct mask) and deterministic within a
|
||||
round (so the Round-1 commitment binds the mask before the challenge is known).
|
||||
`TestHyperballNonceReuseFatal` (`:419`) proves reuse would recover the share and
|
||||
that the derivation prevents it.
|
||||
|
||||
### §3.2 Authenticated-message slot binding
|
||||
`ProtocolMessageTBS(author, ctx, payloadDigest)` (`protocol_auth.go:59`) is
|
||||
SP 800-185-framed over `("PULSAR/protocol-msg/v1", author, be64(epoch), sessionID,
|
||||
nonceID, {round}, payloadDigest)`. Equivocation is per `(Author, Epoch, SessionID,
|
||||
Round)`; two valid signatures on distinct payloads for one slot is non-repudiable
|
||||
(`DetectEquivocation`, `protocol_auth.go:101`).
|
||||
|
||||
---
|
||||
|
||||
## §4. Deliverable 4 — Share-commitment format (with the honest BDLOP flag)
|
||||
|
||||
Three distinct "commitment" notions exist; do not conflate them.
|
||||
|
||||
### §4.1 RSS replicated-share commitment (implemented) — the dealerless key root
|
||||
The RSS key's binding is the published FIPS-204 public key itself: `pub = rho ‖
|
||||
PackT1(t1)` with `t1 = HighBits(A·s1 + s2)` (`mithril_rss.go:192`–`:215`). Each
|
||||
subset secret is a short `χ_η` value keyed by `(leaderSeed, maskS)`; the
|
||||
**dealerless guarantee** is structural (no party holds all subsets,
|
||||
`TestMithrilRSSDealerless` `mithril_rss_test.go:91`), and the **norm bound**
|
||||
`‖s2‖∞ ≤ C·η` keeps it stock-FIPS-204-signable. This is **not** a hiding
|
||||
per-coefficient lattice commitment; it is the public-key root + structural
|
||||
replication.
|
||||
|
||||
### §4.2 Hyperball `w`/`T` commitments (implemented) — binding, not hiding
|
||||
- `CommitW = hyperballCommitW(sid, id, slot, μ, w_{j,k})` (`:1004`): a SHAKE
|
||||
hash-commitment binding each per-slot `w` so a rushing adversary cannot choose
|
||||
`w` after seeing others (verified at `:466`).
|
||||
- `CommitT = hyperballCommitT(sid, id, T_j)` (`:1019`): commitment to the
|
||||
share-verification value `T_j = A·s1_(j)`, revealed **only on blame** — in the
|
||||
honest path `T_j` is never revealed, because `Σ_active T_j = A·s1 = t − s2` would
|
||||
leak `s2`.
|
||||
|
||||
### §4.3 BCC sign-side share-commitment (the BDLOP plug point) — **nil today, flagged**
|
||||
`AlgSetup.s1ShareCommit` holds the per-party hiding commitment to the dealt
|
||||
`s1`-share for identifiable-abort binding. **It is `nil` today**; the single source
|
||||
of truth read by both prover and verifier is `shareCommitmentsFor` (returns
|
||||
`(nil, nil)`, `share_commit.go:94`–`:96`). The intended format is BDLOP
|
||||
(`ia.cr/2017/1235` / Ajtai) under a **separate** public matrix `B` hiding under
|
||||
M-LWE (`Com_s_i = B·r_s_i + embed(s1_i)`, `share_commit.go:42`).
|
||||
|
||||
**Honest consequence (the residual).** Because `s1ShareCommit` is nil, a
|
||||
**valid-sigma but WRONG-`z`** partial is **not yet attributable** — it is bounded
|
||||
to a **liveness** fault (never forgery, never leak: the wrong aggregate fails
|
||||
FIPS-204 verify and nothing secret crosses the wire), marked by
|
||||
`ErrIdentifiableAbortResidual` (`share_commit.go:73`). The hyperball signer has the
|
||||
**same** residual at `blameSlot` (`mithril_rss_hyperball.go:633`–`637`): a share
|
||||
inconsistent with keygen but self-consistent with its own equivocated `T_j` passes
|
||||
the per-party check, is caught by the fail-closed release gate (no bad signature
|
||||
emitted), but is not pinpointed.
|
||||
|
||||
---
|
||||
|
||||
## §5. Deliverable 5 — Valid / invalid DKG (and signing) test vectors
|
||||
|
||||
The structured behavioral vectors live in **`vectors/dkg-proof-boundary.json`**.
|
||||
Each names the scenario, the layer, the expected outcome, the **exact code
|
||||
error/blame constant**, and the `file:line` that enforces it. They are *spec-level
|
||||
state vectors* — distinct from the byte-level wire KATs (§6). Summary:
|
||||
|
||||
**Positive (accept):**
|
||||
- `keygen/rss-dealerless-stock-circl` — dealerless RSS key signs under unmodified
|
||||
circl `mldsa65.Verify` for all 15 committees N ≤ 6
|
||||
(`TestMithrilRSSStockCirclVerify`, `mithril_rss_test.go:38`,`:70`) and T=N at
|
||||
n=8/n=16 (`mithril_rss_n8_test.go:40`). **The gold proof of dealerless
|
||||
stock-FIPS-204 signability.**
|
||||
- `keygen/rss-dealerless-structural` — no party holds all subsets; no
|
||||
`(T−1)`-coalition covers all subsets (`TestMithrilRSSDealerless`,
|
||||
`mithril_rss_test.go:91`).
|
||||
- `sign/hyperball-no-reconstruct` — the 3-round hyperball signature over the RSS
|
||||
key verifies under stock circl with NO key reconstruction; AST + transcript
|
||||
oracles prove no `s1`/`s2`/`y` ever forms (`TestHyperballStockCirclVerify`
|
||||
`mithril_rss_hyperball_test.go:41`; `TestHyperballNoReconstructStructural` `:100`).
|
||||
- `sign/circl-roundtrip` — no-reconstruct BCC/CEF `(c̃,z,h)` accepted by circl
|
||||
(`TestBCCSignRoundTripVerifiesCIRCL`, `bcc_sign_test.go:86`; no-leak oracle
|
||||
`:217`).
|
||||
- `dkg/seed-equivalence` (legacy seed-share lineage) — `GroupPK ==
|
||||
KeyFromSeed(masterSeed).Pub`, reconstructed-key sig verifies under FIPS-204
|
||||
(`TestDKG_ProducesValidPubkey_VerifiableSign`, `dkg_test.go:147`,`:206`).
|
||||
|
||||
**Negative (reject / blame), each grounded in a real constant:**
|
||||
- `keygen/rss-bad-committee` (non-viable `(T,N)`: norm-blown or structural) →
|
||||
`rss.ValidateCommittee` error (`TestMithrilRSSRejectsBadCommittee`,
|
||||
`mithril_rss_test.go:177`).
|
||||
- `sign/hyperball-sub-threshold` (too few / too many / unsorted / duplicate /
|
||||
out-of-range active) → `ErrHyperballActive` / `validateActive`
|
||||
(`TestHyperballSubThresholdFailsClosed`, `mithril_rss_hyperball_test.go:298`).
|
||||
- `sign/hyperball-biased-partial` → no slot verifies (fail-closed release gate);
|
||||
`blameSlot` pinpoints the culprit leak-free
|
||||
(`TestHyperballBiasedPartialCaughtAndBlamed`, `:329`).
|
||||
- `sign/hyperball-equivocation` (party changes `w` between rounds) → binding
|
||||
mismatch (`TestHyperballEquivocationCaught`, `:404`,
|
||||
`aggregateCommitments` `:466`).
|
||||
- `sign/hyperball-mask-on-wire` (the secret mask `y` must not appear on the wire)
|
||||
→ asserted absent (`TestHyperballMaskNeverOnWire`, `:529`).
|
||||
- `sign/nonce-reuse` (BCC) → `ErrNonceReused` (`nonce_ledger.go:80`).
|
||||
- `sign/session-mismatch` → `BlameSessionMismatch` (`blame.go:38`).
|
||||
- `sign/duplicate-partyid` → `BlameDuplicatePartyID` (`blame.go:34`).
|
||||
- `sign/unknown-party` → `BlameUnknownParty` (`blame.go:36`).
|
||||
- `sign/malformed-partial` → `BlameMalformed` (`blame.go:32`).
|
||||
- `sign/invalid-proof` → `BlameProofInvalid` (`blame.go:40`).
|
||||
- `sign/forged-victim-slot` → dropped pre-attribution, victim **not** blamed
|
||||
(`distributed_bcc.go:883`).
|
||||
- `sign/valid-sigma-wrong-z` → liveness fault, not yet attributable
|
||||
(`ErrIdentifiableAbortResidual`, `share_commit.go:73`).
|
||||
- `keygen/naive-additive-byte-fips` → `ErrDealerlessByteFIPSUnreachable` for any
|
||||
committee `parties ≥ 2` (`naive_additive_seta_obstruction.go:152`,`:242`). RSS is
|
||||
the named escape; the naive additive lift stays correctly fail-closed.
|
||||
- `dkg/equivocation`, `dkg/bad-share`, `dkg/missing-participant`,
|
||||
`dkg/node-not-in-committee`, `dkg/duplicate-committee`, `dkg/empty-committee`
|
||||
(legacy seed-share lineage) → `ComplaintEquivocation` / `ComplaintBadDelivery` /
|
||||
`ErrTooFew*` / `ErrNotInCommittee` / `ErrCommitteeDuplicate` /
|
||||
`ErrCommitteeEmpty` (`dkg.go`, `types.go:285`,`:290`).
|
||||
|
||||
---
|
||||
|
||||
## §6. Deliverable 6 — Cross-version KATs (old wire compatibility)
|
||||
|
||||
The committed wire KATs are the **cross-version compatibility suite**: vectors
|
||||
generated by an earlier version, replayed every CI run; drift = gate failure.
|
||||
Runner `kat_test.go`, reads `vectors/*.json`. The v0.6.1/.2 mlwe de-dup was
|
||||
**byte-preserving** — these KATs replay identically after the refactor.
|
||||
|
||||
| Vector file | Entries | Pins | Replay test |
|
||||
|---|---|---|---|
|
||||
| `vectors/keygen.json` | 9 | `seed → public_key, private_key` | `TestKAT_Keygen_Replay` (`kat_test.go:50`) |
|
||||
| `vectors/sign.json` | 9 | `seed,msg,ctx → signature` | `TestKAT_Sign_Replay` (`kat_test.go:91`) |
|
||||
| `vectors/verify.json` | 6 | `public_key,msg,signature → accept` | `TestKAT_Verify_Replay` (`kat_test.go:127`) |
|
||||
| `vectors/threshold-sign.json` | 4 | `n,t,msg,public_key → signature` (Class N1 interchangeability) | `TestKAT_ThresholdSign_Replay` (`kat_test.go:159`) |
|
||||
| `vectors/dkg.json` | 3 | DKG replay | `TestKAT_DKG_Replay` (`kat_test.go:197`) |
|
||||
|
||||
`threshold-sign.json[0]` (`Pulsar-65`, `n=3, t=2`) pins a *threshold* signature
|
||||
that the **single-party** verifier accepts — the wire-level statement of Claim (A)
|
||||
across versions.
|
||||
|
||||
**Cross-implementation KAT.** `TestDKGVSS_RingMLDSA65_ExpandABinding_KAT`
|
||||
(`dkg_vss_kat_test.go:104`) anchors the shared `luxfi/dkg` ring against pulsar's own
|
||||
FIPS-204 arithmetic: `A = ExpandA(rho)` round-trips with no spurious Montgomery
|
||||
factor and the dkg ring recomputes `t1 = Power2Round(A·s1+s2)` **byte-identical to
|
||||
circl**. Its header (`:30`–`:35`) restates the historical residual honestly: the
|
||||
*vss* no-reconstruct group key `T = A·s1 + B·u` (large `s2 = B·u`) is not directly
|
||||
BCC-signable — which is exactly why **RSS** (small `s2 = Σ χ_η`), not vss, is the
|
||||
dealerless keygen that beats the wall.
|
||||
|
||||
---
|
||||
|
||||
## §7. Deliverable 7 — Proof checklist (test → security property)
|
||||
|
||||
Assurance tags are the `PROOF-CLAIMS.md` vocabulary (machine-checked ·
|
||||
sound-by-reduction · interop-tested · test-proven · fail-closed-pending-review ·
|
||||
open-research). The split is always **(A) verifier-compat** vs **(B) Lux
|
||||
construction**.
|
||||
|
||||
| # | Security property | Test / artifact (file:line) | Claim | Assurance |
|
||||
|---|---|---|---|---|
|
||||
| 1 | **Standard-verifier compat — no-reconstruct BCC** — `(c̃,z,h)` accepted by circl + negatives | `TestBCCSignRoundTripVerifiesCIRCL` `bcc_sign_test.go:86` | **A** | **interop-tested** |
|
||||
| 2 | **Standard-verifier compat — dealerless RSS key** — stock circl accepts (all N ≤ 6; T=N n=8/n=16) | `TestMithrilRSSStockCirclVerify` `mithril_rss_test.go:38`; `TestMithrilRSS_LargeN_StockCircl` `mithril_rss_n8_test.go:16` | **A** | **interop-tested** |
|
||||
| 3 | **Standard-verifier compat — no-reconstruct hyperball over RSS** | `TestHyperballStockCirclVerify` `mithril_rss_hyperball_test.go:41` | **A** | **interop-tested** |
|
||||
| 4 | **Dealerless keygen (structural)** — no party holds all subsets; no `(T−1)` covers all | `TestMithrilRSSDealerless` `mithril_rss_test.go:91` | B | test-proven |
|
||||
| 5 | **Secrecy / no-reconstruct (hyperball)** — no `s1`/`s2`/`y`/`w0`/`sk` forms; no `ReconstructKeyMaterial` call; mask never on wire | `TestHyperballNoReconstructStructural` `:100`; `TestHyperballMaskNeverOnWire` `:529` | B | test-proven (AST + transcript oracle) |
|
||||
| 6 | **Secrecy / no-reconstruct (BCC)** — no `s1`/seed/`sk`/`c·s2`/`c·t0`/`w` forms | `assertBCCTranscriptNoLeak` `bcc_sign_test.go:217`; `gate2_reachability_test.go`; Lean `Crypto.Pulsar.NoLeakAggregate` | B | machine-checked (Lean core) + test-proven; reduction sound-by-reduction (M-LWE/M-SIS) |
|
||||
| 7 | **Any-quorum consistency** — every T-quorum reconstructs the identical key | `TestMithrilRSSAnyQuorumSameKey` `mithril_rss_test.go:122` | B | test-proven |
|
||||
| 8 | **Binding — domain separation** — per-purpose DSTs, no reuse | §2 tables; `transcript.go:40`–`:66`; RSS/hyperball prefixes | B | test-proven (KAT-pinned) |
|
||||
| 9 | **Binding — equivocation** — one author/commitment per slot | `TestHyperballEquivocationCaught` `:404`; `DetectEquivocation` `protocol_auth.go:101`; `TestDKG_Equivocation_Detected` `dkg_test.go:111` | B | test-proven |
|
||||
| 10 | **Robustness / identifiable abort + fail-closed** — sub-threshold/biased/malformed rejected & (where possible) attributed | `TestHyperballSubThresholdFailsClosed` `:298`, `TestHyperballBiasedPartialCaughtAndBlamed` `:329`; `AggregateBCCWithBlame` `distributed_bcc.go:875`; `blame_gate_test.go` | B | test-proven (semi-honest) |
|
||||
| 11 | **Robustness residual** — valid-sigma wrong-`z` / equivocated-keygen-share attribution | `share_commit.go:73` `ErrIdentifiableAbortResidual`; `mithril_rss_hyperball.go:633` | B | **fail-closed-pending-review** (BDLOP) |
|
||||
| 12 | **Unforgeability — nonce single-use** — defeats `(c_A−c_B)·s1` recovery | BCC `nonce_ledger.go:80`; hyperball `TestHyperballNonceReuseFatal` `:419` | B | test-proven |
|
||||
| 13 | **Unforgeability — base EUF-CMA** — output is a standard ML-DSA sig | inherits ML-DSA EUF-CMA under M-LWE/M-SIS (output bytes = FIPS-204) | A→B | sound-by-reduction (inherited) |
|
||||
| 14 | **Authenticated origin** — forged victim-slot partial cannot frame/exclude | `distributed_bcc.go:883`; `ErrOriginAuthRequired` `:813` | B | test-proven |
|
||||
| 15 | **Cross-version wire compat** — committed KATs replay byte-identical (incl. post-mlwe-dedup) | `kat_test.go:50`,`:91`,`:127`,`:159`,`:197` vs `vectors/*.json` | A | interop-tested |
|
||||
| 16 | **Cross-impl arithmetic** — `luxfi/dkg` ring reproduces FIPS-204 `t1` | `TestDKGVSS_RingMLDSA65_ExpandABinding_KAT` `dkg_vss_kat_test.go:104` | A | interop-tested |
|
||||
| 17 | **Keygen — naive-additive byte-FIPS obstruction (correctly fail-closed)** | `assessDealerlessFIPS` `naive_additive_seta_obstruction.go:196`; `DealerlessMLDSADKG` `:242` → `ErrDealerlessByteFIPSUnreachable` `:152` | B | sound-by-reduction (parameter-derived) |
|
||||
| 18 | **Keygen residual — FIPS-204 KeyGen-distribution-equivalence** (unbiased composite secret, hiding vs `<t`, abort-bias) for the RSS key | **not proven**; structural facts + stock-circl-verifiability only (rows 2,4) | B | **open-research** |
|
||||
|
||||
### §7.1 What the checklist deliberately does NOT claim
|
||||
Rows 11, 18 are **residuals**, fail-closed and tracked, not silently weakened. No
|
||||
row asserts FIPS/NIST-certified threshold ML-DSA, fully-malicious-secure-*proven*,
|
||||
or global-`N`-validator DKG (`PROOF-CLAIMS.md §0`). Claim (A) (rows 1, 2, 3, 13,
|
||||
15, 16) is the *proven* verifier-compatibility statement; Claim (B) (the rest) is
|
||||
the *scoped* Lux construction. The keygen story for v0.6.3: KEYGEN is **dealerless
|
||||
RSS** (no dealer; no party holds the key; stock-FIPS-204-verifiable — rows 2, 4),
|
||||
and the remaining (B) gap is the *distributional* KeyGen-equivalence proof (row
|
||||
18), not the existence of a dealerless committee key.
|
||||
@@ -0,0 +1,695 @@
|
||||
# PULSAR — Dealerless Committee-Threshold ML-DSA Certificate Layer
|
||||
|
||||
> **Status.** Architecture specification, current to **v0.6.3** (`git log`
|
||||
> → `0650729`, `origin/main`). This document defines the *certificate layer* of
|
||||
> Pulsar: how **dealerless** committee-threshold ML-DSA is organized into epochs,
|
||||
> committees, signing sessions, and on-chain-verifiable certificates so that it
|
||||
> scales to a permissionless validator set of N > 1000 by **sampling many small
|
||||
> committees and accumulating confidence by repetition** (Avalanche-native), not
|
||||
> by pushing one giant Shamir/FROST sharing across all N. It is the
|
||||
> consensus-integration companion to the algorithm-level NIST-MPTC submission
|
||||
> spec (`spec/pulsar.tex`, `spec/parameters.tex`, `spec/system-model.tex`) and
|
||||
> the proofs under `~/work/lux/proofs/pulsar/`.
|
||||
>
|
||||
> **SPEC + grounded reality.** Sections labelled *implemented today* cite the
|
||||
> real reference implementation under `ref/go/pkg/pulsar/` at v0.6.3; sections
|
||||
> labelled *consensus target* are the integration surface to build. No code is
|
||||
> changed by this document.
|
||||
|
||||
---
|
||||
|
||||
## 0. Claim discipline (read first)
|
||||
|
||||
This layer makes **two distinct claims that must never be conflated**. Most
|
||||
flawed "threshold post-quantum" marketing collapses them; Pulsar keeps them
|
||||
apart on purpose.
|
||||
|
||||
- **Claim (A) — FIPS-204 verification *compatibility* — PROVEN.** The verifier
|
||||
boundary is **standard, unmodified** FIPS-204 ML-DSA verification:
|
||||
|
||||
```
|
||||
Verify_MLDSA(GroupPK, digest, sig) ∈ {accept, reject}
|
||||
```
|
||||
|
||||
The threshold-produced `(c̃, z, h)` is byte-for-byte a FIPS-204 signature; a
|
||||
stock verifier (`cloudflare/circl` `mldsa65.Verify` / `mldsa87.Verify`,
|
||||
BoringSSL/AWS-LC FIPS ML-DSA, OpenSSL 3.x PQ provider) accepts it with **no
|
||||
Pulsar code in the verify path**. This is proven today for:
|
||||
- the no-reconstruct BCC/CEF signer over a single group key
|
||||
(`ref/go/pkg/pulsar/bcc_sign_test.go:86`, `TestBCCSignRoundTripVerifiesCIRCL`);
|
||||
- the **dealerless RSS** group key, signed and verified under stock circl for
|
||||
every viable committee N ≤ 6 and the T = N committees n=8,t=8 / n=16,t=16
|
||||
(`mithril_rss_test.go:38`, `mithril_rss_n8_test.go:16`);
|
||||
- the **no-reconstruct hyperball** signer over the dealerless RSS key
|
||||
(`mithril_rss_hyperball_test.go:41`, `TestHyperballStockCirclVerify`).
|
||||
|
||||
- **Claim (B) — DKG/threshold *construction* soundness — Lux-authored, SCOPED.**
|
||||
The dealerless key generation (RSS / Mithril) and the threshold signing
|
||||
protocols (BCC/CEF/CSCP + hyperball) are a **Lux-authored construction**. Its
|
||||
security is argued by reduction to ML-DSA EUF-CMA under Module-LWE /
|
||||
Module-SIS, *plus* the protocol-level privacy/abort properties argued in
|
||||
`~/work/lux/proofs/pulsar/`. This is **our** theorem, not NIST's, and parts of
|
||||
it are **scoped residuals** (§18) — labelled, fail-closed, never silently
|
||||
weakened.
|
||||
|
||||
**What we never say.** There is no such thing as "FIPS-certified threshold
|
||||
ML-DSA" or "NIST-certified threshold ML-DSA." FIPS 204 standardizes
|
||||
*single-party* ML-DSA KeyGen/Sign/Verify. We never claim
|
||||
fully-malicious-secure-*proven* (mechanized) or a global-1000-validator DKG.
|
||||
Conformance language is always one of: "verifies under unmodified FIPS-204"
|
||||
(Claim A), or "Lux-authored threshold construction, reduction in
|
||||
`proofs/pulsar/`" (Claim B).
|
||||
|
||||
**The honest one-line scope (canonical).** *Dealerless committee key generation
|
||||
(RSS / Mithril) + no-reconstruct signing (BCC/CSCP, and the Mithril hyperball
|
||||
3-round signer) + standard-FIPS-204-verifier output, malicious-hardened; the
|
||||
full FIPS-204 KeyGen-distribution-equivalence proof and the malicious-secure
|
||||
CSCP/identifiable-abort layer are labelled residuals.*
|
||||
|
||||
---
|
||||
|
||||
## 1. Why a committee certificate layer, and why not Shamir/FROST end-to-end
|
||||
|
||||
ML-DSA is not Schnorr. Four features break Schnorr-style threshold composition:
|
||||
|
||||
1. **Small secrets.** `s1, s2` are sampled uniformly from
|
||||
`S_η = {p ∈ R_q : ‖p‖∞ ≤ η}` (η = 4 for ML-DSA-65, η = 2 for ML-DSA-87). The
|
||||
*entire* parameter set is calibrated to this bound.
|
||||
2. **Rejection sampling.** Signing loops until `‖z‖∞ < γ1 − β` and
|
||||
`‖r0‖∞ < γ2 − β`; the accepted distribution is not a simple linear image of
|
||||
the inputs.
|
||||
3. **Decompose / rounding.** `w1 = HighBits(A·y)` and `r0 = LowBits(w − c·s2)`
|
||||
are non-linear; there is no homomorphic commitment to `w1` over additive
|
||||
nonce shares — this is precisely why naive FROST-style additive-nonce
|
||||
threshold ML-DSA is impossible.
|
||||
4. **Hints.** The signature carries `h = MakeHint(...)`; recovering it from
|
||||
shares without leaking the key residual `c·t0 − c·s2` is the delicate part.
|
||||
|
||||
Consequence for the *key* layer — the naive-additive obstruction:
|
||||
|
||||
- **Naive Lagrange/additive DKG blows the norm.** A dealerless joint secret
|
||||
formed as a *sum / Lagrange combination* of N ≥ 2 independent `S_η`
|
||||
contributions has `‖s2_joint‖∞ ≤ N·η`, hence `‖c·s2_joint‖∞ ≤ N·β`. This
|
||||
violates both the BCC boundary-clearance hypothesis (`‖c·s2‖∞ ≤ β`) and
|
||||
ML-DSA's `S_η`-calibrated EUF-CMA. This **naive-additive obstruction is
|
||||
computed, not asserted**, in
|
||||
`ref/go/pkg/pulsar/naive_additive_seta_obstruction.go:196`
|
||||
(`assessDealerlessFIPS`: `JointS2Linf = N·η`, `JointCS2Linf = N·β`) and is the
|
||||
reason the *naive* dealerless entry point fails closed
|
||||
(`ErrDealerlessByteFIPSUnreachable`, `naive_additive_seta_obstruction.go:152`).
|
||||
**It is the naive *lift* only — it does *not* prove a general impossibility**;
|
||||
the file's own header (`:84`–`:107`) lists the escape: a sharing whose
|
||||
reconstruction stays in `S_η` *by construction*.
|
||||
|
||||
**That escape is now built (v0.6.0+): Mithril short Replicated Secret Sharing
|
||||
(RSS).** The key is the *plain sum of `C(N, N−T+1)` fresh short `χ_η` subset
|
||||
secrets*, so `‖s2‖∞ ≤ C·η` stays genuinely small (§4). RSS does **not** form an
|
||||
N-way additive blow-up — it sidesteps the obstruction the obstruction file
|
||||
itself names. The dealer is dead **at keygen too**, not just at signing.
|
||||
|
||||
So Pulsar does **not** push one global Shamir/FROST sharing across all N
|
||||
validators, and it does **not** rely on a trusted dealer. Instead it **scales by
|
||||
sampling many small dealerless committees** and treats the *certificate* (an
|
||||
epoch/committee-bound, stock-FIPS-204-verifiable ML-DSA signature) as the unit
|
||||
of composition (§5, §12).
|
||||
|
||||
---
|
||||
|
||||
## 2. What exists today (grounded in `ref/go/pkg/pulsar/` @ v0.6.3)
|
||||
|
||||
| Concern | Implemented today (file:line) |
|
||||
|---|---|
|
||||
| (A) Threshold output verifies under **unmodified FIPS-204** | **DONE** — `bcc_sign_test.go:86` checks a no-leak BCC/CEF signature byte-for-byte under independent `circl` `mldsa65/87.Verify` (+ tamper / wrong-msg / wrong-ctx negatives). |
|
||||
| **Dealerless** committee keygen | **DONE (RSS / Mithril)** — `mithril_rss.go:133` `MithrilRSSKeygen`: no trusted dealer; each subset's short secret is sampled by that subset's leader and replicated; no party holds the whole `(s1,s2)`. Stock-circl-verifiable: `mithril_rss_test.go:38` (all 15 committees N ≤ 6), `mithril_rss_n8_test.go:16` (T=N at n=8, n=16). |
|
||||
| Large-committee keygen (arithmetic) | **DONE (v0.6.3)** — per-subset reduction `accumulateSubset` (`mithril_rss.go:122`) fixes a uint32 overflow that wrapped the key once `C(N,N−T+1) ≥ 512`; unblocks the owner-default large committees (e.g. n=16,t=14, `C(16,3)=560`). |
|
||||
| No-reconstruct online signing (single group key) | **DONE** — `distributed_bcc.go:645` partial `z_i = λ_i·y_i + c·λ_i·s1_i`; `AggregateBCCWithBlame` (`:875`) sums to `z = ȳ + c·s1` **without ever forming `s1`** (let alone the seed); hint from public `w' = A·z − c·t1·2^d`. |
|
||||
| **No-reconstruct signing over the dealerless RSS key** | **DONE (hyperball, gates 5/6)** — `mithril_rss_hyperball.go:780` `SignHyperball`: the Mithril 3-round protocol; each party emits only `z_j = y_j + c·s1_(j)`; **no party or coordinator forms** the full `s1`, any `s2`, `t0`, the mask `y`, the commitment `w`, `w0`, or any `sk`. |
|
||||
| Malicious hardening | **DONE (v0.5)** — nonce single-use safe-by-construction (`nonce_ledger.go`), authenticated-PartyID blame / identifiable abort (`blame.go`, `protocol_auth.go`), origin-auth safe-by-default (`ErrOriginAuthRequired`, `distributed_bcc.go:813`), GATE-2 call-graph reachability (`gate2_reachability_test.go`). |
|
||||
| Offline preprocessing / ticket factory (TALUS) | **BUILT (semi-honest)** — TALUS `talus.go`, CEF `talus_cef.go`, CSCP secure-comparison `talus_cscp.go` (W-LEAK closed semi-honest, simulation-proven). |
|
||||
| Shared lattice base | **DONE (v0.6.1/.2)** — transcript, Shamir, SHAKE samplers, and the ML-DSA ring core routed onto `github.com/luxfi/mlwe` (byte-preserving); Pulsar and Corona share one Module-LWE base. |
|
||||
| Committee/epoch object model + on-chain registry | **Consensus target** — the sampled-certificate finality layer (§12) lives in `luxfi/consensus`; the pulsar repo supplies the per-committee keygen + signing primitive each committee runs. |
|
||||
|
||||
The load-bearing fact, restated for v0.6.3: **dealerless keygen and
|
||||
no-reconstruct signing are both built and stock-FIPS-204-verifiable.** The open
|
||||
work (B) is the *full KeyGen-distribution-equivalence proof* and the
|
||||
*malicious-secure CSCP / identifiable-abort* layer (§18), not the existence of a
|
||||
dealerless committee key.
|
||||
|
||||
---
|
||||
|
||||
## 3. Version lineage (the certificate kernel's own ledger)
|
||||
|
||||
> Read alongside `ref/go/pkg/pulsar/VERSIONS.md` (the gate-read track ledger) and
|
||||
> `PROOF-CLAIMS.md` (the assurance vocabulary). Package-version scheme (distinct
|
||||
> from the repo's `vX` module tags).
|
||||
|
||||
| Version | What it is | Status |
|
||||
|---|---|---|
|
||||
| **v0.3 — algebraic broadcast** | The `AlgebraicAggregate` path broadcast per-party `c·s2`/`c·t0` residual shares and reconstructed the `MakeHint` residual at the aggregator. | **REMOVED** — leaked the long-term key (PULSAR-V13-HINT-LEAK). Ripped out forward-only; no backward-compatible re-entry. |
|
||||
| **v0.4 — BCC/CSCP no-reconstruct** | Boundary-Clearance-Condition (BCC) + Carry-Elimination (CEF) + CarryCompare secure-comparison (CSCP). Each member holds one poly-vector Shamir share of `s1`; signing aggregates only masked `z`-partials; the hint comes from the public `w' = A·z − c·t1·2^d`. No process forms `s1`, the seed, `sk`, `c·s2`, `c·t0`, `r0`, or full `w`. | **Production sign path.** |
|
||||
| **v0.5 — malicious hardening** | Nonce single-use *safe by construction* (`w1`-only dedup, per-share registry); authenticated-PartyID blame (forged victim-slot partials dropped before attribution); origin-auth *safe by default* (`ErrOriginAuthRequired`); identifiable-abort plumbing; GATE-2 reachability + indirection lint; CI pure-Go / no-`legacy_trusted_dealer` invariants. | **Merged, RED-verified 0 crit/high.** Malicious-**hardened**, not fully-malicious-secure-*proven*. |
|
||||
| **v0.6.0 — dealerless RSS keygen** | *The dealer is dead at keygen too.* Mithril short Replicated Secret Sharing (`ia.cr/2026/013`): the key is the sum of `C(N,N−T+1)` fresh `χ_η` subset secrets (`‖s2‖∞ ≤ C·η`, genuinely small), sampled leaderwise and replicated; no party holds all subsets. Signs byte-for-byte under stock circl. | **Built.** `mithril_rss.go`. |
|
||||
| **v0.6.1 / v0.6.2 — mlwe de-dup** | Route transcript → `mlwe/transcript`, Shamir → `mlwe/share`, SHAKE samplers → `mlwe/sample/shake`, ML-DSA ring core → `mlwe/ring/mldsa`. Byte-preserving (all KATs replay identically). Pulsar + Corona on one Module-LWE base. | **Built.** |
|
||||
| **v0.6.3 — RSS overflow fix** | `accumulateSubset` reduces mod q *per subset*; without it, summing all `C(N,M)` `χ_η` coefficients (each stored ≈ q ≈ 2²³) overflows uint32 once `C ≥ ⌊2³²/q⌋ = 512`, wrapping the key into an unsignable large-secret wall key. Mod-q is additively homomorphic ⇒ small committees (n ≤ 8) are byte-unchanged. | **Built (current `main`).** `mithril_rss.go:110`–`127`. |
|
||||
| **+ HYPERBALL signer** | The Mithril 3-round no-reconstruct threshold signer for the RSS key: each party reveals only `z_j = y_j + c·s1_(j)` under a leak-free Excess gate; the summed `z` is a standard FIPS-204 response. Gates 5 (verifies under stock circl, no reconstruction) and 6 (fail-closed). | **Built.** `mithril_rss_hyperball.go`. Lands on the dealerless RSS keygen (commits `645b5c5`→`0faa086`). |
|
||||
|
||||
---
|
||||
|
||||
## 4. Dealerless RSS keygen — the dealer is dead at keygen
|
||||
|
||||
`MithrilRSSKeygen(mode, t, n, partySeeds)` (`mithril_rss.go:133`) runs the
|
||||
dealerless Mithril RSS DKG for an `(T, N)` committee, driven by one contributed
|
||||
32-byte seed per party. There is **no trusted dealer**.
|
||||
|
||||
**Construction.** For every `M`-subset `S` of the committee (`M = N − T + 1`),
|
||||
that subset's **leader** (lowest-indexed member) derives a 64-byte sampling seed
|
||||
from its own contributed entropy (`mithrilSubsetSeed`, `:84`, domain-separated
|
||||
`"pulsar.mithril.rss.subset.v1"`), samples a short secret
|
||||
`(s1^(S), s2^(S)) ∈ S_η` from it, and replicates it to the subset's members and
|
||||
to no one else (`:169`–`182`). The composite key is the plain sum
|
||||
`s1 = Σ_S s1^(S)`, `s2 = Σ_S s2^(S)`; the public key `t = A·s1 + s2` is
|
||||
Power2Round-split into `(t0, t1)` exactly as `deriveKeyMaterial` / circl does
|
||||
(`computePublicKey`, `:192`), so the published `t1` is **byte-identical to what
|
||||
circl derives** from `(rho, s1, s2)`.
|
||||
|
||||
**Why it beats the pick-2 wall (the obstruction's named escape).** The
|
||||
vss/large-blinding dealerless DKG yields `t = A·s1 + B·u` with `‖B·u‖∞ ≈ q/2` —
|
||||
far outside `S_η` — so `FindHint` never fits a ±1 hint of weight ≤ ω and **no**
|
||||
byte-stock-FIPS-204 signature exists. RSS keeps every share short:
|
||||
`‖s2‖∞ ≤ C(N,N−T+1)·η`, genuinely small. The BCC signer recovers the hint from
|
||||
the **public** `w' = A·z − c·t1·2^d` exactly as the verifier does, so the small
|
||||
`s2` only lowers the per-nonce acceptance rate — it never breaks verifiability
|
||||
(`mithril_rss.go:12`–`23`).
|
||||
|
||||
**Dealerless guarantee (structural).** No single party is a member of every
|
||||
subset (T ≥ 2), so no party ever holds the whole `(s1, s2)`; any T parties cover
|
||||
all subsets and reconstruct via the balanced partition; fewer than T are
|
||||
disjoint from at least one whole subset whose fresh short secret masks the key.
|
||||
Proven for the entire viability range by `TestMithrilRSSDealerless`
|
||||
(`mithril_rss_test.go:91`): no party holds all subsets, and no `(T−1)`-coalition
|
||||
covers all subsets.
|
||||
|
||||
**Admission (the per-(N,T) norm bound, not a flat cap).** A committee is
|
||||
admitted iff `2 ≤ T ≤ N ≤ 63` **and** `τ·C(N,N−T+1)·η < γ2` (`luxfi/dkg`
|
||||
`rss.ValidateCommittee`). The second condition is load-bearing: the signer's
|
||||
hint term `‖c·s2‖∞ ≤ τ·C·η` must stay inside one γ2 rounding bucket. Worked
|
||||
numerically (dkg v0.3.5): **admitted** n=8,t=7 (`τCη = 5 488`, 48× margin),
|
||||
n=8,t=8 (1 568), n=16,t=14 (109 760, 2.4× margin — tight but viable);
|
||||
**rejected** n=16,t=12 (856 128 > γ2, hint budget blown). The empirical
|
||||
reconstructed norms at n=16,t=14 are `‖s1‖∞, ‖s2‖∞ ≈ 185–230` — far below the
|
||||
worst-case `C·η = 2240` and far below γ2 = 261 888 (so the key is genuinely
|
||||
signable). `MaxParties = 6` is only the small-committee fast-path / iteration
|
||||
cap, **not** the admissible ceiling.
|
||||
|
||||
**The v0.6.3 overflow fix (why large committees were blocked).** Every `χ_η`
|
||||
coefficient is stored in pulsar's `[q−η, q+η]` representation (≈ q ≈ 2²³), and
|
||||
`poly.add` is a raw uint32 add. Summing all `C(N,M)` subset secrets without
|
||||
intermediate reduction overflows the accumulator once `C ≥ ⌊2³²/q⌋ = 512` —
|
||||
exactly the owner-default n=16,t=14 with `C(16,3) = 560` — wrapping the
|
||||
coefficient into an unsignable large-secret wall key. `accumulateSubset`
|
||||
(`mithril_rss.go:122`) reduces **mod q per subset**; because reduction mod q is
|
||||
an additive homomorphism, the result is the *identical* short `Σ_S` secret a
|
||||
single final reduction would give for a small committee (so n ≤ 8 is
|
||||
byte-unchanged), while every intermediate accumulator stays below 2q ≪ 2³².
|
||||
|
||||
**Signing the RSS key — two paths.**
|
||||
- *Quorum-reconstruct* (`MithrilKey.Sign`, `mithril_rss.go:266`): rebuilds the
|
||||
key material from any T parties' holdings (`ReconstructKeyMaterial`, `:223`,
|
||||
balanced partition `rss.RSSRecover`), BCC-signs, and **fail-closed
|
||||
self-verifies** under the FIPS-204 verifier before returning. This rebuilds
|
||||
the secret at the signing coordinator — fine for a single trusted signer, but
|
||||
it is *reconstruct-at-sign*.
|
||||
- *No-reconstruct* (`MithrilKey.SignHyperball`, §5): never rebuilds the key.
|
||||
|
||||
---
|
||||
|
||||
## 5. No-reconstruct hyperball signer — the Mithril 3-round protocol
|
||||
|
||||
`SignHyperball(active, message, ctx, rng, maxRounds)`
|
||||
(`mithril_rss_hyperball.go:780`) produces a byte-stock-FIPS-204 ML-DSA signature
|
||||
under the dealerless RSS group key from any T active parties **without ever
|
||||
reconstructing the key**. No party and no coordinator ever forms the full `s1`,
|
||||
any `s2`, `t0`, the mask `y`, the commitment `w`, `w0 = LowBits(w)`, or any `sk`.
|
||||
|
||||
**The kernel idea.** Each active party holds only its balanced-partition share
|
||||
`s1_(j)` (the sum of the subset secrets the partition assigns to it, taken from
|
||||
*this party's own holdings* — `partyShareS1`, `:870`, never summed across
|
||||
parties). The party emits only its partial response `z_j = y_j + c·s1_(j)`. The
|
||||
sum `z = Σ_j z_j = y + c·s1` is the standard FIPS-204 response; the hint is
|
||||
recovered from the **public** `w' = A·z − c·t1·2^d`. `s2` is never touched
|
||||
during signing.
|
||||
|
||||
**Three rounds** (`mithril_rss_hyperball.go`):
|
||||
1. **Commit** (`round1`, `:294`). Each party samples `K = kReps` ephemeral masks
|
||||
`y_{j,k}` uniformly inside a hyperball `B(0, r1)` (`sampleHyperballInBall`,
|
||||
`:895`), computes `w_{j,k} = A·y_{j,k}`, and broadcasts binding commitment
|
||||
hashes `CommitW` (and a blame-only `CommitT` to `T_j = A·s1_(j)`,
|
||||
`hyperballCommitT`, `:1019`).
|
||||
2. **Reveal + aggregate** (`round2` `:321`; coordinator `aggregateCommitments`
|
||||
`:430`). Parties reveal `w_{j,k}`; the coordinator verifies each against the
|
||||
Round-1 commitment (equivocation gate, `:466`), sums `w_k = Σ_j w_{j,k}`, and
|
||||
derives the challenge `c_k` for every **boundary-clear** slot (`BoundaryClear`,
|
||||
`boundary.go:103`). A non-clear slot gets `c = nil` (dead — no party responds,
|
||||
no secret consulted).
|
||||
3. **Respond** (`round3`, `:333`). For each live slot the party computes
|
||||
`z_{j,k} = y_{j,k} + c_k·s1_(j)` and applies a **leak-free Excess gate**
|
||||
(`hyperballExcess`, `:966`): if the continuous response leaves `B(0, r)` the
|
||||
partial is **rejected and never revealed**. The coordinator `finalize`
|
||||
(`:518`) requires every active party to have accepted a slot, sums
|
||||
`z_k = Σ_j z_{j,k}`, runs the FIPS-204 reject bound + `FindHint`
|
||||
(`boundary.go:154`) on the public `w'`, and emits `(c̃, z, h)`. A **mandatory
|
||||
fail-closed release gate** runs stock `VerifyCtx` before returning — a biased
|
||||
or malformed partial makes `w'` miss `w1`, so that slot is skipped, never a
|
||||
bad signature emitted.
|
||||
|
||||
**Why it is stock-verifiable (Claim A).** Verifiability is *independent of the
|
||||
hyperball parameters*: the produced `(c̃, z, h)` clears the FIPS-204 verifier iff
|
||||
the summed `z, w` clear the central BCC checks — identical to what `bccSign`
|
||||
checks on a single reconstructed key, only here `y` and `z` are formed
|
||||
additively. So the signature verifies byte-for-byte under unmodified
|
||||
`circl mldsa65.Verify`.
|
||||
|
||||
**Why the partials are leak-free (Claim B argument).** Conditioned on the Excess
|
||||
gate's acceptance, the revealed `z_j` is (almost) uniform on `B(0, r)`,
|
||||
independent of the secret shift `c·s1_(j)`; the residual dependence is bounded by
|
||||
Rényi divergence ≤ 1/(1 − 2⁻⁶⁴) per signature via the leak-free gap
|
||||
`Δ = r1 − r` (`deriveHyperballParams`, `:106`; κ = 64 conservative;
|
||||
`docs/hyperball-mldsa65-params.md`). The mask `y_j` is **never serialised** — the
|
||||
wire carries only `w_{j,k} = A·y_{j,k}` (recovering `y` is Module-SIS) and the
|
||||
public `z_{j,k}`.
|
||||
|
||||
**Gate evidence (proven today):**
|
||||
- **GATE 5(a)** — `TestHyperballStockCirclVerify` (`mithril_rss_hyperball_test.go:41`):
|
||||
the hyperball signature verifies under unmodified `circl mldsa65.Verify` for
|
||||
every committee N ≤ 6 and for n=8,t=8; tamper / wrong-message / wrong-context
|
||||
rejected (verifier non-vacuous).
|
||||
- **GATE 5(b)** — `TestHyperballNoReconstructStructural` (`:100`): a `go/ast` scan
|
||||
proves the signing path **never calls `ReconstructKeyMaterial`**; a source byte
|
||||
scan proves no secret share/mask is ever packed to the wire; a runtime
|
||||
transcript oracle proves no party's share `s1_(j)` nor the full reconstructed
|
||||
`s1`/`s2` bytes appear in `publicBytes()`; and no `(T−1)`-coalition even covers
|
||||
all subsets.
|
||||
- **GATE 6** — fail-closed: `TestHyperballSubThresholdFailsClosed` (`:298`,
|
||||
below-threshold/malformed active sets refused before signing),
|
||||
`TestHyperballBiasedPartialCaughtAndBlamed` (`:329`, the release gate rejects a
|
||||
biased partial and `blameSlot` pinpoints the culprit *without forming
|
||||
Σ_j T_j = t − s2* — leak-free blame), `TestHyperballEquivocationCaught` (`:404`,
|
||||
a rushing party that changes `w` between rounds is rejected by the binding
|
||||
check).
|
||||
- **Mask never on wire** — `TestHyperballMaskNeverOnWire` (`:529`, commit
|
||||
`0faa086`): no party's mask `y` (nor its share) bytes appear in the Round-2 /
|
||||
Round-3 wire data.
|
||||
|
||||
**Honest blame residual (`mithril_rss_hyperball.go:633`–`637`).** A party that
|
||||
uses a share inconsistent with keygen but self-consistent with its *own*
|
||||
(equivocated-at-keygen) `T_j` passes the per-party blame check; it is still
|
||||
caught by the fail-closed release gate (no bad signature ever emitted) but is not
|
||||
pinpointed there. This is the same identifiable-abort residual as the
|
||||
malicious-CSCP layer (§18) — flagged, not faked.
|
||||
|
||||
---
|
||||
|
||||
## 6. Parameter sets
|
||||
|
||||
Pulsar is defined for the BCC-proven scope only: **ML-DSA-65** and
|
||||
**ML-DSA-87**. ML-DSA-44 has **no** Pulsar suite.
|
||||
|
||||
Common FIPS-204 modulus `q = 8380417 = 2²³ − 2¹³ + 1`, ring
|
||||
`R_q = Z_q[X]/(X²⁵⁶ + 1)`, Power2Round `d = 13`.
|
||||
|
||||
| Symbol | ML-DSA-65 | ML-DSA-87 | Meaning |
|
||||
|---|---|---|---|
|
||||
| Category | NIST 3 (production target) | NIST 5 | |
|
||||
| `(K, L)` | `(6, 5)` | `(8, 7)` | matrix `A ∈ R_q^{K×L}` |
|
||||
| `η` | `4` | `2` | secret bound, `s1,s2 ∈ S_η` |
|
||||
| `τ` | `49` | `60` | challenge weight |
|
||||
| `β = τ·η` | `196` | `120` | key-shift bound `‖c·s2‖∞ ≤ β` |
|
||||
| `γ2` | `261888 = (q−1)/32` | `261888` | HighBits bucket half-width |
|
||||
| `ω` | `55` | `75` | hint weight bound |
|
||||
| `\|c̃\|` | `48 B` | `64 B` | challenge-hash length |
|
||||
|
||||
**BCC clearance** (`boundary.go`): a nonce is accepted only if its commitment
|
||||
clears a fixed boundary so `HighBits(w − c·s2) = HighBits(w)`; the hint is then
|
||||
**public-computable** and the key residual never appears in the transcript.
|
||||
|
||||
**Why ML-DSA-44 is excluded.** BCC requires `‖c·t0‖∞ ≤ τ·2^(d−1) < γ2`. For
|
||||
ML-DSA-44, `39·4096 = 159744 > γ2 = 95232` — the hint cannot be kept
|
||||
public-computable. `bccParams` returns `ok = false` (`boundary.go:40`,
|
||||
`:38`–`:39`); both the BCC signer and `deriveHyperballParams` (`ErrHyperballScope`,
|
||||
`mithril_rss_hyperball.go:72`) refuse ML-DSA-44.
|
||||
|
||||
---
|
||||
|
||||
## 7. Avalanche-native committee math — sample many, accumulate by repetition
|
||||
|
||||
This is the load-bearing scaling idea, and it is **not** "one big BFT committee."
|
||||
Lux consensus is Avalanche-family: safety on the chain itself comes from
|
||||
*repeated small-sample sub-sampling*. Pulsar mirrors that for the post-quantum
|
||||
*certificate*: **do not make one small committee the finality root — sample MANY
|
||||
small dealerless RSS committees over the same finalized digest and accumulate
|
||||
confidence by repetition.**
|
||||
|
||||
**Setup.** A permissionless validator set of `N ≥ 1000` with a Byzantine
|
||||
fraction `f ≤ 1/3`. Per epoch, sample `m` independent committees, each of size
|
||||
`n` with signing threshold `t`; require `r` of the `m` committees to produce a
|
||||
valid certificate over the same digest.
|
||||
|
||||
**One-committee capture probability.** A single committee of `n` stake-weighted
|
||||
members is *captured* (the adversary controls ≥ t of it, hence could forge that
|
||||
committee's leg) with probability
|
||||
```
|
||||
p = Pr[X ≥ t], X ~ Binomial(n, f).
|
||||
```
|
||||
|
||||
**r-of-m failure probability.** Treating committee captures as independent
|
||||
(unbiased sampling, §8), the certificate forges only if **at least r** of the
|
||||
`m` committees are captured:
|
||||
```
|
||||
P_fail ≈ Σ_{j ≥ r} C(m, j) · p^j · (1 − p)^{m − j} (exact binomial tail)
|
||||
```
|
||||
The special case `r = m` (require *all* sampled committees) collapses to
|
||||
`P_fail ≈ p^r`. The general `r`-of-`m` tail is what the default uses, because it
|
||||
tolerates up to `m − r` offline/stalled committees for liveness while keeping
|
||||
the forgery budget astronomically small.
|
||||
|
||||
**Default profile — `Pulsar-HYBRID-PQ-v1`: n = 8, t = 7, m = 12, r = 8.**
|
||||
- One-committee capture `p = Pr[X ≥ 7], X ~ Binomial(8, 1/3) = 17/6561 ≈ 2⁻⁸·⁶`.
|
||||
- 8-of-12 tail `P_fail ≈ 2⁻⁵⁹·⁸` (the dominant `j = 8` term
|
||||
`C(12,8)·p⁸·(1−p)⁴` dominates; computed with exact `math/big` on the consensus
|
||||
side).
|
||||
- This is **NOT** `n = 64 / t = 5` or any single large committee. Small, high
|
||||
threshold (t close to n) maximizes per-committee `p`-resistance; repetition
|
||||
(`r`-of-`m`) does the security amplification.
|
||||
|
||||
Why small-and-high-`t` committees, specifically: the dealerless RSS keygen is
|
||||
norm-viable exactly in the small/high-`t` regime (§4: n=8,t=7 has 48× margin;
|
||||
n=16,t=14 is 2.4×; n=16,t=12 is rejected). The Avalanche sampled-cert model wants
|
||||
exactly those committees — so the cryptographic feasibility envelope and the
|
||||
consensus security model **coincide**. We never need the research-open
|
||||
large-committee dealerless DKG, because we never use a large committee.
|
||||
|
||||
**`PulsarSampledCert` shape.** `r` standard ML-DSA signatures (one per
|
||||
contributing committee, each a `(c̃, z, h)` under that committee's RSS `GroupPK`),
|
||||
plus the committee plan binding (§8). Storage and verify cost are `O(r)`,
|
||||
independent of `N` — each leg is verified by an **unmodified** FIPS-204 verifier.
|
||||
|
||||
---
|
||||
|
||||
## 8. Unbiasable committee selection
|
||||
|
||||
The independence assumption behind §7's `P_fail` requires that the adversary
|
||||
**cannot grind committee membership**.
|
||||
|
||||
- **Stake-weighted VRF sortition.** Each committee's members are drawn by
|
||||
stake-weighted VRF from the snapshotted validator set, seeded by an
|
||||
**unbiasable** beacon.
|
||||
- **The seed is the previous *finalized* block**, not a proposer-chosen value —
|
||||
it is **not proposer-grindable**. An adversary cannot re-roll the sortition to
|
||||
land ≥ t members in a committee.
|
||||
- **`committeePlanHash` is bound into the Quasar subject `M`.** The full plan
|
||||
(epoch, the `m` committees' member sets, thresholds, the seed) is hashed and
|
||||
folded into the message the committees sign, so a certificate is valid only for
|
||||
the exact plan it was sampled under — a captured committee from one plan cannot
|
||||
be replayed into another.
|
||||
|
||||
This is what lets §7 treat the `m` committee captures as (near-)independent
|
||||
Bernoulli trials, and what makes the `r`-of-`m` tail meaningful rather than
|
||||
grindable down to one lucky committee.
|
||||
|
||||
---
|
||||
|
||||
## 9. Three finality tiers
|
||||
|
||||
Pulsar's sampled certificate is the **default PQ finality**, sitting between a
|
||||
fast classical path and a maximal large-quorum PQ root.
|
||||
|
||||
| Tier | Cert | Use | PQ posture |
|
||||
|---|---|---|---|
|
||||
| **FAST** | **Beam-only** (classical BLS/consensus finality) | low-latency, non-adversarial-PQ lanes | classical only |
|
||||
| **HYBRID_PQ** | **Beam + Pulsar sampled-cert** (§7 default `n=8,t=7,m=12,r=8`) | **default finality** | classical safety + compact PQ certs (`P_fail ≈ 2⁻⁵⁹·⁸`) |
|
||||
| **PQ_ROOT** | **P3Q large-quorum** — a ≥ ⅔-weighted ML-DSA quorum over the validator set | recovery / checkpoint / maximal-assurance root of trust | full PQ super-majority |
|
||||
|
||||
**Division of labour.** Avalanche sub-sampling carries *chain safety*; Pulsar
|
||||
produces *compact post-quantum certificates over consensus-finalized digests*.
|
||||
The sampled-cert tier (HYBRID_PQ) is not re-deriving consensus — it is attaching
|
||||
a small, independently-verifiable PQ proof to a digest consensus already
|
||||
finalized. PQ_ROOT (P3Q) is the heavyweight fallback when a maximal,
|
||||
non-sampled, super-majority PQ attestation is required.
|
||||
|
||||
---
|
||||
|
||||
## 10. System, adversary, and synchrony model
|
||||
|
||||
**Parties.** `N` permissionless validators (target `N > 1000`), each with stake
|
||||
and a registered long-term identity key; the epoch validator set is committed by
|
||||
`validator_set_root` (§11). Per epoch, `m` committees of size `n` are sampled by
|
||||
stake-weighted VRF (§8). A per-session **coordinator** is a committee member with
|
||||
**no special trust** — it routes/aggregates public data, and the fail-closed
|
||||
release gate makes coordinator misbehavior detectable (liveness-only).
|
||||
|
||||
**Adversary.** Byzantine, Module-LWE/Module-SIS-bounded, SHA3/SHAKE modeled as a
|
||||
RO for domain-separated input. Per committee, up to `t − 1` corruptions for
|
||||
unforgeability and `(t−1)`-privacy (the standard threshold bound). The *certificate*
|
||||
forgery budget is the `r`-of-`m` product across committees (§7), not a single
|
||||
committee. Static corruption is the submission posture. The hyperball signer's
|
||||
malicious-deviation containment is **fail-closed/liveness-only**: a biased
|
||||
partial cannot forge or leak (§5); identifiable-abort against an
|
||||
equivocated-at-keygen share is a labelled residual (§18).
|
||||
|
||||
**Synchrony.** *Keygen* (RSS) and *preprocessing*: partially synchronous with a
|
||||
bounded complaint/blame round. *Online signing*: 3 rounds (hyperball) or 1 round
|
||||
(BCC over an offline ticket) under partial synchrony; liveness is provided by
|
||||
sampling `m > r` committees so a stalled committee does not stall finality.
|
||||
*On-chain verification*: deterministic, no synchrony assumption.
|
||||
|
||||
---
|
||||
|
||||
## 11. Object model
|
||||
|
||||
All objects are content-addressed by a SHAKE256 hash over their canonical
|
||||
encoding with a domain tag (§14). On-chain we store **commitments**, not raw
|
||||
material.
|
||||
|
||||
### PulsarEpoch
|
||||
```
|
||||
epoch_id uint64 monotonic epoch counter
|
||||
validator_set_root [32]byte Merkle root over (validator_id, stake, ltk) leaves
|
||||
randomness_seed [32]byte UNBIASABLE beacon (prev finalized block) → committee sampling (§8)
|
||||
policy_id uint32 selects (n, t, m, r) profile + suite (§7, §9)
|
||||
activation_height uint64 first block at which this epoch's committees may sign
|
||||
expiry_height uint64 last block; certs under this epoch invalid after it
|
||||
```
|
||||
|
||||
### PulsarCommittee
|
||||
```
|
||||
epoch_id uint64
|
||||
committee_id uint32 index within the epoch (0..m-1)
|
||||
members []ValidatorID stake/VRF-sampled, size n
|
||||
stake_weights []uint64 aligned with members
|
||||
threshold_t uint16 RSS signing threshold (§4 viability bound)
|
||||
scheme uint8 ML-DSA-65 | ML-DSA-87
|
||||
group_public_key []byte FIPS-204 pk bytes — the RSS GroupPK a verifier uses
|
||||
keygen_root [32]byte commitment to the RSS keygen transcript (DKG-PROOF-BOUNDARY.md)
|
||||
status uint8 Proposed | Active | Expired | Slashed
|
||||
```
|
||||
|
||||
### PulsarSampledCert
|
||||
```
|
||||
epoch_id uint64
|
||||
policy_id uint32 the (n,t,m,r) profile (§7)
|
||||
message_kind uint16 finality | bridge | upgrade | warp | emergency
|
||||
message_digest [32]byte domain-separated digest the committees signed (§14)
|
||||
committee_plan_hash [32]byte bound into the signed digest (§8) — anti-grinding
|
||||
legs []Leg r entries, each { committee_id, signature (c̃,z,h), group_public_key_ref }
|
||||
```
|
||||
Each `Leg.signature` is a **standard FIPS-204** signature under that committee's
|
||||
RSS `GroupPK`. `O(r)` storage; `r` independent stock-verifier checks (§13).
|
||||
|
||||
---
|
||||
|
||||
## 12. Per-epoch lifecycle
|
||||
|
||||
1. **Epoch start** → snapshot the validator set; commit `validator_set_root`.
|
||||
2. **Beacon** → `randomness_seed` (prev finalized block, §8) seeds the
|
||||
stake-weighted VRF sortition of `m` committees.
|
||||
3. **Dealerless committee DKG** (off-chain / p2p) → each committee runs
|
||||
`MithrilRSSKeygen` (§4): **no dealer**, no party holds the full key, the
|
||||
public `GroupPK` is a genuine FIPS-204 key. The keygen transcript root is
|
||||
committed.
|
||||
4. **Commit** → the chain accepts each committee's `GroupPK` iff the keygen
|
||||
transcript is well-formed and the committee is admissible (§4 norm bound).
|
||||
Faulty members → blame set → slashing input.
|
||||
5. **Per certificate:** for a consensus-finalized digest, each sampled committee
|
||||
runs the **no-reconstruct** signer (hyperball, §5 — or the 1-round BCC signer
|
||||
over an offline ticket) and emits its leg; the chain assembles a
|
||||
`PulsarSampledCert` once `r` legs land.
|
||||
6. **Verify** (any relying party / chain) → §13.
|
||||
7. **Rotation** → at `expiry_height` the epoch's committees expire; membership
|
||||
changes take effect at the **next** epoch's fresh DKG (key expiry, not key
|
||||
mutation — a live committee key is never mutated per join/leave).
|
||||
|
||||
**Never all-N-sign.** A certificate is signed by `r` small committees of `n`
|
||||
members each, never by all `N` validators. Cost is `O(r·n)`, independent of `N`.
|
||||
|
||||
---
|
||||
|
||||
## 13. On-chain verification
|
||||
|
||||
Verification is **cheap and stateless w.r.t. DKG** — no threshold or DKG math
|
||||
runs per signature. Given a `PulsarSampledCert` and the on-chain committee
|
||||
registry, check, in order, fail-closed:
|
||||
|
||||
1. **Epoch active.** `epoch_id` resolves to an epoch whose
|
||||
`[activation_height, expiry_height]` brackets the current height, and whose
|
||||
`policy_id` admits `message_kind`.
|
||||
2. **Plan binding.** Recompute `committee_plan_hash` from the registered epoch
|
||||
sortition and confirm it equals the value bound into `message_digest` (§8).
|
||||
3. **Quorum of legs.** Exactly `r` distinct committees' legs are present, each
|
||||
resolving to an `Active` committee of this epoch.
|
||||
4. **Each leg: GroupPK matches registry** (`group_public_key_ref == hash(registry
|
||||
GroupPK)`), then **standard verify**:
|
||||
`MLDSA.Verify(GroupPK, message_digest, leg.signature)` with an **unmodified**
|
||||
FIPS-204 verifier (Claim A). This is the only crypto op, run `r` times.
|
||||
5. **Not replayed.** `(epoch_id, message_digest)` has not been accepted before.
|
||||
|
||||
The `r`-of-`m` policy (§7) is enforced by step 3 + the per-leg checks; the forgery
|
||||
budget is `P_fail` (§7). This is the **HYBRID_PQ** tier verifier; **PQ_ROOT** (P3Q)
|
||||
runs the analogous large-quorum check over a ≥ ⅔-weighted ML-DSA set.
|
||||
|
||||
---
|
||||
|
||||
## 14. Domain separation tags
|
||||
|
||||
All hashing uses SHAKE256 / cSHAKE256 (SP 800-185) with a version-pinned tag;
|
||||
one tag per purpose, never reused. The *implemented* DSTs (grounded in
|
||||
`transcript.go` and the RSS/hyperball files) include:
|
||||
|
||||
| Tag | Purpose | Site |
|
||||
|---|---|---|
|
||||
| `Pulsar` (cSHAKE function-name `N`) | all cSHAKE calls | `transcript.go:73` |
|
||||
| `PULSAR-DKG-COMMIT-V1` | seed-share DKG Round-2 digest + committeeRoot | `transcript.go:40` |
|
||||
| `PULSAR-SEED-SHARE-V1` | Shamir coeff stream + master-seed mix | `transcript.go:66` |
|
||||
| `pulsar.mithril.rss.rho.v1` | RSS joint public seed `rho` | `mithril_rss.go:101` |
|
||||
| `pulsar.mithril.rss.subset.v1` | RSS per-subset sampling seed | `mithril_rss.go:86` |
|
||||
| `pulsar.mithril.hyperball.nonce.v1` | hyperball per-round nonce seed | `mithril_rss_hyperball.go:993` |
|
||||
| `pulsar.mithril.hyperball.commitW.v1` | hyperball `w`-commitment binding | `mithril_rss_hyperball.go:1006` |
|
||||
| `pulsar.mithril.hyperball.commitT.v1` | hyperball `T_j` (blame-only) commitment | `mithril_rss_hyperball.go:1021` |
|
||||
| `pulsar.mithril.hyperball.sid.v1` | hyperball session id | `mithril_rss_hyperball.go:1032` |
|
||||
| `PULSAR/nonce-single-use/v1` | nonce dedup key (`w1` alone) | `nonce_ledger.go:395` |
|
||||
| `PULSAR-BCC-CEF/joint-pk-id/v1` | stable group-PK id | `distributed_bcc.go` |
|
||||
| `PULSAR/protocol-msg/v1` | authenticated-protocol-message TBS | `protocol_auth.go:61` |
|
||||
|
||||
The certificate-layer namespace (`pulsar:v1:<kind>` for `message_digest`) is the
|
||||
*consensus target* binding `epoch / committee-plan / policy / chain_id /
|
||||
message_kind` (§8, §13); it is kept distinct from the implemented kernel DSTs
|
||||
above on purpose.
|
||||
|
||||
---
|
||||
|
||||
## 15. Abort, blame, and slashing
|
||||
|
||||
- **DKG abort.** A member that fails to deliver/open a subset secret, or
|
||||
equivocates, is placed in the blame set; the committee re-runs without it (if
|
||||
`n − |blame| ≥ t`) or the epoch resamples. Blame is on-chain → slashing input.
|
||||
- **Signing abort (liveness, not safety).** A biased `z_j` or a bad aggregate is
|
||||
caught by the **mandatory fail-closed release gate** (`finalize` runs stock
|
||||
FIPS-204 verify before emit, `mithril_rss_hyperball.go:610`–`616`; the BCC path's
|
||||
`TalusReleaseGate`): the slot is skipped/aborted. A deviating party is bounded
|
||||
to **liveness** — never a forgery or leak. `blameSlot` (`:638`) attributes the
|
||||
culprit leak-free (never forming `Σ_j T_j = t − s2`).
|
||||
- **Nonce-reuse.** The hyperball protocol derives fresh per-round nonces (`round1`
|
||||
is keyed on fresh round entropy); `TestHyperballNonceReuseFatal` (`:419`)
|
||||
demonstrates why reuse would be catastrophic (`z1 − z2 = (c1 − c2)·s1_(j)`
|
||||
recovers the share) and that the derivation prevents it. The BCC path enforces
|
||||
`w1`-keyed single-use (`ErrNonceReused`, `nonce_ledger.go:80`).
|
||||
|
||||
---
|
||||
|
||||
## 16. Build note — packaging & shared base
|
||||
|
||||
Pulsar's lattice primitives are routed onto **`github.com/luxfi/mlwe`** (v0.6.1 /
|
||||
v0.6.2): transcript → `mlwe/transcript`, Shamir → `mlwe/share`, SHAKE samplers →
|
||||
`mlwe/sample/shake`, ML-DSA ring core → `mlwe/ring/mldsa`, all byte-preserving.
|
||||
The dealerless committee combinatorics (subset enumeration, the `(n,t)` viability
|
||||
bound, the balanced reconstruction partition) come from
|
||||
**`github.com/luxfi/dkg/rss`**. Pulsar and Corona share the one Module-LWE base,
|
||||
so a change to the shared arithmetic is made in one place — and the two **legs of
|
||||
the Quasar dual-PQ cert build and version independently** (a Module-LWE issue in
|
||||
one must not block the other).
|
||||
|
||||
---
|
||||
|
||||
## 17. Security summary
|
||||
|
||||
- **(A) Verification compatibility — PROVEN today.** The no-reconstruct BCC/CEF
|
||||
signer (`bcc_sign_test.go:86`), the dealerless RSS key
|
||||
(`mithril_rss_test.go:38`, `mithril_rss_n8_test.go:16`), and the no-reconstruct
|
||||
hyperball signer (`mithril_rss_hyperball_test.go:41`) all produce `(c̃, z, h)`
|
||||
accepted by **unmodified** `circl mldsa{65,87}.Verify`, with
|
||||
tamper/wrong-message/wrong-context negatives.
|
||||
- **(B) Construction — Lux-authored, partly residual.** Dealerless RSS keygen
|
||||
(no dealer, no party holds the whole key) + no-reconstruct signing (BCC/CSCP +
|
||||
hyperball) reduce to ML-DSA EUF-CMA under Module-LWE / Module-SIS for the
|
||||
*output bytes*. The **scoped residuals** (§18) are the full FIPS-204
|
||||
KeyGen-distribution-equivalence proof and the malicious-secure
|
||||
CSCP/identifiable-abort layer.
|
||||
- **Certificate-level safety — sampling, not one committee.** A `PulsarSampledCert`
|
||||
forges only if `r` of `m` independent, unbiasably-sampled committees are
|
||||
captured: `P_fail ≈ 2⁻⁵⁹·⁸` for the default `n=8,t=7,m=12,r=8` (§7).
|
||||
- **Dual-PQ defence in depth.** Pulsar is the FIPS-204-standard, Module-LWE leg of
|
||||
the Quasar AND-mode dual-PQ cert; **Corona** (natively dealerless Module-LWE
|
||||
Raccoon/Ringtail line — a *non*-FIPS verifier) is the assumption-diverse
|
||||
companion leg. A forgery requires breaking both legs.
|
||||
|
||||
---
|
||||
|
||||
## 18. Residuals (labelled, fail-closed, never silently weakened)
|
||||
|
||||
| # | Residual | Status |
|
||||
|---|---|---|
|
||||
| **R1** | **Full FIPS-204 KeyGen-distribution-equivalence** for the dealerless RSS keygen — that `GroupPK` is distributed identically to a single honest `KeyGen`, with (i) an unbiased composite secret, (ii) hiding against `< t` corruptions, (iii) abort-bias resistance. Standard-verifier compatibility (A) is **proven**; this distributional (B) equivalence needs a simulation/hiding/abort-bias proof. | **open-research** (Claim B). The structural facts (no party holds the key, `‖s2‖∞ ≤ C·η`, stock-circl-verifiable) are proven; the distributional proof is not. |
|
||||
| **R2** | **Malicious-secure CSCP + identifiable-abort.** A valid-sigma but wrong-`z` partial (BCC), or an equivocated-at-keygen share (hyperball `blameSlot`), is bounded to a **liveness fault** (never forgery/leak — the release gate catches it) but is **not yet attributed**. Needs BDLOP/Ajtai hiding share-commitments + an extended linear-sigma. | **fail-closed-pending-review** (`share_commit.go:73` `ErrIdentifiableAbortResidual`; `mithril_rss_hyperball.go:633`). |
|
||||
| **R3** | **Leak-free distributed NonceMPC** (BCC offline ticket factory). The production sign path consumes a `NonceCert` (only `w1` public); the stand-in dealer-models the nonce and exposes `DebugW` to tests only (PULSAR-V13-W-LEAK). | **fail-closed-pending-review.** The hyperball signer does **not** use this path (it forms `w` additively from per-party commitments, no nonce dealer). |
|
||||
| **R4** | **Networked, non-simulation MPC + persistent (crash-restart) nonce ledger.** The crypto binding is in place; the authenticated transport and a restart-surviving per-share ledger are consensus-layer residuals. | **flagged.** |
|
||||
|
||||
**Never claimed.** FIPS/NIST-certified threshold ML-DSA · fully-malicious-secure-
|
||||
*proven* (mechanized) · global-1000-validator DKG. (RSS keygen is per-committee
|
||||
and small; the global scale is achieved by *sampling* small committees, §7.)
|
||||
|
||||
---
|
||||
|
||||
## 19. References
|
||||
|
||||
- **TALUS** — J. Kao, "TALUS: Threshold ML-DSA with One-Round Online Signing via
|
||||
Boundary Clearance and Carry Elimination," `arXiv:2603.22109`. *(BCC = Boundary
|
||||
Clearance Condition; CEF = Carry Elimination Framework; reduces to ML-DSA
|
||||
EUF-CMA; offline ticket factory + one-round online signing.)*
|
||||
- **Mithril** — Celi, del Pino, Espitau, Niot, Prest, "Mithril: Threshold ML-DSA
|
||||
from Short Replicated Secret Sharing," `ia.cr/2026/013`, USENIX Security 2026.
|
||||
*(Short replicated sharing — the dealerless RSS keygen; the 3-round hyperball
|
||||
no-reconstruct signer; standard-verifier-compatible; practical for small,
|
||||
high-threshold committees.)*
|
||||
- **Threshold Raccoon** — del Pino, Katsumata, Prest, Rossi, EUROCRYPT 2024.
|
||||
*(Noise-flooded lattice signatures — a non-FIPS verifier; the Corona/Raccoon
|
||||
line, why Corona is the assumption-diverse dealerless leg.)*
|
||||
- **Corona** — Boschini et al., Module-LWE threshold signatures (`luxfi/corona`),
|
||||
the dealerless companion leg of the dual-PQ Quasar cert.
|
||||
- **Avalanche** — Team Rocket, "Scalable and Probabilistic Leaderless BFT
|
||||
Consensus through Metastability." *(The repeated-small-sample sub-sampling whose
|
||||
`Pr[capture]^r`-style amplification the sampled-cert model mirrors for PQ
|
||||
certificates.)*
|
||||
- **FIPS 204** — NIST, Module-Lattice-Based Digital Signature Standard (ML-DSA).
|
||||
*(The single-party standard whose **verifier** accepts Pulsar output — Claim A.
|
||||
NIST does not standardize threshold ML-DSA.)*
|
||||
|
||||
### Companion artifacts
|
||||
- DKG/threshold proof boundary: `DKG-PROOF-BOUNDARY.md` +
|
||||
`vectors/dkg-proof-boundary.json`.
|
||||
- Assurance vocabulary / gate-read: `PROOF-CLAIMS.md`; track ledger:
|
||||
`ref/go/pkg/pulsar/VERSIONS.md`; open findings: `BLOCKERS.md`.
|
||||
- Algorithm-level spec: `spec/pulsar.tex`, `spec/parameters.tex`,
|
||||
`spec/system-model.tex`, `spec/security-games.tex`.
|
||||
- Proofs: `~/work/lux/proofs/pulsar/` (LaTeX) + `~/work/lux/proofs/lean/Crypto/Pulsar/`.
|
||||
- Reference implementation: `ref/go/pkg/pulsar/` (BCC/CEF kernel, TALUS, the
|
||||
dealerless RSS keygen `mithril_rss.go`, the hyperball signer
|
||||
`mithril_rss_hyperball.go`, the computed naive-additive obstruction).
|
||||
@@ -0,0 +1,248 @@
|
||||
{
|
||||
"schema": "pulsar.dkg-proof-boundary.v1",
|
||||
"description": "Structured DKG + threshold-signing behavioral vectors for the Pulsar proof boundary. Spec-level state vectors (positive + negative), each grounded in the exact v0.6.3 code constant that enforces it. Distinct from the byte-level wire KATs under vectors/{keygen,sign,verify,threshold-sign,dkg}.json (see cross_version_kats).",
|
||||
"grounded_in": {
|
||||
"tag": "v0.6.3",
|
||||
"commit": "0650729",
|
||||
"tree": "ref/go/pkg/pulsar/",
|
||||
"deps": {"luxfi/dkg": "v0.3.5", "luxfi/mlwe": "v0.2.0", "luxfi/lattice/v7": "v7.1.4"},
|
||||
"companion_docs": ["DKG-PROOF-BOUNDARY.md", "PROOF-CLAIMS.md", "VERSIONS.md", "BLOCKERS.md", "PULSAR.md"]
|
||||
},
|
||||
"claim_discipline": {
|
||||
"A_verifier_compat": "PROVEN: threshold (c-tilde,z,h) is byte-FIPS-204; unmodified circl mldsa{65,87}.Verify accepts. Proven in three settings: no-reconstruct BCC (bcc_sign_test.go:86), DEALERLESS RSS key (mithril_rss_test.go:38 all N<=6; mithril_rss_n8_test.go:16 T==N at n=8,n=16), and NO-RECONSTRUCT HYPERBALL over the RSS key (mithril_rss_hyperball_test.go:41). interop-tested.",
|
||||
"B_construction": "SCOPED (Lux-authored). Dealerless committee keygen (RSS/Mithril) + no-reconstruct signing (BCC/CSCP + Mithril hyperball) + standard-ML-DSA-verifier output, malicious-hardened; the full FIPS-204 KeyGen-distribution-equivalence proof and the malicious-secure CSCP/identifiable-abort layer are labelled residuals.",
|
||||
"never_claim": ["FIPS/NIST-certified threshold ML-DSA", "fully-malicious-secure-proven (mechanized)", "global-1000-validator DKG"],
|
||||
"keygen_residual": "v0.6 CLOSES the dealerless-keygen gap for Claim (A): MithrilRSSKeygen (mithril_rss.go:133) is DEALERLESS (no dealer; no party holds the whole (s1,s2); s2 stays small as ||s2||inf <= C(N,N-T+1)*eta), and its threshold signatures verify under stock circl (mithril_rss_test.go:70, mithril_rss_n8_test.go:40). The v0.6.3 accumulateSubset (mithril_rss.go:122) per-subset mod-q reduction fixes a uint32 overflow that wrapped the key once C>=512, unblocking large committees (e.g. n=16,t=14, C(16,3)=560). The naive-additive byte-FIPS DKG stays correctly fail-closed (ErrDealerlessByteFIPSUnreachable) — RSS is its named escape, not a weakening. WHAT REMAINS RESIDUAL: full FIPS-204 KeyGen-distribution-equivalence (unbiased composite secret, hiding vs <t, abort-bias) is open-research — structural facts + stock-circl-verifiability are proven, the distributional equivalence is not. SIGNING is no-reconstruct (BCC/CSCP and hyperball) + malicious-hardened; permissionless dealerless safety is additionally carried by the Corona leg."
|
||||
},
|
||||
"complaint_kinds": {
|
||||
"ComplaintEquivocation": {"value": 1, "site": "types.go:285"},
|
||||
"ComplaintBadDelivery": {"value": 2, "site": "types.go:290"},
|
||||
"ComplaintBadPartial": {"value": 5, "site": "types.go:307"}
|
||||
},
|
||||
"positive_vectors": [
|
||||
{
|
||||
"id": "keygen/rss-dealerless-stock-circl",
|
||||
"layer": "keygen",
|
||||
"scenario": "Run the DEALERLESS Mithril RSS DKG (no trusted dealer) for every viable committee, reconstruct from a T-quorum, BCC-sign, and verify under unmodified circl mldsa65.Verify.",
|
||||
"expected": "accept",
|
||||
"invariant": "mldsa65.Verify(rss.pub, msg, ctx, sig)==true for all 15 committees 2<=T<=N<=6 and for T==N at n=8,n=16; tamper/wrong-message rejected",
|
||||
"code_ref": "mithril_rss.go:133 (MithrilRSSKeygen), :223 (ReconstructKeyMaterial), :122 (accumulateSubset overflow fix)",
|
||||
"test_ref": "TestMithrilRSSStockCirclVerify mithril_rss_test.go:38 (circl verify :70); TestMithrilRSS_LargeN_StockCircl mithril_rss_n8_test.go:16 (:40)",
|
||||
"property": "claim-A verifier-compatibility (the gold proof of dealerless stock-FIPS-204 signability)"
|
||||
},
|
||||
{
|
||||
"id": "keygen/rss-dealerless-structural",
|
||||
"layer": "keygen",
|
||||
"scenario": "For the whole viability range, assert no single party holds all subsets and no (T-1)-coalition covers all subsets.",
|
||||
"expected": "accept",
|
||||
"invariant": "for all id: |holdings[id]| < C(N,N-T+1); for all (T-1)-coalitions: covered != full",
|
||||
"code_ref": "mithril_rss.go:72 (Holdings), :169-182 (per-subset leader sampling + replication)",
|
||||
"test_ref": "TestMithrilRSSDealerless mithril_rss_test.go:91",
|
||||
"property": "claim-B dealerless guarantee (structural)"
|
||||
},
|
||||
{
|
||||
"id": "sign/hyperball-no-reconstruct",
|
||||
"layer": "sign",
|
||||
"scenario": "Sign the dealerless RSS key via the Mithril 3-round HYPERBALL protocol; NO party or coordinator forms the full s1/s2/y/w0/sk; the signing path never calls ReconstructKeyMaterial.",
|
||||
"expected": "accept",
|
||||
"invariant": "mldsa65.Verify accepts; AST scan finds no ReconstructKeyMaterial call; public transcript contains no share s1_(j) nor full s1/s2; mask y never on the wire",
|
||||
"code_ref": "mithril_rss_hyperball.go:780 (SignHyperball), :261 (newHyperballParty no-reconstruct boundary), :870 (partyShareS1 never sums across parties), :518 (finalize fail-closed VerifyCtx :613)",
|
||||
"test_ref": "TestHyperballStockCirclVerify mithril_rss_hyperball_test.go:41; TestHyperballNoReconstructStructural :100 (AST :109, transcript oracle :149); TestHyperballMaskNeverOnWire :529",
|
||||
"property": "claim-A verifier-compatibility; claim-B secrecy/no-reconstruct over the dealerless key"
|
||||
},
|
||||
{
|
||||
"id": "sign/circl-roundtrip",
|
||||
"layer": "sign",
|
||||
"scenario": "No-reconstruct BCC/CEF threshold signature (single group key) verified under an independent circl public key re-derived from the seed (no pulsar code in the verify path).",
|
||||
"expected": "accept",
|
||||
"invariant": "mldsa65.Verify(pk, msg, ctx, sig)==true; transcript carries no leaking secret",
|
||||
"code_ref": "distributed_bcc.go:875 (AggregateBCCWithBlame); :645 (partial z_i = lambda_i*y_i + c*lambda_i*s1_i)",
|
||||
"test_ref": "TestBCCSignRoundTripVerifiesCIRCL bcc_sign_test.go:86; assertBCCTranscriptNoLeak bcc_sign_test.go:217",
|
||||
"property": "claim-A verifier-compatibility; secrecy/no-reconstruct"
|
||||
},
|
||||
{
|
||||
"id": "dkg/seed-equivalence",
|
||||
"layer": "dkg",
|
||||
"scenario": "Legacy seed-share lineage: reconstruct the master seed from a threshold share set, recompute KeyFromSeed(masterSeed), compare to the DKG GroupPubkey; then sign and FIPS-204-verify.",
|
||||
"expected": "accept",
|
||||
"invariant": "GroupPK == KeyFromSeed(masterSeed).Pub AND Verify(GroupPK, msg, sig)==ok",
|
||||
"code_ref": "dkg.go:423-426 (masterSeed=cSHAKE256(byteSum||committeeRoot,'PULSAR-SEED-SHARE-V1'); sk=KeyFromSeed)",
|
||||
"test_ref": "TestDKG_ProducesValidPubkey_VerifiableSign dkg_test.go:147 (equal at :206)",
|
||||
"property": "correctness of the legacy seed-share map (structural seed-equivalence; NOT KeyGen-distribution-equivalence; superseded by RSS for the dealerless claim)"
|
||||
}
|
||||
],
|
||||
"negative_vectors": [
|
||||
{
|
||||
"id": "keygen/rss-bad-committee",
|
||||
"layer": "keygen",
|
||||
"scenario": "Attempt RSS keygen for a non-viable committee: structurally invalid (T<2 or T>N) or norm-blown (tau*C(N,N-T+1)*eta >= gamma2, e.g. n=16,t=12).",
|
||||
"expected": "reject (fail-closed)",
|
||||
"expected_outcome": "rss.ValidateCommittee error (ErrCommittee) — never a wall key",
|
||||
"code_ref": "mithril_rss.go:134 (ValidateCommittee gate); rss.ValidateCommittee per-(N,T) norm bound",
|
||||
"test_ref": "TestMithrilRSSRejectsBadCommittee mithril_rss_test.go:177 ({1,2},{3,2},{12,16})",
|
||||
"property": "keygen viability (per-(N,T) norm bound; admits n=8,t=7 48x margin and n=16,t=14 2.4x; rejects n=16,t=12)"
|
||||
},
|
||||
{
|
||||
"id": "sign/hyperball-sub-threshold",
|
||||
"layer": "sign",
|
||||
"scenario": "Hyperball sign with a below/above-threshold or malformed active set (too few, too many, unsorted, duplicate, out-of-range id).",
|
||||
"expected": "reject (fail-closed, before any signing)",
|
||||
"expected_outcome": "ErrHyperballActive (nil signature)",
|
||||
"code_ref": "mithril_rss_hyperball.go:1054 (validateActive), :87 (ErrHyperballActive)",
|
||||
"test_ref": "TestHyperballSubThresholdFailsClosed mithril_rss_hyperball_test.go:298",
|
||||
"property": "robustness (threshold-distinctness, fail-closed)"
|
||||
},
|
||||
{
|
||||
"id": "sign/hyperball-biased-partial",
|
||||
"layer": "sign",
|
||||
"scenario": "A malicious member biases its partial z_{j,k} on every accepted slot (keeps Accepted=true to look live).",
|
||||
"expected": "reject (no signature) + blame",
|
||||
"expected_outcome": "no slot yields a stock-verifiable signature (FindHint + fail-closed VerifyCtx release gate); blameSlot pinpoints the culprit WITHOUT forming Sum_j T_j = t - s2 (leak-free)",
|
||||
"code_ref": "mithril_rss_hyperball.go:518 (finalize release gate), :638 (blameSlot leak-free), :633-637 (documented attribution residual)",
|
||||
"test_ref": "TestHyperballBiasedPartialCaughtAndBlamed mithril_rss_hyperball_test.go:329",
|
||||
"property": "robustness (fail-closed release gate + leak-free identifiable abort)"
|
||||
},
|
||||
{
|
||||
"id": "sign/hyperball-equivocation",
|
||||
"layer": "sign",
|
||||
"scenario": "A rushing party reveals a DIFFERENT w for a slot in Round 2 than it committed in Round 1.",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "aggregateCommitments returns a w-commitment mismatch (equivocation) error",
|
||||
"code_ref": "mithril_rss_hyperball.go:466 (binding check: revealed w must match CommitW)",
|
||||
"test_ref": "TestHyperballEquivocationCaught mithril_rss_hyperball_test.go:404",
|
||||
"property": "binding (anti-equivocation)"
|
||||
},
|
||||
{
|
||||
"id": "sign/hyperball-mask-on-wire",
|
||||
"layer": "sign",
|
||||
"scenario": "Assert the secret mask y_j (and the share s1_(j)) bytes never appear in the Round-2/Round-3 wire data.",
|
||||
"expected": "reject (leak would fail the assertion)",
|
||||
"expected_outcome": "wire carries only w_{j,k}=A*y_{j,k} (recovering y is Module-SIS) and the public z_{j,k}; no mask, no share",
|
||||
"code_ref": "mithril_rss_hyperball.go:732 (publicBytes), :214 (HyperballRound2 W), :222 (HyperballRound3 Z)",
|
||||
"test_ref": "TestHyperballMaskNeverOnWire mithril_rss_hyperball_test.go:529 (commit 0faa086)",
|
||||
"property": "secrecy (mask never serialised)"
|
||||
},
|
||||
{
|
||||
"id": "sign/nonce-reuse",
|
||||
"layer": "sign",
|
||||
"scenario": "BCC path: the same joint nonce (same w1) is consumed for a second partial, even relabeled under a fresh nonceID or across two committees sharing the victim.",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "ErrNonceReused (no second z-partial emitted; (c_A-c_B)*s1 system never assembled)",
|
||||
"code_ref": "nonce_ledger.go:80 (ErrNonceReused), nonceMaterialKey nonce_ledger.go:393-401",
|
||||
"test_ref": "TestRED_NonceReuse_RecoversS1, TestRED_PoC_DefaultLedger_NonceReuse_Refused, TestRED_LOW_CrossCommittee_SameNonce_Deduped (VERSIONS.md); hyperball analogue TestHyperballNonceReuseFatal mithril_rss_hyperball_test.go:419",
|
||||
"property": "unforgeability (nonce single-use)"
|
||||
},
|
||||
{
|
||||
"id": "sign/session-mismatch",
|
||||
"layer": "sign",
|
||||
"scenario": "A partial's SessionID/NonceID does not match the round.",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "PartialBlame{Reason: BlameSessionMismatch}",
|
||||
"code_ref": "blame.go:38; AggregateBCCWithBlame distributed_bcc.go:875",
|
||||
"property": "robustness (identifiable abort)"
|
||||
},
|
||||
{
|
||||
"id": "sign/duplicate-partyid",
|
||||
"layer": "sign",
|
||||
"scenario": "A second partial carrying an already-seen PartyID (sub-threshold-via-duplicates vector).",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "PartialBlame{Reason: BlameDuplicatePartyID}",
|
||||
"code_ref": "blame.go:34; distributed_bcc.go:875",
|
||||
"property": "robustness (threshold-distinctness)"
|
||||
},
|
||||
{
|
||||
"id": "sign/unknown-party",
|
||||
"layer": "sign",
|
||||
"scenario": "A partial's PartyID is outside the signing quorum's eval-point range.",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "PartialBlame{Reason: BlameUnknownParty}",
|
||||
"code_ref": "blame.go:36; distributed_bcc.go:875",
|
||||
"property": "robustness (identifiable abort)"
|
||||
},
|
||||
{
|
||||
"id": "sign/malformed-partial",
|
||||
"layer": "sign",
|
||||
"scenario": "A partial's ZShare/Proof does not parse for the mode (unpackPolyVecChecked fails, no panic).",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "PartialBlame{Reason: BlameMalformed}",
|
||||
"code_ref": "blame.go:32; distributed_bcc.go:875",
|
||||
"property": "robustness (identifiable abort)"
|
||||
},
|
||||
{
|
||||
"id": "sign/invalid-proof",
|
||||
"layer": "sign",
|
||||
"scenario": "A partial's linear-sigma proof fails verification (bound to session,nonce,party,c,lambda).",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "PartialBlame{Reason: BlameProofInvalid}",
|
||||
"code_ref": "blame.go:40; AggregateBCCWithBlame distributed_bcc.go:875",
|
||||
"property": "robustness (identifiable abort)"
|
||||
},
|
||||
{
|
||||
"id": "sign/forged-victim-slot",
|
||||
"layer": "sign",
|
||||
"scenario": "An attacker stamps a victim's PartyID on a forged partial to get the victim blamed or front-run-excluded.",
|
||||
"expected": "reject",
|
||||
"expected_outcome": "dropped pre-attribution; NO blame against the slot's honest owner; nil verifier itself REFUSED fail-closed (ErrOriginAuthRequired)",
|
||||
"code_ref": "distributed_bcc.go:883 (auth gate before attribution); ErrOriginAuthRequired :813; UnauthenticatedAggregation opt-out :836",
|
||||
"test_ref": "TestRED_PoC_MEDIUM_CannotFrameOrExcludeHonestVictim (VERSIONS.md)",
|
||||
"property": "robustness (authenticated origin, safe-by-default)"
|
||||
},
|
||||
{
|
||||
"id": "sign/valid-sigma-wrong-z",
|
||||
"layer": "sign",
|
||||
"scenario": "A malicious member submits a VALID-sigma but WRONG-z partial (BCC), or an equivocated-at-keygen-but-self-consistent share (hyperball).",
|
||||
"expected": "liveness-fault (NOT yet attributable)",
|
||||
"expected_outcome": "wrong aggregate fails FIPS-204 verify (no forgery, no leak); attribution requires BDLOP dealt-share binding -> ErrIdentifiableAbortResidual",
|
||||
"code_ref": "share_commit.go:73 (ErrIdentifiableAbortResidual); shareCommitmentsFor returns nil today share_commit.go:94-96; hyperball analogue mithril_rss_hyperball.go:633-637",
|
||||
"property": "robustness residual (BDLOP plug point) — flagged honestly, fail-closed-pending-review"
|
||||
},
|
||||
{
|
||||
"id": "keygen/naive-additive-byte-fips",
|
||||
"layer": "keygen",
|
||||
"scenario": "Attempt a naive additive (Pedersen/Gennaro) dealerless byte-FIPS-204 ML-DSA DKG for any committee of parties>=2 (the additive lift, NOT RSS).",
|
||||
"expected": "reject (fail-closed, never fakes a key, never silently falls back to dealer/TEE)",
|
||||
"expected_outcome": "ErrDealerlessByteFIPSUnreachable; computed obstruction JointS2Linf=N*eta, JointCS2Linf=N*beta > beta",
|
||||
"code_ref": "naive_additive_seta_obstruction.go:152 (err), :196 (assessDealerlessFIPS), :242 (DealerlessMLDSADKG)",
|
||||
"property": "keygen obstruction (parameter-derived; RSS ia.cr/2026/013 is the NAMED ESCAPE — small s2=Sum chi_eta, not an N-way additive blow-up; Corona additionally carries dealerless safety)"
|
||||
}
|
||||
],
|
||||
"cross_version_kats": {
|
||||
"note": "Committed wire KATs replayed every CI run; drift from runtime output is a gate failure. These prove OLD WIRE COMPATIBILITY across versions. The v0.6.1/v0.6.2 mlwe de-dup (transcript/Shamir/SHAKE-samplers/ring routed onto luxfi/mlwe) was BYTE-PRESERVING — these KATs replay identically after the refactor.",
|
||||
"runner": "ref/go/pkg/pulsar/kat_test.go",
|
||||
"files": [
|
||||
{"file": "vectors/keygen.json", "entries": 9, "pins": "seed -> public_key, private_key", "test": "TestKAT_Keygen_Replay kat_test.go:50", "claim": "A"},
|
||||
{"file": "vectors/sign.json", "entries": 9, "pins": "seed,message,context -> signature", "test": "TestKAT_Sign_Replay kat_test.go:91", "claim": "A"},
|
||||
{"file": "vectors/verify.json", "entries": 6, "pins": "public_key,message,signature -> accept", "test": "TestKAT_Verify_Replay kat_test.go:127", "claim": "A"},
|
||||
{"file": "vectors/threshold-sign.json", "entries": 4, "pins": "n,t,message,public_key -> signature (Class N1 interchangeability)", "test": "TestKAT_ThresholdSign_Replay kat_test.go:159", "claim": "A"},
|
||||
{"file": "vectors/dkg.json", "entries": 3, "pins": "DKG replay", "test": "TestKAT_DKG_Replay kat_test.go:197", "claim": "B"}
|
||||
],
|
||||
"cross_implementation": {
|
||||
"test": "TestDKGVSS_RingMLDSA65_ExpandABinding_KAT dkg_vss_kat_test.go:104",
|
||||
"proves": "shared luxfi/dkg ring reproduces pulsar's FIPS-204 t1 byte-identical to circl; A-matrix round-trips with no spurious Montgomery factor",
|
||||
"honest_note": "the vss no-reconstruct group key T=A*s1+B*u (large s2=B*u) is NOT directly BCC-signable (dkg_vss_kat_test.go:30-35) — which is exactly why RSS (small s2=Sum chi_eta), not vss, is the dealerless keygen that beats the wall"
|
||||
}
|
||||
},
|
||||
"proof_checklist_summary": {
|
||||
"note": "Full 18-row table in DKG-PROOF-BOUNDARY.md §7. Assurance tags per PROOF-CLAIMS.md vocabulary.",
|
||||
"rows": [
|
||||
{"property": "verifier-compat/no-reconstruct-BCC", "test": "bcc_sign_test.go:86", "claim": "A", "assurance": "interop-tested"},
|
||||
{"property": "verifier-compat/dealerless-RSS-key", "test": "mithril_rss_test.go:38; mithril_rss_n8_test.go:16", "claim": "A", "assurance": "interop-tested"},
|
||||
{"property": "verifier-compat/no-reconstruct-hyperball", "test": "mithril_rss_hyperball_test.go:41", "claim": "A", "assurance": "interop-tested"},
|
||||
{"property": "dealerless-keygen-structural", "test": "mithril_rss_test.go:91", "claim": "B", "assurance": "test-proven"},
|
||||
{"property": "secrecy/no-reconstruct-hyperball", "test": "mithril_rss_hyperball_test.go:100; :529", "claim": "B", "assurance": "test-proven (AST+transcript oracle)"},
|
||||
{"property": "secrecy/no-reconstruct-BCC", "test": "bcc_sign_test.go:217; gate2_reachability_test.go; Lean NoLeakAggregate", "claim": "B", "assurance": "machine-checked(core)+test-proven; reduction sound-by-reduction (M-LWE/M-SIS)"},
|
||||
{"property": "any-quorum-consistency", "test": "mithril_rss_test.go:122", "claim": "B", "assurance": "test-proven"},
|
||||
{"property": "binding/domain-separation", "test": "transcript.go:40-66 + RSS/hyperball prefixes + KAT-pinned", "claim": "B", "assurance": "test-proven"},
|
||||
{"property": "binding/equivocation", "test": "mithril_rss_hyperball_test.go:404; protocol_auth.go:101; dkg_test.go:111", "claim": "B", "assurance": "test-proven"},
|
||||
{"property": "robustness/identifiable-abort+fail-closed", "test": "mithril_rss_hyperball_test.go:298,:329; distributed_bcc.go:875; blame_gate_test.go", "claim": "B", "assurance": "test-proven (semi-honest)"},
|
||||
{"property": "robustness/valid-sigma-wrong-z+equivocated-keygen-share", "test": "share_commit.go:73; mithril_rss_hyperball.go:633", "claim": "B", "assurance": "fail-closed-pending-review (BDLOP residual)"},
|
||||
{"property": "unforgeability/nonce-single-use", "test": "nonce_ledger.go:80; mithril_rss_hyperball_test.go:419", "claim": "B", "assurance": "test-proven"},
|
||||
{"property": "unforgeability/base-EUF-CMA", "test": "output bytes = FIPS-204", "claim": "A->B", "assurance": "sound-by-reduction (inherited)"},
|
||||
{"property": "authenticated-origin", "test": "distributed_bcc.go:883; ErrOriginAuthRequired :813", "claim": "B", "assurance": "test-proven"},
|
||||
{"property": "cross-version-wire-compat (incl. post-mlwe-dedup)", "test": "kat_test.go vs vectors/*.json", "claim": "A", "assurance": "interop-tested"},
|
||||
{"property": "cross-impl-arithmetic", "test": "dkg_vss_kat_test.go:104", "claim": "A", "assurance": "interop-tested"},
|
||||
{"property": "keygen/naive-additive-byte-fips-obstruction (fail-closed)", "test": "naive_additive_seta_obstruction.go:196,:242", "claim": "B", "assurance": "sound-by-reduction (parameter-derived)"},
|
||||
{"property": "keygen/KeyGen-distribution-equivalence (RSS)", "test": "NOT PROVEN (structural facts + stock-circl-verifiability only, rows 2,4)", "claim": "B", "assurance": "open-research"}
|
||||
]
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user