mirror of
https://github.com/luxfi/pulsar.git
synced 2026-07-26 22:53:49 +00:00
PULSAR-V13: contain hint-path leak + land verified BCC/CEF math core
- hard-gate threshold_v03 AlgebraicAggregate (fail-closed, PULSAR-V13-HINT-LEAK) - threshold_bcc.go: BoundaryClear + findHintToTarget (FIPS UseHint) + ML-DSA-65/87 param guard; no production code forms c*s2/c*t0/r0/LowBits - 6 verified tests green (gate, param guard, FindHintToTarget<->UseHint round-trip, BoundaryClear=>HighBits-stable+r0-bound, off-by-one edges, yield 9.8%) - spec/threshold-mldsa-boundary-clearance.tex (BCC0/BCC+, full-w-hidden, ZK req) - BLOCKERS: V13-HINT-LEAK + V13-W-LEAK + V13-PARTIAL-Z-PROOF + resolution criteria
This commit is contained in:
Antje Worring
+79
-1
@@ -22,7 +22,85 @@ and the v1.0.7 sign-off.
|
||||
|
||||
## Open
|
||||
|
||||
None.
|
||||
### PULSAR-V13-HINT-LEAK (CRITICAL)
|
||||
|
||||
The v0.3/v0.4 `AlgebraicAggregate*` path broadcasts `CS2 = c·λ_i·s_{2,i}`
|
||||
and `CT0 = c·λ_i·t_{0,i}` **unmasked** (`ref/go/pkg/pulsar/threshold_v03.go`
|
||||
round2EmitFull, ~:930-963) and reconstructs `c·s2_joint`, `c·t0_joint` at
|
||||
the aggregator (~:1131-1168). Both are secret-key-derived: `c`, `λ_i`
|
||||
public ⇒ `s_{2,i} = (c·λ_i)^{-1}·CS2` (one session when `c` invertible;
|
||||
else accumulate). Worse, `c·s2_joint = c·s2_master` (Shamir), so revealing
|
||||
the **aggregate** over varying public `c` leaks the long-term secret-key
|
||||
components `s2` (and likewise `t0`) via a linear system, plus the secret
|
||||
relation `A·s1 = (t1·2^d + t0) − s2`; whether or not this immediately
|
||||
recovers short `s1` (a lattice/preimage problem), threshold secrecy and
|
||||
transcript simulation are already broken. Leaderless ⇒ every
|
||||
quorum member aggregates ⇒ every corrupt validator learns it each round.
|
||||
The in-code `PUBLIC-BFT-SAFETY NOTE` claiming `(z_i,cs2_i,ct0_i)` are
|
||||
`(t−1)`-secret is **false** — it only covers the `y_i`-masked `z_i`.
|
||||
|
||||
Confirmed by adversarial audit (`AUDIT-2026-06.md` re-audit) + direct code
|
||||
read. Masking the individual shares is necessary but **not** sufficient —
|
||||
the aggregate reconstruction still leaks the master key. The fix must
|
||||
never reconstruct `c·s2`/`c·t0`/`r0`.
|
||||
|
||||
**Containment (landed, branch `fix/threshold-mldsa-hint-leak`):**
|
||||
`Round2Sign` now **fails closed** with `ErrUnsafeThresholdV03HintPath`
|
||||
unless `AllowUnsafeThresholdV03ForTests` is set (test
|
||||
`TestThresholdV03DisabledByDefault`). The dangerously-false `(t−1)`-secret
|
||||
note is corrected.
|
||||
|
||||
**Replacement design + verified math core:** boundary-cleared nonces +
|
||||
carry elimination (`spec/threshold-mldsa-boundary-clearance.tex`,
|
||||
`threshold_bcc.go`). The hint is computed from the **public**
|
||||
`w' = A·z − c·t1·2^d` and `w1 = HighBits(w)` strictly via FIPS `UseHint`
|
||||
(`findHintToTarget`); boundary clearance (margin `2β`) keeps the small
|
||||
`c·s2` shift off the boundary; `c·t0` is structurally
|
||||
`‖c·t0‖∞ ≤ τ·2^{d-1} < γ2` for **ML-DSA-65/87 only** (param-guarded).
|
||||
Verified (`threshold_bcc_test.go`, all green): `FindHintToTarget↔UseHint`
|
||||
round-trip, `BoundaryClear ⇒ HighBits-stable + r0-bound`, exact off-by-one
|
||||
edges, offline yield ≈ **9.8 %**.
|
||||
|
||||
**NOT RESOLVED.** The math is verified but the production path is not built.
|
||||
Resolution criteria (all required for NIST/consensus):
|
||||
- [x] `AlgebraicAggregate*` disabled in production builds (hard gate).
|
||||
- [x] Hint derived only via public `FindHintToTarget(w', w1)` (FIPS `UseHint`).
|
||||
- [x] No production code computes `c·s2`/`c·t0`/`r0`/`LowBits(residual)`.
|
||||
- [x] Boundary predicate proves the hidden `r0` bound; ML-DSA-65 scope enforced.
|
||||
- [ ] `CS2`/`CT0` and all hint-secret wire fields **deleted** from production messages (reflection test).
|
||||
- [ ] **Full `w` never public / reconstructible** (PULSAR-V13-W-LEAK) — needs the ZK clearance proof.
|
||||
- [ ] Partial-`z` correctness proof (PULSAR-V13-PARTIAL-Z-PROOF).
|
||||
- [ ] Canonical, non-grindable nonce selection.
|
||||
- [ ] DKG never reconstructs the master key / `t0`; certifies the `t0` bound.
|
||||
- [ ] Rejected attempts simulatable, not publicly leaked; coarse abort classes.
|
||||
- [ ] Tree aggregation (z-sums + bitmaps + proof roots) for ~1000 signers.
|
||||
- [ ] Two-certificate consensus artifact (ML-DSA sig + signer bitmap/transcript root).
|
||||
- [ ] Final sigs verify under ≥2 independent FIPS 204 verifiers on the BCC path.
|
||||
- [ ] External cryptographic review of the no-MPC leaderless instantiation.
|
||||
|
||||
### PULSAR-V13-W-LEAK (CRITICAL — replacement-design hazard)
|
||||
|
||||
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
|
||||
public, so anyone with full `w` computes `w' − w = c·t0 − c·s2 = Δ` — the
|
||||
same challenge-multiplied long-term-secret residual as PULSAR-V13-HINT-LEAK,
|
||||
in a different form. Production may publish only `w1 = HighBits(w)`, a
|
||||
commitment to `w`, and a **zero-knowledge boundary-clearance proof** (that a
|
||||
hidden `w = A·y` is boundary-clear), never full `w`, `w_i` shares that
|
||||
reconstruct it, `LowBits(w)`, or `w' − w`. The current `BoundaryClear(w)`
|
||||
Go predicate and `spec` are **debug-oracle/prototype**: production needs the
|
||||
ZK proof machinery, which does not yet exist ⇒ the BCC/CEF signing path is
|
||||
**prototype, not production**, even though the arithmetic tests pass.
|
||||
|
||||
### PULSAR-V13-PARTIAL-Z-PROOF (HIGH — consensus robustness)
|
||||
|
||||
BCC/CEF removes the hint-path leakage, but leaderless consensus also needs
|
||||
proof-carrying `z`-partials: each signer proves `z_i = λ_i·y_i + c·λ_i·s_{1,i}`
|
||||
bound to `(session_id, nonce_id, party_id, DKG share commitment, nonce
|
||||
commitment)` without revealing `y_i`/`s_{1,i}`. Otherwise one bad partial
|
||||
fails the aggregate with no clean blame path (leaderless DoS). Verify
|
||||
partials **without** `c·s2_i`/`c·t0_i`/`r0_i`/hint shares (those fields must
|
||||
not exist).
|
||||
|
||||
## Forward-looking (v1.2)
|
||||
|
||||
|
||||
@@ -0,0 +1,167 @@
|
||||
package pulsar
|
||||
|
||||
import "errors"
|
||||
|
||||
// Boundary-Cleared / Carry-Elimination threshold ML-DSA (Pulsar-BCC/CEF).
|
||||
//
|
||||
// No-MPC / no-TEE hint path replacing the leaking AlgebraicAggregate
|
||||
// reconstruction (BLOCKERS.md PULSAR-V13-HINT-LEAK,
|
||||
// spec/threshold-mldsa-boundary-clearance.tex).
|
||||
//
|
||||
// CONFORMANCE RULE (central invariant): the final hint h is determined by
|
||||
// public nonce-region certificates and the public challenge — NEVER by
|
||||
// reconstructing the secret residual. Nothing here forms c·s2, c·t0, r0,
|
||||
// or LowBits(w + Δ). The hint is derived from the public reconstructed
|
||||
// w' = A·z − c·t1·2^d and the public target w1 strictly via the FIPS 204
|
||||
// UseHint primitive (no informal "±1 corrector").
|
||||
|
||||
var (
|
||||
// ErrUnsafeThresholdV03HintPath gates the disabled, leaking
|
||||
// AlgebraicAggregate path (PULSAR-V13-HINT-LEAK).
|
||||
ErrUnsafeThresholdV03HintPath = errors.New(
|
||||
"pulsar: threshold_v03 AlgebraicAggregate path is disabled " +
|
||||
"(PULSAR-V13-HINT-LEAK: broadcasts c*s2/c*t0 hint-path secret " +
|
||||
"material); use the BCC/CEF signing path")
|
||||
|
||||
// ErrBCCParamSet rejects parameter sets outside the proven scope.
|
||||
ErrBCCParamSet = errors.New(
|
||||
"pulsar: Pulsar-BCC/CEF is proven for ML-DSA-65/87 only; this " +
|
||||
"parameter set violates the ||c*t0||_inf < gamma2 bound")
|
||||
|
||||
// ErrNoFIPSHint means no valid FIPS 204 hint reaches the target w1 for
|
||||
// some coefficient (boundary/region violated, or weight > omega).
|
||||
ErrNoFIPSHint = errors.New(
|
||||
"pulsar: no valid FIPS hint reaches target w1 (boundary/region " +
|
||||
"violated); consume the nonce and retry")
|
||||
)
|
||||
|
||||
// bccD is the ML-DSA Power2Round low-bit drop; t0 ∈ [−2^(d−1), 2^(d−1)].
|
||||
const bccD = 13
|
||||
|
||||
// bccParams returns (gamma2, beta = τ·η, omega) for a mode, and ok=false
|
||||
// for any FIPS 204 parameter set outside the proven BCC scope. The scope
|
||||
// condition is ‖c·t0‖∞ ≤ τ·2^(d−1) < γ2: it makes the FIPS c·t0 check
|
||||
// vacuous and bounds the carry to ±1 high-bit. It holds for ML-DSA-65
|
||||
// (49·4096 < 261888) and ML-DSA-87 (60·4096 < 261888) but NOT ML-DSA-44
|
||||
// (39·4096 > 95232). Callers MUST gate on ok before signing.
|
||||
func bccParams(mode Mode) (gamma2, beta, omega uint32, ok bool) {
|
||||
tau, om, _, g2 := modeTauOmega(mode)
|
||||
_, _, eta := modeShape(mode)
|
||||
if uint32(tau)*(1<<(bccD-1)) >= g2 {
|
||||
return 0, 0, 0, false
|
||||
}
|
||||
return g2, uint32(tau) * eta, uint32(om), true
|
||||
}
|
||||
|
||||
// boundaryThreshold is the centered-low-bits magnitude below which a
|
||||
// coefficient is boundary-clear: |a0_centered(w_j)| < γ2 − 2β. The 2β
|
||||
// margin covers BOTH the HighBits boundary (the ±β shift c·s2 cannot
|
||||
// change HighBits) AND the FIPS r0 rejection edge (‖LowBits(w − c·s2)‖∞ <
|
||||
// γ2 − β stays in range) — high-bit stability alone is insufficient.
|
||||
func boundaryThreshold(gamma2 uint32, beta uint32) uint32 { return gamma2 - 2*beta }
|
||||
|
||||
// centeredLowBits returns the FIPS Decompose low part of a, centered into
|
||||
// (−γ2, γ2]. a must be normalized to [0, q).
|
||||
func centeredLowBits(a uint32, gamma2 uint32) int32 {
|
||||
a0plusQ, _ := decompose(a, gamma2)
|
||||
a0 := int32(a0plusQ)
|
||||
if a0plusQ > (mldsaQ-1)/2 {
|
||||
a0 -= mldsaQ
|
||||
}
|
||||
return a0
|
||||
}
|
||||
|
||||
// highBitsCoeff returns the FIPS Decompose high part a1 of a.
|
||||
func highBitsCoeff(a uint32, gamma2 uint32) uint32 {
|
||||
_, a1 := decompose(a, gamma2)
|
||||
return a1
|
||||
}
|
||||
|
||||
// boundaryClearCoeff reports whether coefficient a is far enough from
|
||||
// every HighBits boundary that a hidden ±β shift cannot move its high bits
|
||||
// and its hidden r0 stays in FIPS range.
|
||||
func boundaryClearCoeff(a uint32, gamma2 uint32, beta uint32) bool {
|
||||
a0 := centeredLowBits(a, gamma2)
|
||||
if a0 < 0 {
|
||||
a0 = -a0
|
||||
}
|
||||
return uint32(a0) < boundaryThreshold(gamma2, beta)
|
||||
}
|
||||
|
||||
// BoundaryClear is the offline, message-independent, fully-public nonce-
|
||||
// certification predicate: every coefficient of the public commitment w is
|
||||
// boundary-clear for the c·s2 perturbation. A surviving nonce guarantees
|
||||
// HighBits(w − c·s2) = HighBits(w) = w1 and the FIPS r0-norm check for
|
||||
// every valid challenge — without ever computing c·s2.
|
||||
func BoundaryClear(w polyVec, gamma2 uint32, beta uint32) bool {
|
||||
for i := range w {
|
||||
for j := 0; j < mldsaN; j++ {
|
||||
if !boundaryClearCoeff(w[i][j], gamma2, beta) {
|
||||
return false
|
||||
}
|
||||
}
|
||||
}
|
||||
return true
|
||||
}
|
||||
|
||||
// highBitsVec returns HighBits(w) coefficient-wise. w must be normalized.
|
||||
func highBitsVec(w polyVec, gamma2 uint32) polyVec {
|
||||
out := make(polyVec, len(w))
|
||||
for i := range w {
|
||||
for j := 0; j < mldsaN; j++ {
|
||||
out[i][j] = highBitsCoeff(w[i][j], gamma2)
|
||||
}
|
||||
}
|
||||
return out
|
||||
}
|
||||
|
||||
// useHint applies one FIPS 204 (Algorithm 40) hint bit to coefficient r,
|
||||
// returning the corrected high part r1. m = (q−1)/(2γ2) high-bit buckets.
|
||||
// r must be normalized to [0, q).
|
||||
func useHint(hbit, r, gamma2 uint32) uint32 {
|
||||
m := uint32((mldsaQ - 1) / (2 * gamma2))
|
||||
r0plusQ, r1 := decompose(r, gamma2)
|
||||
if hbit == 0 {
|
||||
return r1
|
||||
}
|
||||
r0 := int32(r0plusQ)
|
||||
if r0plusQ > (mldsaQ-1)/2 {
|
||||
r0 -= mldsaQ
|
||||
}
|
||||
if r0 > 0 {
|
||||
return (r1 + 1) % m
|
||||
}
|
||||
return (r1 + m - 1) % m
|
||||
}
|
||||
|
||||
// findHintToTarget derives the ML-DSA hint from PUBLIC data only — the
|
||||
// public reconstructed wPrime = A·z − c·t1·2^d and the public target w1 =
|
||||
// HighBits(w). It NEVER forms c·s2, c·t0, or r0. The hint bit is not a
|
||||
// signed correction: a coefficient takes h_j = 0 when HighBits already
|
||||
// matches, h_j = 1 iff UseHint(1, ·) reaches the target, else there is no
|
||||
// valid FIPS hint (boundary/region violated) and signing must consume the
|
||||
// nonce and retry. Returns the hint and ok; ok=false ⇒ ErrNoFIPSHint.
|
||||
//
|
||||
// Theorem: findHintToTarget(wPrime, w1) = (h, true) iff
|
||||
// UseHint(h, wPrime) = w1 and weight(h) ≤ omega.
|
||||
func findHintToTarget(wPrime, targetW1 polyVec, gamma2, omega uint32) (polyVec, bool) {
|
||||
h := make(polyVec, len(wPrime))
|
||||
var weight uint32
|
||||
for i := range wPrime {
|
||||
for j := 0; j < mldsaN; j++ {
|
||||
switch {
|
||||
case highBitsCoeff(wPrime[i][j], gamma2) == targetW1[i][j]:
|
||||
h[i][j] = 0
|
||||
case useHint(1, wPrime[i][j], gamma2) == targetW1[i][j]:
|
||||
h[i][j] = 1
|
||||
weight++
|
||||
default:
|
||||
return nil, false // no valid FIPS hint for this coefficient
|
||||
}
|
||||
}
|
||||
}
|
||||
if weight > omega {
|
||||
return nil, false
|
||||
}
|
||||
return h, true
|
||||
}
|
||||
@@ -0,0 +1,186 @@
|
||||
package pulsar
|
||||
|
||||
import (
|
||||
"math/rand"
|
||||
"testing"
|
||||
)
|
||||
|
||||
// These are DEBUG-ORACLE tests: they reconstruct the hidden commitment w
|
||||
// directly to verify the BCC/CEF arithmetic, lemmas, and yield. Production
|
||||
// code must NOT compute or publish full w (PULSAR-V13-W-LEAK); it publishes
|
||||
// only w1, a commitment to w, and a ZK boundary-clearance proof.
|
||||
|
||||
func randPolyVec(rng *rand.Rand, k int) polyVec {
|
||||
w := make(polyVec, k)
|
||||
for i := 0; i < k; i++ {
|
||||
for j := 0; j < mldsaN; j++ {
|
||||
w[i][j] = uint32(rng.Int63n(mldsaQ))
|
||||
}
|
||||
}
|
||||
return w
|
||||
}
|
||||
|
||||
func subMod(a uint32, delta int32) uint32 {
|
||||
v := (int64(a) - int64(delta)) % mldsaQ
|
||||
if v < 0 {
|
||||
v += mldsaQ
|
||||
}
|
||||
return uint32(v)
|
||||
}
|
||||
|
||||
// The leaking AlgebraicAggregate path must be disabled by default
|
||||
// (PULSAR-V13-HINT-LEAK), independent of any other signer state.
|
||||
func TestThresholdV03DisabledByDefault(t *testing.T) {
|
||||
s := &AlgebraicThresholdSigner{}
|
||||
if _, _, err := s.Round2Sign(nil, nil); err != ErrUnsafeThresholdV03HintPath {
|
||||
t.Fatalf("threshold_v03 must fail closed by default; got err=%v", err)
|
||||
}
|
||||
}
|
||||
|
||||
// BCC/CEF is proven only where ||c·t0||_inf < gamma2 (ML-DSA-65/87, not 44).
|
||||
func TestBCCParamGuard(t *testing.T) {
|
||||
for _, m := range []Mode{ModeP65, ModeP87} {
|
||||
if _, _, _, ok := bccParams(m); !ok {
|
||||
t.Fatalf("mode %d must be in BCC scope", m)
|
||||
}
|
||||
}
|
||||
if _, _, _, ok := bccParams(ModeP44); ok {
|
||||
t.Fatalf("ML-DSA-44 must be rejected (tau*2^(d-1) >= gamma2)")
|
||||
}
|
||||
// Sanity on the c·t0 bound itself.
|
||||
for _, m := range []Mode{ModeP65, ModeP87} {
|
||||
tau, _, _, g2 := modeTauOmega(m)
|
||||
if uint32(tau)*(1<<(bccD-1)) >= g2 {
|
||||
t.Fatalf("mode %d: c·t0 bound should be vacuous", m)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Theorem: findHintToTarget(w', target) = (h, true) implies
|
||||
// UseHint(h, w') = target coefficient-wise. The hint bit is validated via
|
||||
// FIPS UseHint, never an informal ±1 corrector.
|
||||
func TestFindHintToTargetMatchesUseHint(t *testing.T) {
|
||||
gamma2, _, omega, _ := bccParams(ModeP65)
|
||||
k, _, _ := modeShape(ModeP65)
|
||||
rng := rand.New(rand.NewSource(2))
|
||||
checked := 0
|
||||
for iter := 0; iter < 3000; iter++ {
|
||||
wPrime := randPolyVec(rng, k)
|
||||
// Build a reachable, omega-sparse target like a real ML-DSA hint:
|
||||
// baseline all h=0 (HighBits), then flip up to omega coefficients to
|
||||
// the h=1 result.
|
||||
target := highBitsVec(wPrime, gamma2)
|
||||
nflip := rng.Intn(int(omega) + 1)
|
||||
for f := 0; f < nflip; f++ {
|
||||
i := rng.Intn(k)
|
||||
j := rng.Intn(mldsaN)
|
||||
target[i][j] = useHint(1, wPrime[i][j], gamma2)
|
||||
}
|
||||
h, ok := findHintToTarget(wPrime, target, gamma2, omega)
|
||||
if !ok {
|
||||
continue // weight > omega for random targets; skip
|
||||
}
|
||||
checked++
|
||||
for i := 0; i < k; i++ {
|
||||
for j := 0; j < mldsaN; j++ {
|
||||
if useHint(h[i][j], wPrime[i][j], gamma2) != target[i][j] {
|
||||
t.Fatalf("UseHint(h,w') != target at [%d][%d]", i, j)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
if checked == 0 {
|
||||
t.Fatal("no reachable targets exercised")
|
||||
}
|
||||
t.Logf("verified UseHint(findHintToTarget(w',t),w')==t on %d vectors", checked)
|
||||
}
|
||||
|
||||
// Core BCC+ lemma (debug oracle): a boundary-clear w keeps HighBits stable
|
||||
// under every hidden ||c·s2||_inf <= beta shift, and the hidden r0 stays in
|
||||
// the FIPS rejection range — without the protocol ever forming c·s2 or r0.
|
||||
func TestBoundaryClearImpliesHighBitsStable(t *testing.T) {
|
||||
gamma2, beta, _, ok := bccParams(ModeP65)
|
||||
if !ok {
|
||||
t.Fatal("P65 params")
|
||||
}
|
||||
k, _, _ := modeShape(ModeP65)
|
||||
rng := rand.New(rand.NewSource(1))
|
||||
cleared := 0
|
||||
for iter := 0; iter < 4000; iter++ {
|
||||
w := randPolyVec(rng, k)
|
||||
if !BoundaryClear(w, gamma2, beta) {
|
||||
continue
|
||||
}
|
||||
cleared++
|
||||
hb0 := highBitsVec(w, gamma2)
|
||||
for i := 0; i < k; i++ {
|
||||
for j := 0; j < mldsaN; j++ {
|
||||
delta := int32(rng.Intn(int(2*beta+1))) - int32(beta) // [-beta, beta]
|
||||
shifted := subMod(w[i][j], delta)
|
||||
if highBitsCoeff(shifted, gamma2) != hb0[i][j] {
|
||||
t.Fatalf("HighBits moved under |c·s2|<=beta on boundary-clear w [%d][%d]", i, j)
|
||||
}
|
||||
r0 := centeredLowBits(shifted, gamma2)
|
||||
if r0 < 0 {
|
||||
r0 = -r0
|
||||
}
|
||||
if uint32(r0) >= gamma2-beta {
|
||||
t.Fatalf("hidden r0 bound violated on boundary-clear w [%d][%d]", i, j)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
if cleared == 0 {
|
||||
t.Fatal("no boundary-clear nonces sampled")
|
||||
}
|
||||
t.Logf("verified HighBits-stable + r0-bound on %d boundary-clear nonces", cleared)
|
||||
}
|
||||
|
||||
// Exact off-by-one audit of the 2β margin against FIPS Decompose.
|
||||
func TestBoundaryClearEdgeCases(t *testing.T) {
|
||||
gamma2, beta, _, _ := bccParams(ModeP65)
|
||||
thr := int32(boundaryThreshold(gamma2, beta)) // gamma2 - 2*beta
|
||||
mk := func(a0 int32) uint32 { // coefficient with centered low bits a0 in bucket 1
|
||||
v := (int64(2*gamma2) + int64(a0)) % mldsaQ
|
||||
if v < 0 {
|
||||
v += mldsaQ
|
||||
}
|
||||
return uint32(v)
|
||||
}
|
||||
cases := []struct {
|
||||
a0 int32
|
||||
want bool
|
||||
}{
|
||||
{thr - 1, true}, {thr, false}, {thr + 1, false},
|
||||
{-(thr - 1), true}, {-thr, false}, {-(thr + 1), false},
|
||||
{0, true},
|
||||
}
|
||||
for _, c := range cases {
|
||||
a := mk(c.a0)
|
||||
if got := centeredLowBits(a, gamma2); got != c.a0 {
|
||||
t.Fatalf("centeredLowBits(mk(%d))=%d", c.a0, got)
|
||||
}
|
||||
if got := boundaryClearCoeff(a, gamma2, beta); got != c.want {
|
||||
t.Fatalf("boundaryClearCoeff(a0=%d)=%v want %v (thr=%d)", c.a0, got, c.want, thr)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Measure the real offline boundary-clearance yield for ML-DSA-65.
|
||||
func TestBoundaryClearanceYield(t *testing.T) {
|
||||
gamma2, beta, _, _ := bccParams(ModeP65)
|
||||
k, _, _ := modeShape(ModeP65)
|
||||
rng := rand.New(rand.NewSource(3))
|
||||
const trials = 3000
|
||||
clear := 0
|
||||
for i := 0; i < trials; i++ {
|
||||
if BoundaryClear(randPolyVec(rng, k), gamma2, beta) {
|
||||
clear++
|
||||
}
|
||||
}
|
||||
yield := float64(clear) / trials
|
||||
t.Logf("ML-DSA-65 boundary-clear yield (margin 2β=%d, γ2=%d): %.4f", 2*beta, gamma2, yield)
|
||||
if yield < 0.03 || yield > 0.25 {
|
||||
t.Fatalf("yield %.4f outside expected ~0.10 band", yield)
|
||||
}
|
||||
}
|
||||
@@ -439,6 +439,12 @@ type AlgebraicThresholdSigner struct {
|
||||
NodeID NodeID
|
||||
Share *AlgebraicKeyShare
|
||||
|
||||
// AllowUnsafeThresholdV03ForTests opts INTO the disabled, leaking
|
||||
// AlgebraicAggregate hint path (PULSAR-V13-HINT-LEAK). Default false ⇒
|
||||
// Round2Sign fails closed with ErrUnsafeThresholdV03HintPath. Set only
|
||||
// in tests exercising the legacy vector; NEVER in production.
|
||||
AllowUnsafeThresholdV03ForTests bool
|
||||
|
||||
SessionID [16]byte
|
||||
Attempt uint32
|
||||
|
||||
@@ -754,15 +760,25 @@ func (s *AlgebraicThresholdSigner) Round2W(round1 []*AlgebraicRound1Message) (*A
|
||||
// (This party's own w_i is taken from local state — do not include it
|
||||
// in peerW.)
|
||||
//
|
||||
// PUBLIC-BFT-SAFETY NOTE: this party's contribution (z_i, cs2_i, ct0_i)
|
||||
// is INFORMATION-THEORETICALLY (t-1)-secret about its share material —
|
||||
// the per-party arithmetic is z_i = y_i + c·λ_i·s_{1,i} where y_i is
|
||||
// fresh randomness from this party's RNG and c is a public challenge.
|
||||
// An adversary that obtains t-1 such contributions cannot recover any
|
||||
// single party's s_{1,i} because the y_i mask hides it (each y_i is
|
||||
// drawn from the FIPS 204 (-γ_1', γ_1'] uniform distribution, which
|
||||
// is sufficient to mask under the M-LWE assumption).
|
||||
// ⚠️ SECURITY-CRITICAL — PULSAR-V13-HINT-LEAK (see BLOCKERS.md).
|
||||
// The y_i mask hides s_{1,i} in z_i = y_i + c·λ_i·s_{1,i} (correct). But
|
||||
// the cs2_i = c·λ_i·s_{2,i} and ct0_i = c·λ_i·t_{0,i} fields emitted by
|
||||
// round2EmitFull below carry NO mask. Since c and λ_i are public,
|
||||
// s_{2,i} = (c·λ_i)^{-1}·cs2_i is recoverable; and the aggregate
|
||||
// Σ cs2_i = c·s2_master (likewise ct0_i → t0) leaks long-term ML-DSA
|
||||
// secret-key material over varying-c sessions plus the secret relation
|
||||
// A·s1 = (t1·2^d + t0) − s2 — breaking threshold secrecy and transcript
|
||||
// simulation. The prior claim that (z_i, cs2_i, ct0_i) are
|
||||
// (t-1)-secret was FALSE — it only held for z_i. This path is being
|
||||
// replaced by boundary-cleared nonces + carry elimination
|
||||
// (spec/threshold-mldsa-boundary-clearance.tex), which never forms
|
||||
// c·s2/c·t0/r0. Do NOT rely on this path for production secrecy.
|
||||
func (s *AlgebraicThresholdSigner) Round2Sign(round1 []*AlgebraicRound1Message, peerW map[NodeID]polyVec) (*AlgebraicRound2Message, *AbortEvidence, error) {
|
||||
// PULSAR-V13-HINT-LEAK: this path broadcasts c*s2/c*t0 hint-path secret
|
||||
// material; fail closed in production. Opt in only for legacy tests.
|
||||
if !s.AllowUnsafeThresholdV03ForTests {
|
||||
return nil, nil, ErrUnsafeThresholdV03HintPath
|
||||
}
|
||||
return s.round2EmitFull(round1, peerW)
|
||||
}
|
||||
|
||||
|
||||
@@ -0,0 +1,250 @@
|
||||
\documentclass[11pt]{article}
|
||||
\usepackage{amsmath,amssymb,amsthm}
|
||||
\usepackage[margin=1in]{geometry}
|
||||
\newtheorem{lemma}{Lemma}
|
||||
\newtheorem{theorem}{Theorem}
|
||||
\newtheorem{definition}{Definition}
|
||||
\theoremstyle{remark}\newtheorem{remark}{Remark}
|
||||
\title{Pulsar Threshold ML-DSA via Boundary-Cleared Nonces and Carry
|
||||
Elimination\\(No MPC, No TEE) --- BCC0 / BCC+}
|
||||
\author{Lux Core Team --- \texttt{github.com/luxfi/pulsar}}
|
||||
\date{}
|
||||
\begin{document}
|
||||
\maketitle
|
||||
|
||||
\section{The leak this replaces}
|
||||
The v0.3/v0.4 \texttt{AlgebraicAggregate} path reconstructs $c\,\mathbf
|
||||
s_2^{\mathrm{joint}}$ and $c\,\mathbf t_0^{\mathrm{joint}}$ at the
|
||||
aggregator to form the FIPS hint. But $\mathbf s_2^{\mathrm{joint}}$ is
|
||||
the master $\mathbf s_2$ (Shamir reconstruction) and $c$ is public and
|
||||
varies per session, so revealing $c\,\mathbf s_2^{\mathrm{joint}}$ over
|
||||
sessions is a linear system in the fixed $\mathbf s_2$ --- one invertible
|
||||
$c$ recovers it; then $A\mathbf s_1 = \mathbf t - \mathbf s_2$ recovers
|
||||
$\mathbf s_1$, a total key break. In the leaderless model every quorum
|
||||
member aggregates, so every corrupt validator learns it. \textbf{Masking
|
||||
the per-party shares does not help: the masks cancel in the aggregate the
|
||||
protocol must reconstruct.} The cure is never to form the secret residual.
|
||||
|
||||
\section{The invariant and the whole game}
|
||||
With $\mathbf w = A\mathbf y$, $\mathbf z = \mathbf y + c\,\mathbf s_1$,
|
||||
$\mathbf t = A\mathbf s_1 + \mathbf s_2 = \mathbf t_1 2^d + \mathbf t_0$,
|
||||
the verifier recomputes
|
||||
\[
|
||||
\mathbf w' \;=\; A\mathbf z - c\,\mathbf t_1 2^d
|
||||
\;=\; \mathbf w + c\,\mathbf t_0 - c\,\mathbf s_2
|
||||
\;=\; \mathbf w + \Delta, \qquad \Delta := c\,\mathbf t_0 - c\,\mathbf
|
||||
s_2,
|
||||
\]
|
||||
and accepts iff $\mathrm{UseHint}(\mathbf h, \mathbf w') = \mathbf w_1$
|
||||
where $\mathbf w_1 = \mathrm{HighBits}(\mathbf w)$ fixed $c = H(\mu \| \mathbf
|
||||
w_1)$.
|
||||
\begin{theorem}[No-leak target]
|
||||
Produce a public $\mathbf h$ with $\mathrm{UseHint}(\mathbf h, \mathbf w +
|
||||
\Delta) = \mathrm{HighBits}(\mathbf w)$ \emph{without} revealing $\Delta$,
|
||||
$\mathrm{LowBits}(\mathbf w + \Delta)$, $c\,\mathbf s_2$, $c\,\mathbf
|
||||
t_0$, or $r_0$.
|
||||
\end{theorem}
|
||||
|
||||
\section{Conformance rule (central invariant)}
|
||||
\label{sec:rule}
|
||||
\textbf{The final hint $\mathbf h$ must be determined by public
|
||||
nonce-region certificates and the public challenge --- never by
|
||||
reconstructing the secret residual.} For BCC0 the certificate guarantees
|
||||
$\mathbf h = 0$; for BCC+ it guarantees a publicly-determined hint
|
||||
pattern. \emph{Any implementation that computes $\mathbf h$ by first
|
||||
forming $c\,\mathbf s_2$, $c\,\mathbf t_0$, $r_0$, or
|
||||
$\mathrm{LowBits}(\mathbf w + \Delta)$ is non-conformant.} Note $\mathbf
|
||||
w' = A\mathbf z - c\,\mathbf t_1 2^d$ is itself \emph{public} (computable
|
||||
by the verifier from $A,\mathbf z,c,\mathbf t_1$); reading $\mathbf h$ off
|
||||
$(\mathbf w', \mathbf w_1)$ reveals only $\mathbf h$, which is in the
|
||||
signature anyway --- it is \emph{not} residual reconstruction.
|
||||
|
||||
\subsection{Full $\mathbf w$ must be hidden (PULSAR-V13-W-LEAK)}
|
||||
The full commitment $\mathbf w = A\mathbf y$ must \emph{never} be public or
|
||||
reconstructible by a $t-1$ coalition. Since $\mathbf w' = A\mathbf z -
|
||||
c\,\mathbf t_1 2^d$ becomes public once $\mathbf z$ is assembled, anyone
|
||||
holding full $\mathbf w$ computes $\mathbf w' - \mathbf w = c\,\mathbf t_0
|
||||
- c\,\mathbf s_2 = \Delta$ --- the same long-term-secret residual as the
|
||||
original leak. \textbf{Public:} $\mathbf w_1$, a commitment to $\mathbf w$,
|
||||
a \emph{zero-knowledge} boundary-clearance proof, and the final $(\mathbf
|
||||
z,\mathbf h,\text{sig})$. \textbf{Forbidden:} full $\mathbf w$, $\mathbf
|
||||
w_i$ shares reconstructing it, $\mathrm{LowBits}(\mathbf w)$, $\mathbf w' -
|
||||
\mathbf w$. Hence $\textsc{BoundaryClear}(\mathbf w)$ on \emph{public}
|
||||
$\mathbf w$ is \textbf{debug-oracle only}; production replaces it with a ZK
|
||||
proof that a hidden $\mathbf w = A\mathbf y$ satisfies the predicate,
|
||||
revealing none of $\mathbf w$, $\mathrm{LowBits}(\mathbf w)$, or per-
|
||||
coefficient distances. \textbf{Until that ZK machinery exists the BCC/CEF
|
||||
signing path is prototype, not production.}
|
||||
|
||||
\section{Profiles}
|
||||
\subsection{BCC0 --- conservative $\mathbf h = 0$}
|
||||
Use only nonces whose hidden shift cannot move any coefficient across a
|
||||
high-bit boundary: $\mathrm{HighBits}(\mathbf w + \Delta) =
|
||||
\mathrm{HighBits}(\mathbf w)$, so $\mathbf h = 0$.
|
||||
\begin{lemma}[BCC0 stability]\label{lem:bcc0}
|
||||
$\textsc{BoundaryClear}(\mathbf w, B_\Delta) \wedge \|\Delta\|_\infty \le
|
||||
B_\Delta \;\Rightarrow\; \mathrm{HighBits}(\mathbf w + \Delta) =
|
||||
\mathrm{HighBits}(\mathbf w)$, whence $\mathrm{UseHint}(0, \mathbf w') =
|
||||
\mathbf w_1$ and unmodified FIPS 204 accepts.
|
||||
\end{lemma}
|
||||
\textbf{BCC0 is infeasible for ML-DSA-65} (\S\ref{sec:bounds}): the worst-
|
||||
case $B_\Delta$ exceeds $\gamma_2$, so no coefficient can clear. Retained
|
||||
as a definition / fallback profile only, not used.
|
||||
|
||||
\subsection{BCC+ --- carry elimination, nonzero $\mathbf h$}
|
||||
Allow $\mathbf h \neq 0$, but derive it from public data. The shift splits
|
||||
into a \emph{small} part $-c\,\mathbf s_2$ and a \emph{large} part
|
||||
$c\,\mathbf t_0$. Boundary-clear \emph{only} the small part; the large
|
||||
part is resolved by the public hint.
|
||||
\begin{definition}[Per-coefficient region]
|
||||
For coefficient $w_j$ and margin $B$ (covering $\|c\,\mathbf
|
||||
s_2\|_\infty$), classify by FIPS \texttt{Decompose}:
|
||||
$\textsc{SafeZeroCarry}$ if $\mathrm{dist}(w_j) > B$ and the $c\,\mathbf
|
||||
t_0$ carry cannot cross; $\textsc{SafeKnownCarry}$ if the carry is
|
||||
resolvable to a single public bit from $\mathbf w'$; $\textsc{Unsafe}$
|
||||
otherwise. Accept a nonce iff no coefficient is $\textsc{Unsafe}$.
|
||||
\end{definition}
|
||||
\begin{lemma}[BCC+ correctness]\label{lem:bccplus}
|
||||
If $\textsc{BoundaryClear}(\mathbf w, 2\beta)$ (clears $c\,\mathbf s_2$)
|
||||
and $\|c\,\mathbf t_0\|_\infty < \alpha$ (so each coefficient's high bits
|
||||
move by at most $\pm 1$), then (i) $\mathrm{HighBits}(\mathbf w -
|
||||
c\,\mathbf s_2) = \mathbf w_1$ and $\|\mathrm{LowBits}(\mathbf w -
|
||||
c\,\mathbf s_2)\|_\infty < \gamma_2 - \beta$ (the FIPS $r_1{=}\mathbf
|
||||
w_1$, $r_0$-norm conditions); and (ii) the public hint $h_j := [\,
|
||||
\mathrm{HighBits}(w'_j) \neq w_{1,j}\,]$ equals the FIPS hint
|
||||
$\mathrm{MakeHint}(-c\,\mathbf t_0, \mathbf w - c\,\mathbf s_2)$ and
|
||||
satisfies $\mathrm{UseHint}(\mathbf h, \mathbf w') = \mathbf w_1$.
|
||||
\end{lemma}
|
||||
\emph{Reconciliation with ``region-derived'':} the $c\,\mathbf t_0$ carry
|
||||
depends on the secret $\mathbf t_0$ and the online $c$, so it cannot be
|
||||
fixed fully offline; the \emph{offline} certificate clears $c\,\mathbf
|
||||
s_2$ and bounds the carry to $\pm 1$, and the \emph{online} step reads the
|
||||
carry bit off the public $\mathbf w'$. Both inputs ($\mathbf w'$, $\mathbf
|
||||
w_1$) are public; no residual is formed. This is BCC+ \S2A realised.
|
||||
|
||||
\section{Concrete bounds (ML-DSA-65)}
|
||||
\label{sec:bounds}
|
||||
$q{=}8380417,\ d{=}13,\ \tau{=}49,\ \eta{=}4,\ \gamma_2{=}261888,\
|
||||
\alpha{=}2\gamma_2{=}523776,\ \beta{=}\tau\eta{=}196,\ \omega{=}55$.
|
||||
\begin{itemize}
|
||||
\item $\|c\,\mathbf s_2\|_\infty \le B_{s_2} = \tau\eta = 196$.
|
||||
\item $\|c\,\mathbf t_0\|_\infty \le \tau\,2^{d-1} = 49\cdot4096 = 200704
|
||||
< \gamma_2 < \alpha$: the FIPS $\|c\,\mathbf t_0\|<\gamma_2$ check is
|
||||
\emph{vacuous} (always holds), and the carry moves $\mathrm{HighBits}$
|
||||
by at most $\pm1$ per coefficient. No check, no reconstruction.
|
||||
\item \textbf{BCC0 infeasible:} needs clearance $> B_\Delta = B_{s_2} +
|
||||
\tau\,2^{d-1} \approx 401555 > \gamma_2 = 261888$ (max possible
|
||||
clearance). Yield $0$.
|
||||
\item \textbf{BCC+ feasible:} clear only $c\,\mathbf s_2$ with margin $B =
|
||||
2\beta = 392$ (covers the $\mathrm{HighBits}$ boundary and the $r_0 <
|
||||
\gamma_2-\beta$ edge). Per-coefficient clear prob $\approx 1 -
|
||||
B/\gamma_2 = 0.9985$; all-$256{\cdot}6$ yield $\approx 0.10$ (measure;
|
||||
raise margin only, never lower). $c\,\mathbf t_0$ contributes the
|
||||
nonzero, $\omega$-sparse public hint.
|
||||
\end{itemize}
|
||||
|
||||
\section{Proof obligations}
|
||||
\paragraph{BCC0 chain (Lemma~\ref{lem:bcc0}).} $\mathbf w{=}A\mathbf y$;
|
||||
$\mathbf z{=}\mathbf y{+}c\mathbf s_1$; $A\mathbf z{-}c\mathbf t_1 2^d
|
||||
{=}\mathbf w{+}\Delta$; $\|\Delta\|_\infty\le B_\Delta$;
|
||||
$\textsc{BoundaryClear}(\mathbf w,B_\Delta)$ $\Rightarrow$
|
||||
$\mathrm{HighBits}(\mathbf w{+}\Delta){=}\mathbf w_1$ $\Rightarrow$
|
||||
$\mathrm{UseHint}(0,\cdot){=}\mathbf w_1$ $\Rightarrow$ accept.
|
||||
\paragraph{BCC+ / CEF chain (Lemma~\ref{lem:bccplus}).} as above with the
|
||||
public hint; $h$ region/public-$\mathbf w'$-derived; for all $\Delta$ with
|
||||
$\|\Delta\|_\infty\le B_\Delta$, $\mathrm{UseHint}(\mathbf h,\mathbf w{+}
|
||||
\Delta){=}\mathbf w_1$.
|
||||
\paragraph{Soundness.} A malicious signer's bad $\mathbf z_i$ yields a
|
||||
wrong $\mathbf w'$ and a wrong $\mathbf h$ $\Rightarrow$ the mandatory
|
||||
final unmodified-FIPS verify \emph{fails} (identifiable abort via the
|
||||
per-party $\mathbf z_i$ proof/MAC). \textbf{Never fall back to forming
|
||||
$c\,\mathbf s_2$/$c\,\mathbf t_0$/$r_0$.}
|
||||
\paragraph{Transcript privacy / simulatability.} The transcript holds
|
||||
$\{\mathbf w,\mathbf w_1,c,\mathbf z,\mathbf h,\text{commitments},
|
||||
\text{proofs}\}$ and \emph{not} $c\,\mathbf s_{2,i}$, $c\,\mathbf
|
||||
t_{0,i}$, $c\,\mathbf s_2^{\mathrm{joint}}$, $c\,\mathbf
|
||||
t_0^{\mathrm{joint}}$, $\Delta$, $r_0$, $\mathrm{LowBits}(\mathbf
|
||||
w{+}\Delta)$. A simulator reproduces it from $(pk, m, \text{final sig},
|
||||
\text{signer bitmap}, \text{corrupt shares})$ without honest shares.
|
||||
\paragraph{Conditioned-nonce security (hardest).} Conditioning the pool on
|
||||
the public predicate $\textsc{BoundaryClear}(\mathbf w, 2\beta)$ (resp.\
|
||||
$\textsc{AllRegionsSafe}$) must not weaken EUF-CMA: $\mathbf w = A\mathbf
|
||||
y$ is independent of the key, and the surviving $\mathbf y$ distribution
|
||||
must remain a valid rejection-sampled nonce distribution (or the signature
|
||||
distribution must remain simulatable). \emph{This is a required proof, not
|
||||
an assumption; if \textsc{2B nonce shaping} is used, the distribution
|
||||
proof is mandatory before deployment.}
|
||||
|
||||
\section{Wire format (deletion audit)}
|
||||
\textbf{Remove} \texttt{CS2}, \texttt{CT0} (and any \texttt{cs2},
|
||||
\texttt{ct0}, \texttt{D2}, \texttt{D0}, \texttt{R0Share},
|
||||
\texttt{LowBitsShare}, \texttt{HintInput}, \texttt{HintShare}) from the
|
||||
Round-2 message and the $\tau_2$ transcript. Old fields fail
|
||||
deserialization outside an explicit legacy-test parser.
|
||||
\begin{verbatim}
|
||||
type BoundaryNonceCert struct {
|
||||
NonceID [32]byte; PKEpoch uint64; CommitteeID [32]byte
|
||||
SignerSetRoot [32]byte; W1 PackedHighBits; WCommitment []byte
|
||||
ClearanceProof []byte; Margin uint32; CommitRoot [32]byte; Consumed bool }
|
||||
// NO full W field (PULSAR-V13-W-LEAK); W is debug-oracle only.
|
||||
type ZPartial struct {
|
||||
PartyID PartyID; NonceID [32]byte; SessionID [32]byte
|
||||
ZShare PackedPolyVecL; Proof []byte; MAC []byte }
|
||||
type PulsarSignature struct { C PackedChallenge; Z PackedPolyVecL; H PackedHint }
|
||||
\end{verbatim}
|
||||
No \texttt{CS2/CT0/D2/D0/R0Share/LowBitsShare/HintInput/HintShare}.
|
||||
|
||||
\section{Protocol}
|
||||
\paragraph{Offline (message-independent) nonce pool.} Sample $\mathbf
|
||||
y_i$; commit. The aggregate $\mathbf w = \sum\lambda_i\mathbf w_i$ is
|
||||
\emph{hidden}: in production each signer proves in zero knowledge that the
|
||||
hidden $\mathbf w$ is boundary-clear, publishing only $\mathbf w_1$, a
|
||||
commitment to $\mathbf w$, and the clearance proof (PULSAR-V13-W-LEAK; the
|
||||
debug oracle may form $\mathbf w$ to classify regions vs $B$). If
|
||||
\textsc{AllRegionsSafe}, store the cert ($\mathbf w_1,\text{WCommitment},
|
||||
\text{ClearanceProof},\text{CommitRoot}$); else discard. Run continuously off
|
||||
the consensus path.
|
||||
\paragraph{Online sign.} Pick an unused cert; $\mu = H(pk\|ctx\|m)$, $c =
|
||||
H(\mu\|\mathbf w_1)$; collect $\mathbf z_i = \lambda_i\mathbf y_i +
|
||||
c\lambda_i\mathbf s_{1,i}$; $\mathbf z = \sum\mathbf z_i$; reject to a
|
||||
fresh nonce if $\|\mathbf z\|_\infty \ge \gamma_1-\beta$; compute public
|
||||
$\mathbf w' = A\mathbf z - c\mathbf t_1 2^d$ and $\mathbf h$ (BCC0:
|
||||
$\mathbf 0$; BCC+: $h_j=[\mathrm{HighBits}(w'_j)\neq w_{1,j}]$); reject if
|
||||
$\mathrm{wt}(\mathbf h) > \omega$; emit $\textsc{sigEncode}(\tilde
|
||||
c,\mathbf z,\mathbf h)$; assert unmodified FIPS 204 verify (failure $=$
|
||||
bug).
|
||||
|
||||
\section{Fallback (Option 3)}
|
||||
If unmodified-FIPS-204-byte-equality is not mandatory, use the
|
||||
Raccoon/Ringtail-style threshold-friendly hint scheme --- this is exactly
|
||||
the \textbf{Corona} route (\texttt{luxfi/corona}, LP-4440): public
|
||||
threshold signature, leaderless, no MPC/TEE, but \emph{not} FIPS-byte-
|
||||
equal.
|
||||
|
||||
\section{Scale / consensus notes}
|
||||
For $\sim$1000+ validators: generate boundary-safe nonce certs
|
||||
continuously offline; online consensus only tree-aggregates $\mathbf z$
|
||||
shares; the final signature is ordinary ML-DSA; the QC carries the signer
|
||||
bitmap $+$ transcript root. Do \emph{not} boundary-filter online per
|
||||
message.
|
||||
|
||||
\section{Practical risks}
|
||||
(1) usable safe-nonce rate; (2) the conditioned-nonce distribution proof;
|
||||
(3) exact FIPS boundary classification (against \texttt{Decompose}, not
|
||||
integer rounding); (4) keeping the margin small enough for yield while
|
||||
covering $c\,\mathbf s_2$. If BCC+ yield is poor, prefer \textsc{2B nonce
|
||||
shaping} (with its distribution proof) over weakening the margin.
|
||||
|
||||
\section{Phased plan + TALUS alignment}
|
||||
\textbf{Phase 1:} BCC+ as above --- this spec, Lemmas~\ref{lem:bcc0},
|
||||
\ref{lem:bccplus} machine-checked (\texttt{Crypto/Pulsar/Boundary\-
|
||||
Clearance.lean}) against the FIPS \texttt{Decompose}/\texttt{HighBits}/
|
||||
\texttt{MakeHint}/\texttt{UseHint} definitions, Go impl reusing the
|
||||
existing \texttt{decompose}/\texttt{power2Round} primitives, the
|
||||
regression / no-residual / distribution / CIRCL$+$pq-crystals interop
|
||||
tests on the BCC path, and the offline-yield measurement.
|
||||
\textbf{Phase 2:} \textsc{2B nonce shaping} if yield demands, with the
|
||||
distribution proof. \textbf{Phase 3:} align terminology and proof
|
||||
obligations with the TALUS boundary-clearance / carry-elimination
|
||||
construction.
|
||||
\end{document}
|
||||
Reference in New Issue
Block a user