mirror of
https://github.com/luxfi/pulsar.git
synced 2026-07-26 22:53:49 +00:00
pulsar: TALUS docs to v1.2.0 — PULSAR-V13-W-LEAK closed (semi-honest), residuals scoped
TALUS threshold ML-DSA built: dealerless nonce DKG + CEF + REAL CSCP CarryCompare secure-comparison closes PULSAR-V13-W-LEAK (semi-honest, simulation-proven) — no node forms w0/w even transiently. FindHint + ReleaseGate bound malicious deviation to liveness (never forge/leak). Open items narrowed to Residual A (malicious-secure CSCP + networked non-simulation MPC) and Residual B (dealerless byte-FIPS-204 key DKG proven unreachable via S_eta bound -> trusted-dealer keygen; Corona carries permissionless). BLOCKERS reconciled, README/LLM/CHANGELOG/PROOF-CLAIMS refreshed; tag refs -> v1.2.0.
This commit is contained in:
zeekay
+90
-19
@@ -1,12 +1,19 @@
|
||||
# Finding registry — luxfi/pulsar
|
||||
|
||||
**Status: OPEN items present (see `## Open`).** The v1.1.1 byte-equality /
|
||||
ctx-bound / public-BFT claims are submission-ready, but the v0.3/v0.4
|
||||
leaderless threshold path has CRITICAL open findings (PULSAR-V13-*), and
|
||||
the EasyCrypt byte-equality proof rests on an OPEN reconstruct-then-sign
|
||||
axiom cone (PULSAR-EC-RECON-MODEL). None blocks the single-party / N4 /
|
||||
interop-tested BCC claims; all block any "production threshold path is
|
||||
proven" statement.
|
||||
**Status (v1.2.0): the TALUS threshold ML-DSA path is BUILT and
|
||||
PULSAR-V13-W-LEAK is CLOSED (semi-honest, simulation-proven).** The v1.1.x
|
||||
byte-equality / ctx-bound / public-BFT claims remain submission-ready. On the
|
||||
leaderless threshold path the REAL CSCP secure-comparison circuit closes the
|
||||
W-LEAK under an honest majority (commit `530c24e`); exactly TWO honest
|
||||
residuals remain open — **Residual A** (the CSCP malicious-secure /
|
||||
identifiable-abort layer, plus a networked non-simulation MPC deployment) and
|
||||
**Residual B** (dealerless byte-FIPS-204 KEY DKG is proven unreachable ⇒
|
||||
KEYGEN stays trusted-dealer; permissionless safety is carried by the dealerless
|
||||
Corona leg of the AND-mode Quasar cert). The EasyCrypt byte-equality proof
|
||||
still rests on an OPEN reconstruct-then-sign axiom cone
|
||||
(PULSAR-EC-RECON-MODEL). None of these blocks the single-party / N4 /
|
||||
interop-tested BCC claims; the two residuals block any "malicious-secure,
|
||||
networked, permissionless threshold path is proven" statement.
|
||||
|
||||
Forward-looking v1.2 extensions are tracked under
|
||||
`## Forward-looking (v1.2)` below; they are EXTENSIONS surfaced by the
|
||||
@@ -28,6 +35,41 @@ and the v1.0.7 sign-off.
|
||||
|
||||
## Open
|
||||
|
||||
**Open items (v1.2.0) = exactly two honest residuals on the TALUS threshold
|
||||
path.** The old "two novel components fail-closed — (i) tight small-norm
|
||||
lattice range proofs and (ii) HighBits-inside-MPC" framing is retired:
|
||||
component (ii) is now BUILT (that is exactly what the REAL CSCP
|
||||
secure-comparison does, semi-honest — PULSAR-V13-W-LEAK, now CLOSED), and
|
||||
component (i)'s malicious-secure VSS for the nonce DKG folds into Residual A
|
||||
(it is NOT a separate byte-equality blocker). The genuinely-open items are:
|
||||
|
||||
- **Residual A — CSCP is semi-honest-secure only (+ networked MPC).** The REAL
|
||||
CSCP secure-comparison circuit (`cscpSecureHighBitsVec`) closes the W-LEAK
|
||||
under an honest majority (N ≥ 2T−1, enforced by `TalusMinPartiesMPC` /
|
||||
`newCSCPCtx` / `bgwMulShares`), but it is proven leak-free in an in-process
|
||||
N-party SIMULATION, and the malicious-secure / identifiable-abort layer
|
||||
(Feldman/Pedersen-committed shares + verified openings + a bit-validity proof
|
||||
+ complaint round, including the malicious-secure VSS for the nonce DKG) is
|
||||
UN-built, as is a networked non-simulation deployment. A malicious deviation
|
||||
can never forge or leak — `FindHint` + `TalusReleaseGate` bound it to a
|
||||
LIVENESS fault (abort/retry) (`TestCSCP_WrongW1_CaughtByFindHint`). Detailed
|
||||
record: PULSAR-V13-HINT-LEAK (malicious-secure gates) + PULSAR-V13-W-LEAK
|
||||
(marked CLOSED below + its "Residual" paragraph).
|
||||
- **Residual B — dealerless byte-FIPS-204 KEY DKG is impossible (proven).**
|
||||
FIPS-204 KeyGen samples s1,s2 uniformly from S_η = {p : ‖p‖∞ ≤ η}; a
|
||||
dealerless DKG forms the joint secret as a sum/Lagrange combination of N ≥ 2
|
||||
contributions each in S_η, whose ℓ∞-support is up to N·η > η — not
|
||||
S_η-distributed. This breaks BCC byte-validity (‖c·s2‖∞ ≤ N·β > β) AND the
|
||||
FIPS-204 security-equivalence; forcing back into S_η "is exactly a dealer."
|
||||
Code: `distributed_bcc_dkg.go` returns `ErrDealerlessByteFIPSUnreachable`.
|
||||
THEREFORE KEYGEN stays **trusted-dealer** (`DealAlgShares`) and the
|
||||
**permissionless-public guarantee is carried by Corona** (natively dealerless
|
||||
via Pedersen DKG over R_q) in the Quasar AND-mode cert. Detailed record:
|
||||
PULSAR-V12-PARALLEL-PQ item 2 (`## Forward-looking`).
|
||||
|
||||
`PULSAR-EC-RECON-MODEL` below is a separate proof-scope disclosure (the EC
|
||||
reduction `no_leak_reduction`), not a threshold-path safety residual.
|
||||
|
||||
### PULSAR-EC-RECON-MODEL (HIGH — proof-scope disclosure; RE-SCOPED this pass)
|
||||
|
||||
**Status: OPEN, but RE-SCOPED — reconstruct-then-sign is no longer the
|
||||
@@ -131,15 +173,18 @@ exact off-by-one edges, offline yield ≈ **9.8 %**, and a no-leak single-key
|
||||
signature that verifies **byte-for-byte under CIRCL + pq-crystals** (ML-DSA-65/87).
|
||||
|
||||
**Status: leak removed + no-leak core complete + cert-verification hardened;
|
||||
the production threshold path remains gated FAIL-CLOSED pending external
|
||||
review of the novel ZK parts.** `[~]` = structurally complete in code but
|
||||
registered fail-closed pending review (NOT claimed proven). Resolution criteria:
|
||||
PULSAR-V13-W-LEAK is now CLOSED semi-honest on the TALUS-MPC CSCP path (see
|
||||
its CLOSED marker below), and the remaining malicious-secure / range-proof
|
||||
gates are the open **Residual A**.** `[~]` = structurally complete in code,
|
||||
semi-honest; the malicious-secure hardening is Residual A (a deviation is
|
||||
liveness-only via `FindHint` + `TalusReleaseGate`, never forge/leak).
|
||||
Resolution criteria:
|
||||
- [x] v0.3 `AlgebraicAggregate*` path **removed** from the codebase (not merely gated).
|
||||
- [x] Hint derived only via public `FindHint(w', w1)` (FIPS `UseHint`); secret `makeHint` deleted.
|
||||
- [x] No production code computes `c·s2`/`c·t0`/`r0`/`LowBits(residual)`.
|
||||
- [x] Boundary predicate proves the hidden `r0` bound; ML-DSA-65/87 scope enforced (`ErrBCCParamSet`).
|
||||
- [x] `CS2`/`CT0` + all hint-secret wire fields deleted; reflection guard (`TestNoHintSecretFieldsInProductionWireTypes`) enforces it.
|
||||
- [~] **Full `w` never on the wire** — `NonceCert` carries only `w1` + a commitment + the clearance QC; the ZK boundary-clearance proof that a hidden `w` is clear is registered **fail-closed** (`ErrClearanceProofUnsound`) pending review (PULSAR-V13-W-LEAK).
|
||||
- [x] **Full `w` never on the wire** — CLOSED semi-honest on the TALUS-MPC CSCP path: no node forms `w`/`w0`/`A0` even transiently, and `NonceCert` carries only `w1` + a binding commitment (simulation-proven — see PULSAR-V13-W-LEAK, marked CLOSED below). The earlier debug-oracle ZK-boundary-clearance prototype (`ErrClearanceProofUnsound`) is superseded by the REAL CSCP secure-comparison; the malicious-secure layer is Residual A.
|
||||
- [~] Partial-`z` correctness — sound linear sigma proof, FS-bound, challenge validated as `SampleInBall` (`partial_proof.go`); registered **fail-closed** by default; the small-norm range gate is fail-closed (L2-vs-L∞, no faithful proof exists).
|
||||
- [x] Canonical, non-grindable nonce selection (`CanonicalNonceIndex`).
|
||||
- [~] DKG never reconstructs the master key / `t0` (`DKGPublicOutput`, no `t0`); sound DKG linear proof; the `t0`-bound range gate is fail-closed pending review.
|
||||
@@ -147,9 +192,20 @@ registered fail-closed pending review (NOT claimed proven). Resolution criteria:
|
||||
- [x] Tree aggregation (z-sums + bitmaps + proof roots) for ~1000 signers.
|
||||
- [x] Two-certificate consensus artifact — ML-DSA sig + signer bitmap **bound to the signature** via an accountability QC (`ConsensusCert.Verify`).
|
||||
- [x] Final sigs verify under ≥2 independent FIPS 204 verifiers (CIRCL + pq-crystals) on the BCC path.
|
||||
- [ ] External cryptographic review of the no-MPC leaderless instantiation (the remaining gate).
|
||||
- [ ] External cryptographic review + the malicious-secure CSCP layer and a networked, non-simulation MPC deployment (**Residual A** — the remaining gate; the semi-honest leak-free property is already proven in simulation).
|
||||
|
||||
### PULSAR-V13-W-LEAK (CRITICAL — replacement-design hazard)
|
||||
### PULSAR-V13-W-LEAK (CLOSED — semi-honest, simulation-proven, v1.2.0; TALUS-MPC CSCP path)
|
||||
|
||||
**Status**: CLOSED on the TALUS-MPC CSCP path (commit `530c24e`) — semi-honest,
|
||||
honest-majority (N ≥ 2T−1), proven leak-free in an in-process N-party
|
||||
SIMULATION (the harness holds all parties' shares; it is the *algorithm* that
|
||||
never reconstructs `w`/`w0`, faithfully proven — but this is NOT yet a
|
||||
networked/deployed distributed MPC). The orthogonal malicious-secure /
|
||||
identifiable-abort layer (and a networked, non-simulation MPC deployment) is the
|
||||
named **Residual A** (see `## Open`); a malicious deviation is bounded to
|
||||
liveness (abort/retry) by `FindHint` + `TalusReleaseGate`, never forge or leak.
|
||||
Retained here with the HINT-LEAK cluster for narrative continuity; the registry
|
||||
pointer lives in `## Closed`. The hazard history and the closure proof follow.
|
||||
|
||||
The boundary-cleared nonce certificate must **not** publish the full
|
||||
commitment `w = A·y`. Once `z` is assembled, `w' = A·z − c·t1·2^d` is
|
||||
@@ -321,12 +377,13 @@ group-key signature in the consensus multi-node test.
|
||||
but **no concrete poly-vector share type or concrete `RoundSigner`
|
||||
implementor exists on the current line** (the v0.3 algebraic stack was
|
||||
removed in the b185533 consolidation).
|
||||
- Even with poly-vector shares, the leaderless production path stays
|
||||
fenced **fail-closed** behind the two unproven ZK gates:
|
||||
**PULSAR-V13-W-LEAK** (the distributed boundary-clear NONCE proof —
|
||||
"does not yet exist ⇒ the BCC/CEF signing path is prototype, not
|
||||
production") and **PULSAR-V13-PARTIAL-Z-PROOF** (the proof-carrying
|
||||
z-partial verifier, `RegisterPartialZVerifier` default-fail-closed).
|
||||
- The leaderless production path is now BUILT (TALUS, v1.2.0):
|
||||
**PULSAR-V13-W-LEAK** is CLOSED semi-honest on the TALUS-MPC CSCP path
|
||||
(marked CLOSED above) and **PULSAR-V13-PARTIAL-Z-PROOF** is functionally
|
||||
closed on the no-reconstruct path. The remaining open work is **Residual A**
|
||||
(the CSCP malicious-secure / identifiable-abort layer + a networked,
|
||||
non-simulation MPC deployment); a malicious deviation is liveness-only via
|
||||
`FindHint` + `TalusReleaseGate`, never forge or leak.
|
||||
|
||||
**Why the consumer is permissionless-safe anyway.** The consensus cert
|
||||
is AND-mode and the **Corona leg is genuinely dealerless and
|
||||
@@ -552,6 +609,20 @@ MLDSA batch path once the substrate ships.
|
||||
|
||||
## Closed
|
||||
|
||||
### PULSAR-V13-W-LEAK — CLOSED semi-honest (v1.2.0)
|
||||
|
||||
**Status**: CLOSED (semi-honest, simulation-proven), commit `530c24e`. The
|
||||
REAL CSCP secure-comparison circuit (`talus_cscp.go::cscpSecureHighBitsVec`,
|
||||
driven by `CEFComputeW1`) realises the ideal so that no node forms `w`/`w0`/`A0`
|
||||
even transiently — proven leak-free by `TestCSCP_MultiNode_LeakFree` /
|
||||
`TestCSCP_LeakFree_Structural` / `TestCSCP_MaskOpen_HidesW` in an in-process
|
||||
N-party SIMULATION. The full hazard description and closure narrative are
|
||||
retained in-place with the V13 threshold-path cluster above (its header is
|
||||
marked CLOSED). The orthogonal malicious-secure / identifiable-abort layer + a
|
||||
networked, non-simulation MPC deployment is the open **Residual A** (`## Open`);
|
||||
a malicious deviation is bounded to a liveness fault (abort/retry) by `FindHint`
|
||||
+ `TalusReleaseGate`, never forge or leak (`TestCSCP_WrongW1_CaughtByFindHint`).
|
||||
|
||||
### PULSAR-V04-CTX — v0.4 ctx-bound threshold sign (FIPS 204 §5.4)
|
||||
|
||||
**Status**: CLOSED in v1.1.1 (tag pending — see CHANGELOG.md for the
|
||||
|
||||
@@ -4,6 +4,64 @@ This file tracks substantive changes to the EasyCrypt proof
|
||||
artifact, the spec, and the residual trust footprint. For
|
||||
implementation-level changes see `git log`.
|
||||
|
||||
## v1.2.0 — TALUS threshold ML-DSA (one-round online; W-LEAK closed semi-honest)
|
||||
|
||||
TALUS is the threshold ML-DSA scheme on the two-round lattice kernel, adding
|
||||
**one-round online signing** via three pillars: a dealerless Shamir **nonce
|
||||
DKG**, the **CEF** (Carry Elimination Framework, distributed `w1`), and **CSCP**
|
||||
(the CarryCompare secure-comparison protocol). Source:
|
||||
`ref/go/pkg/pulsar/talus*.go`.
|
||||
|
||||
**PULSAR-V13-W-LEAK closed (semi-honest, simulation-proven).** Commit
|
||||
`530c24e` lands the REAL CSCP secure-comparison circuit (bit-decompose +
|
||||
carry-save `bitAdd` + prefix `bitLT` over BGW multiplication, validated
|
||||
coefficient-exact against FIPS Decompose). On the production
|
||||
`CEFComputeW1` → `cscpSecureHighBitsVec` path NO node forms `w0` or the full
|
||||
commitment `w` even transiently — only three masked openings
|
||||
(`{valid, maskC, w1}`) — proven leak-free by `TestCSCP_MultiNode_LeakFree`,
|
||||
`TestCSCP_LeakFree_Structural`, and `TestCSCP_MaskOpen_HidesW`. HONEST SCOPE:
|
||||
this is an in-process N-party SIMULATION (the harness holds all parties'
|
||||
shares); the *algorithm* never reconstructs `w`/`w0`, faithfully proven, but
|
||||
this is NOT yet a networked/deployed distributed MPC and the malicious-secure
|
||||
layer is unbuilt.
|
||||
|
||||
- **Two profiles.** **Pulsar-TEE** (TEE-backed `w1` source) and **Pulsar-MPC**
|
||||
(honest-majority N ≥ 2T−1, enforced by `TalusMinPartiesMPC` / `newCSCPCtx` /
|
||||
`cscpSecureHighBitsVec` / `bgwMulShares`). The emitted signature is
|
||||
byte-identical across profiles.
|
||||
- **Stock FIPS-204 verify.** A TALUS signature verifies byte-equal under the
|
||||
UNMODIFIED `cloudflare/circl` `mldsa65.Verify` / `mldsa87.Verify`
|
||||
(`TestTalus_MPC_EndToEnd_StockVerify`, `TestTalus_MPC_Mode87`).
|
||||
- **Malicious deviation = liveness-only.** `FindHint` (recovers the FIPS hint
|
||||
from public `w' = A·z − c·t1·2^d`) + `TalusReleaseGate` (mandatory stock
|
||||
FIPS-204 verify; never releases a failed signature) bound any malicious CSCP
|
||||
deviation to abort/retry — never forge or leak
|
||||
(`TestCSCP_WrongW1_CaughtByFindHint`). This is the open **Residual A** (the
|
||||
CSCP malicious-secure / identifiable-abort layer + a networked,
|
||||
non-simulation MPC deployment).
|
||||
- **KEYGEN stays trusted-dealer (Residual B).** Dealerless byte-FIPS-204 KEY
|
||||
DKG is *proven unreachable*: FIPS-204 KeyGen samples `s1,s2` from
|
||||
`S_η = {p : ‖p‖∞ ≤ η}`, but a dealerless sum/Lagrange combination of N ≥ 2
|
||||
contributions has ℓ∞-support up to `N·η > η`, breaking BCC byte-validity
|
||||
(`‖c·s2‖∞ ≤ N·β > β`) and the FIPS-204 security-equivalence
|
||||
(`distributed_bcc_dkg.go` returns `ErrDealerlessByteFIPSUnreachable`). KEYGEN
|
||||
therefore stays trusted-dealer (`DealAlgShares`); the
|
||||
**permissionless-public guarantee is carried by Corona** (natively dealerless
|
||||
via Pedersen DKG over `R_q`), composed alongside Pulsar in the Quasar AND-mode
|
||||
dual-PQ cert.
|
||||
|
||||
## v1.1.0 – v1.1.5 — BCC/CEF byte-equal threshold ML-DSA + honest-status hardening
|
||||
|
||||
The Boundary-Clearance-Condition (BCC) + Carry-Elimination (CEF)
|
||||
no-reconstruct signing path: the hint is recovered from the **public**
|
||||
`w' = A·z − c·t1·2^d` via `FindHint` (FIPS `UseHint`), no production code forms
|
||||
`c·s2`/`c·t0`/`r0`, and the single-key BCC signature verifies byte-for-byte
|
||||
under CIRCL + pq-crystals (ML-DSA-65/87). The leaking v0.3 `AlgebraicAggregate*`
|
||||
path was deleted forward-only; PULSAR-V04-CTX (FIPS 204 §5.4 ctx-bound sign)
|
||||
closed; and the proof-claim vocabulary was hardened to an honest two-model
|
||||
framing (idealised reconstruct-then-sign vs the production no-leak residual
|
||||
under a standard Module-LWE / Module-SIS reduction).
|
||||
|
||||
## v1.0.14 — v0.2 honesty rename (Algebraic → Transitional)
|
||||
|
||||
The v0.2 API previously named `Algebraic*` was materially
|
||||
|
||||
@@ -2,8 +2,8 @@
|
||||
|
||||
**Repository (current)**: github.com/luxfi/pulsar
|
||||
**Repository (target)**: github.com/luxfi/pulsar
|
||||
**Latest Tag**: v1.1.4
|
||||
**Status**: Research / Reference (not production hardened, not FIPS validated). EasyCrypt + Lean machine-check on host (gate `ec-machine-check.sh`, 14/14); no-leak BCC threshold path interop-verified under CIRCL + pq-crystals.
|
||||
**Latest Tag**: v1.2.0
|
||||
**Status**: TALUS threshold ML-DSA BUILT; PULSAR-V13-W-LEAK CLOSED (semi-honest, simulation-proven). Not yet FIPS-validated; open residuals = the malicious-secure CSCP layer + a networked MPC deployment (Residual A) and dealerless-key impossibility ⇒ trusted-dealer keygen + Corona-carries-permissionless (Residual B). EasyCrypt + Lean machine-check on host (gate `ec-machine-check.sh`, 14/14); TALUS / no-leak BCC threshold path interop-verified byte-equal under CIRCL + pq-crystals.
|
||||
|
||||
## Rename in progress: Pulsar-M → Pulsar
|
||||
|
||||
@@ -148,14 +148,56 @@ and resolve before advancing.
|
||||
|
||||
## Purpose (one-liner)
|
||||
|
||||
Threshold ML-DSA: 2-round threshold signing and DKG whose generated
|
||||
signatures are verifiable by **unmodified FIPS 204 ML-DSA verification**.
|
||||
Targeting NIST MPTC Class N1 (signing) + N4 (ML keygen / DKG).
|
||||
Threshold ML-DSA: a two-round lattice kernel + one-round online signing
|
||||
(TALUS) and DKG whose generated signatures are verifiable by **unmodified
|
||||
FIPS 204 ML-DSA verification**. Targeting NIST MPTC Class N1 (signing) + N4
|
||||
(ML keygen / DKG).
|
||||
|
||||
Pulsar-M is the Module-LWE sibling of `luxfi/pulsar` (Ring-LWE). Pulsar's
|
||||
2-round protocol is transplanted onto ML-DSA-65's polynomial-vector-over-`R_q`
|
||||
two-round kernel is transplanted onto ML-DSA-65's polynomial-vector-over-`R_q`
|
||||
algebra so the aggregated signature is bit-identical to a single-party
|
||||
FIPS 204 signature on the same message + public key.
|
||||
FIPS 204 signature on the same message + public key; TALUS (v1.2.0) adds
|
||||
one-round online signing on top.
|
||||
|
||||
## TALUS — threshold ML-DSA (v1.2.0)
|
||||
|
||||
TALUS is the threshold ML-DSA scheme on Pulsar's two-round lattice kernel,
|
||||
adding **one-round online signing**. Source: `ref/go/pkg/pulsar/talus*.go`.
|
||||
|
||||
- **Three pillars.** Dealerless Shamir **nonce DKG** (`talus_nonce_dkg.go`),
|
||||
**CEF** = Carry Elimination Framework / distributed `w1` (`talus_cef.go`),
|
||||
**CSCP** = the CarryCompare secure-comparison protocol (`talus_cscp.go`).
|
||||
BCC = Boundary Clearance Condition. These route around the impossibility of
|
||||
FROST-style additive-nonce threshold ML-DSA (HighBits/r0/carry is non-linear).
|
||||
- **W-LEAK closed (semi-honest, simulation-proven).** Commit `530c24e`: the
|
||||
REAL CSCP secure-comparison circuit (bit-decompose + carry-save bitAdd +
|
||||
prefix bitLT over BGW multiplication, coefficient-exact vs FIPS Decompose)
|
||||
drives `CEFComputeW1` → `cscpSecureHighBitsVec`, so NO node forms `w0` or the
|
||||
full commitment `w` even transiently (only masked openings {valid, maskC,
|
||||
w1}). Proven leak-free by `TestCSCP_MultiNode_LeakFree` /
|
||||
`TestCSCP_LeakFree_Structural` / `TestCSCP_MaskOpen_HidesW` — but in an
|
||||
in-process N-party SIMULATION (NOT a networked/deployed MPC, NOT
|
||||
malicious-secure). Always describe as **semi-honest, simulation-proven**.
|
||||
- **Two profiles.** **Pulsar-TEE** (TEE-backed `w1`) and **Pulsar-MPC**
|
||||
(honest-majority N ≥ 2T−1, enforced by `TalusMinPartiesMPC` / `newCSCPCtx` /
|
||||
`cscpSecureHighBitsVec` / `bgwMulShares`). Signature byte-identical across both.
|
||||
- **Stock FIPS-204.** A TALUS signature verifies byte-equal under UNMODIFIED
|
||||
`cloudflare/circl` `mldsa65.Verify` / `mldsa87.Verify`
|
||||
(`TestTalus_MPC_EndToEnd_StockVerify`, `TestTalus_MPC_Mode87`).
|
||||
- **Malicious deviation = liveness-only.** `FindHint` (recovers the FIPS hint
|
||||
from public `w' = A·z − c·t1·2^d`) + `TalusReleaseGate` (mandatory stock
|
||||
FIPS-204 verify, never releases a failed sig) bound any malicious CSCP
|
||||
deviation to abort/retry — never forge or leak
|
||||
(`TestCSCP_WrongW1_CaughtByFindHint`). This is **Residual A** (the
|
||||
malicious-secure CSCP layer + a networked MPC deployment, un-built).
|
||||
- **KEYGEN is trusted-dealer (Residual B).** Dealerless byte-FIPS-204 KEY DKG
|
||||
is *proven unreachable*: FIPS-204 KeyGen samples s1,s2 from S_η = {‖p‖∞ ≤ η};
|
||||
a dealerless sum of N ≥ 2 contributions has ℓ∞-support up to N·η > η, breaking
|
||||
BCC byte-validity (‖c·s2‖∞ ≤ N·β > β) and the FIPS-204 security-equivalence
|
||||
(`distributed_bcc_dkg.go` → `ErrDealerlessByteFIPSUnreachable`). KEYGEN stays
|
||||
trusted-dealer; the **permissionless guarantee is carried by Corona**
|
||||
(corona v0.8.0, natively dealerless via Pedersen DKG over R_q) in the Quasar
|
||||
AND-mode cert.
|
||||
|
||||
## Canonical profile + scheme constants
|
||||
|
||||
@@ -166,7 +208,7 @@ FIPS 204 signature on the same message + public key.
|
||||
share. Canonical extreme committee target: `TargetCommitteeSize =
|
||||
1_111_111` (seven 1s).
|
||||
- Curve / lattice: same Module-LWE parameters as ML-DSA-65.
|
||||
- Round count: 2 (commit + reveal).
|
||||
- Round count: two-round kernel (commit + reveal); TALUS adds one-round online signing.
|
||||
- Abort model: identifiable.
|
||||
- Arithmetic width: uint32 lanes with uint64 accumulators. uint128 /
|
||||
uint256 not required (reserved for the Z-Chain SNARK side).
|
||||
@@ -187,7 +229,7 @@ FIPS 204 signature on the same message + public key.
|
||||
|
||||
## Active versions
|
||||
|
||||
- Repo: `v1.1.4` (current; patch-bump only, next `v1.1.5`).
|
||||
- Repo: `v1.2.0` (current; TALUS threshold ML-DSA + PULSAR-V13-W-LEAK closed semi-honest).
|
||||
- Pinned by: `luxfi/consensus v1.23.5+` (finality verify path replaces
|
||||
the placeholder Pulsar-M verifier).
|
||||
|
||||
|
||||
@@ -17,6 +17,7 @@
|
||||
| **machine-checked** | A proof assistant verifies it; the named EasyCrypt or Lean theory has ZERO `sorry` / `admit.` / `:= True` (real tactics, per the repo's own admit gate). The EasyCrypt toolchain **is live on the host** (opam switch `proofs`: easycrypt + why3 + alt-ergo, z3 solver) — all theories compile under `easycrypt compile`, enforced every run by `security/framework/checks/ec-machine-check.sh` (pulsar 14/14). Lean compiles under `lake build`. |
|
||||
| **sound-by-reduction** | A pen-and-paper reduction to a stated assumption exists; not mechanized. |
|
||||
| **interop-tested** | Validated by running against ≥2 INDEPENDENT implementations (CIRCL + pq-crystals), not the signer's own library. |
|
||||
| **test-proven** | A property established by executable tests (transcript / structural / reflection / round-trip), not a proof assistant or a reduction; the tests are named. For TALUS-CSCP this is **semi-honest** and runs in an in-process N-party **SIMULATION** (not a networked MPC, not malicious-secure). |
|
||||
| **asserted-axiom** | Taken as an axiom in EC; bucketed in AXIOM-INVENTORY.md (A/B). Not proved here. |
|
||||
| **fail-closed-pending-review** | Implemented but gated to REFUSE until external review; not claimed correct. |
|
||||
| **open-research** | Not done; multi-month roadmap. |
|
||||
@@ -89,6 +90,23 @@
|
||||
| 5 Lagrange/algebra identities | machine-checked (Lean 4 + Mathlib), asserted-axiom (EC side) | `proofs/lean-easycrypt-bridge.md`; `scripts/check-lean-bridge.sh` |
|
||||
| FIPS 204 per-type codec round-trips (B-cone) | asserted-axiom | AXIOM-INVENTORY.md §B; closing = Dilithium codec mechanization (open-research) |
|
||||
| ML-DSA post-quantum hardness (M-LWE/M-SIS) | open-research (inherited) | NIST FIPS 204 analysis; NOT a Pulsar claim |
|
||||
| TALUS sig verifies under stock FIPS-204 (circl `mldsa65`/`mldsa87.Verify`) | interop-tested (unmodified upstream verifier) | `TestTalus_MPC_EndToEnd_StockVerify`, `TestTalus_MPC_Mode87`; BCC single-key also byte-equal under CIRCL + pq-crystals |
|
||||
| TALUS CSCP path leak-free (no node forms `w`/`w0`/`A0`; only `{valid,maskC,w1}` opened) | **test-proven — semi-honest, in-process N-party SIMULATION** (NOT machine-checked, NOT a networked MPC) | `TestCSCP_MultiNode_LeakFree`, `TestCSCP_LeakFree_Structural`, `TestCSCP_MaskOpen_HidesW` (transcript + source-structural + reflection) |
|
||||
| TALUS malicious CSCP deviation = liveness-only (never forge/leak) | test-proven (FindHint + `TalusReleaseGate` mandatory stock verify) | `TestCSCP_WrongW1_CaughtByFindHint`; a corrupt `w1` is caught by `FindHint`, the release-gate refuses any non-verifying signature |
|
||||
| Dealerless byte-FIPS-204 KEY DKG impossible (S_η argument) | sound-by-reduction (parameter-derived obstruction) | `distributed_bcc_dkg.go` → `ErrDealerlessByteFIPSUnreachable`; `s1,s2 ∈ S_η = {‖p‖∞ ≤ η}`, a dealerless sum has ‖·‖∞ ≤ N·η > η ⇒ breaks BCC (‖c·s2‖∞ ≤ N·β > β) + FIPS-204 equivalence; KEYGEN trusted-dealer, Corona carries permissionless |
|
||||
|
||||
### §2 addendum — TALUS / CSCP assurance (v1.2.0)
|
||||
|
||||
The four rows above record the v1.2.0 TALUS threshold ML-DSA assurance. The
|
||||
leak-free CSCP property (`w`/`w0` never formed) is **semi-honest and proven in
|
||||
an in-process N-party SIMULATION** — the harness holds every party's shares; it
|
||||
is the *algorithm* that never reconstructs `w`/`w0`, faithfully proven, but this
|
||||
is NOT yet a networked/deployed distributed MPC, and the malicious-secure CSCP
|
||||
layer is UNBUILT (**Residual A**, `BLOCKERS.md`). A malicious deviation can
|
||||
never forge or leak — `FindHint` + `TalusReleaseGate` bound it to a liveness
|
||||
fault. KEYGEN stays trusted-dealer because dealerless byte-FIPS-204 KEY DKG is
|
||||
proven unreachable (**Residual B**); the permissionless-public guarantee is
|
||||
carried by the dealerless Corona leg of the Quasar AND-mode cert.
|
||||
|
||||
## §3 What is NOT proved (the load-bearing honesty disclosure)
|
||||
|
||||
@@ -100,6 +118,11 @@
|
||||
3. **ML-DSA hardness, side-channels beyond jasmin-CT, adaptive-corruption
|
||||
unforgeability, robust completion, async identifiable-abort** — not
|
||||
proved here (see `docs/proof-claims.md` §3 for the full list).
|
||||
4. **The TALUS leak-free property is semi-honest and simulation-only.** It is
|
||||
not machine-checked, not a networked MPC deployment, and the malicious-secure
|
||||
CSCP layer is unbuilt (Residual A). KEYGEN is trusted-dealer (dealerless
|
||||
byte-FIPS-204 KEY DKG is proven unreachable, Residual B); permissionless
|
||||
safety rests on Corona.
|
||||
|
||||
## §4 The honest one-paragraph version
|
||||
|
||||
|
||||
@@ -1,8 +1,9 @@
|
||||
# Pulsar — NIST MPTC submission package
|
||||
|
||||
> **Threshold ML-DSA** — a 2-round threshold signing and DKG system whose
|
||||
> generated signatures are verifiable by **unmodified FIPS 204 ML-DSA
|
||||
> verification**. Targeting NIST MPTC Class N1 (signing) + N4 (ML keygen / DKG).
|
||||
> **Threshold ML-DSA** — a two-round lattice kernel (TALUS adds one-round
|
||||
> online signing) for threshold signing and DKG whose generated signatures are
|
||||
> verifiable by **unmodified FIPS 204 ML-DSA verification**. Targeting NIST
|
||||
> MPTC Class N1 (signing) + N4 (ML keygen / DKG).
|
||||
|
||||
This repository is the **active NIST MPTC submission package** for Pulsar
|
||||
and the canonical home for the submission artifacts (spec, KAT vectors,
|
||||
@@ -18,10 +19,11 @@ is the identifier NIST receives and reviews against.
|
||||
|
||||
## Library identities (post-2026 split)
|
||||
|
||||
`Pulsar` is the Module-LWE threshold ML-DSA construction. The 2-round
|
||||
threshold protocol structure operates on ML-DSA-65's polynomial-vector-
|
||||
over-`R_q` algebra so the per-party-aggregated signature is bit-identical
|
||||
to a single-party FIPS 204 signature on the same message + public key.
|
||||
`Pulsar` is the Module-LWE threshold ML-DSA construction. The two-round
|
||||
lattice kernel operates on ML-DSA-65's polynomial-vector-over-`R_q` algebra so
|
||||
the per-party-aggregated signature is bit-identical to a single-party FIPS 204
|
||||
signature on the same message + public key; TALUS (v1.2.0) adds one-round
|
||||
online signing on top of that kernel.
|
||||
|
||||
> **Aggregator-honesty caveat (v0.2 vs v0.3).** Bit-identity to a
|
||||
> single-party FIPS 204 signature is achieved without master-secret
|
||||
@@ -47,14 +49,47 @@ The module path inside this submission package remains
|
||||
`github.com/luxfi/pulsar` because that is the identifier NIST receives
|
||||
and reviews against the submitted KAT vectors and spec. Downstream
|
||||
consumers who want the live production library should pin
|
||||
`github.com/luxfi/pulsar@v1.0.x` (Module-LWE) or
|
||||
`github.com/luxfi/pulsar@v1.2.x` (Module-LWE) or
|
||||
`github.com/luxfi/corona@v0.2.x` (Ring-LWE) instead.
|
||||
|
||||
> **Status.** Algorithm-level reference implementation. NIST-profile
|
||||
> vectors use SHAKE / cSHAKE / KMAC (FIPS 202 + SP 800-185); the
|
||||
> MPTC submission excludes BLAKE3. Deployed-binary tracks (Rust
|
||||
> crate, C library, WASM, no_std) carry their own constant-time
|
||||
> audit + KAT cross-validation before claiming production posture.
|
||||
> **Status (v1.2.0).** Algorithm-level reference implementation. The TALUS
|
||||
> threshold ML-DSA path (dealerless nonce DKG + CEF + CSCP) is BUILT and
|
||||
> PULSAR-V13-W-LEAK is CLOSED (semi-honest, simulation-proven); the two open
|
||||
> residuals are the CSCP malicious-secure layer + a networked MPC deployment
|
||||
> (Residual A) and dealerless-key impossibility ⇒ trusted-dealer keygen with
|
||||
> Corona carrying permissionless (Residual B) — see `BLOCKERS.md`. NIST-profile
|
||||
> vectors use SHAKE / cSHAKE / KMAC (FIPS 202 + SP 800-185); the MPTC
|
||||
> submission excludes BLAKE3. Deployed-binary tracks (Rust crate, C library,
|
||||
> WASM, no_std) carry their own constant-time audit + KAT cross-validation
|
||||
> before claiming production posture.
|
||||
|
||||
## TALUS — one-round online threshold signing (v1.2.0)
|
||||
|
||||
TALUS is the threshold ML-DSA scheme built on the two-round lattice kernel; it
|
||||
adds **one-round online signing** via three pillars — a dealerless Shamir
|
||||
**nonce DKG**, the **CEF** (Carry Elimination Framework, distributed `w1`), and
|
||||
**CSCP** (the CarryCompare secure-comparison protocol). FROST-style
|
||||
additive-nonce threshold ML-DSA is impossible (HighBits/r0/carry rounding is
|
||||
non-linear; no homomorphic nonce commitment exists); TALUS routes around it
|
||||
with the BCC (Boundary Clearance Condition) + CEF + dealerless nonce DKG.
|
||||
|
||||
- **Two profiles.** **Pulsar-TEE** — a TEE-backed `w1` source. **Pulsar-MPC** —
|
||||
TEE-free, honest-majority (N ≥ 2T−1); no node forms the joint nonce `ȳ` or
|
||||
the commitment `w`. The emitted signature is byte-identical across profiles.
|
||||
- **W-LEAK closed (semi-honest, simulation-proven).** The REAL CSCP
|
||||
secure-comparison circuit computes `w1 = HighBits(Σ g_i mod q)` so that NO
|
||||
node forms `w0` or the full commitment `w` even transiently — proven leak-free
|
||||
by transcript / structural / reflection tests in an in-process N-party
|
||||
SIMULATION (not yet a networked deployment; the malicious-secure layer is
|
||||
unbuilt — see `BLOCKERS.md` Residual A).
|
||||
- **Stock FIPS-204 verify.** A TALUS signature verifies byte-equal under the
|
||||
UNMODIFIED `cloudflare/circl` `mldsa65.Verify` / `mldsa87.Verify`; `FindHint`
|
||||
+ a mandatory release-gate verify bound any malicious CSCP deviation to
|
||||
liveness-only (abort/retry) — never forge or leak.
|
||||
- **KEYGEN is trusted-dealer.** Dealerless byte-FIPS-204 KEY DKG is *proven
|
||||
unreachable* (a sum-of-contributions secret leaves S_η = {‖p‖∞ ≤ η}); the
|
||||
**permissionless-public guarantee is carried by Corona** (natively dealerless)
|
||||
in the Quasar AND-mode dual-PQ cert (Residual B).
|
||||
|
||||
## High-assurance headline
|
||||
|
||||
@@ -144,7 +179,7 @@ The win, if Pulsar's Sign output is byte-equal to FIPS 204 Sign:
|
||||
|
||||
```
|
||||
pulsar/
|
||||
├── BLOCKERS.md closed-finding registry (Open: none; Closed: PULSAR-V03-1 v1.0.20 ExpandA-convention fix postmortem)
|
||||
├── BLOCKERS.md finding registry (Open: Residual A — CSCP malicious-secure + networked MPC; Residual B — dealerless-key impossible ⇒ trusted-dealer keygen + Corona carries permissionless. Closed: PULSAR-V13-W-LEAK semi-honest v1.2.0; PULSAR-V03-1 v1.0.20 ExpandA fix)
|
||||
├── SUBMISSION.md NIST MPTC cover sheet (single source of truth for reviewer)
|
||||
├── CHANGELOG.md per-version proof artefact log (v4 → v13)
|
||||
├── README.md this file
|
||||
|
||||
Reference in New Issue
Block a user