luxfi/security
1
0
Fork 0
mirror of https://github.com/luxfi/security.git synced 2026-10-30 15:17:20 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
main
security/releases/2026-06-pq-threshold-stack/CLAIMS.md
T

11 KiB
Raw Permalink Blame History

Claim matrix — Lux PQ Threshold Stack, release 2026-06-pq-threshold-stack

Every claim below is scoped to the exact commits in RELEASE-MANIFEST.toml. Each has an ID, an evidence class, the assumptions it rests on, and a status. A claim is proven only as "proven under stated assumptions". External reviewers sign these IDs (EXTERNAL-REVIEW-SIGNOFF.md).

Evidence classes (see framework/ASSURANCE.tex): machine-checked · sound-by-reduction · interop-tested · asserted-axiom · fail-closed-pending-review · open-research.

Assumption buckets: A standard math fact (discharge/Lean-bridge) · B implementation/spec bridge (KAT + property + independent-impl + small formal wrapper) · C actual security assumption (state explicitly; never "proved"; prove reductions under it). The per-repo AXIOM-INVENTORY.md + .assurance/reviewed-axioms.txt are the authoritative bucketed ledgers.

Pulsar — threshold ML-DSA (FIPS 204)

  • PULSAR-C1 BoundaryClear. |LowBits(w)| < γ2−2β ∧ |δ|≤β ⇒ HighBits(w−δ)=HighBits(w) and hidden r0 stays in range. Class: machine-checked (Lean BoundaryClearance.lean) + tested (boundary_test.go). Assumptions: A (decompose spec). Status: proven under A.
  • PULSAR-C2 FindHint. FindHint(w',W1)=h ⇒ UseHint(h,w')=W1 ∧ weight(h)≤ω. Class: machine-checked + tested (TestFindHintToTargetMatchesUseHint). Status: proven under A.
  • PULSAR-C3 FIPS compatibility. FinalizeSignature emits bytes accepted by unmodified ML-DSA-65/87 verifiers. Class: interop-tested (circl + pq-crystals, bcc_sign_test.go). Status: interop-tested (not EC-proven; the EC byte-walk rests on Bucket-C combine_body_axiom/S_functional_spec — OPEN).
  • PULSAR-C4 Transcript privacy. Public transcript simulatable without honest s1,s2,t0,y,w; never reveals full w/LowBits(w)/c·s2/c·t0/r0. Class: tested (forbidden-field reflection guard, debug-oracle residual test) + red-team (P3Q/quorum reviews). Assumptions: NonceTranscript verifier sound (fail-closed-pending-review), PartialProof verifier sound. Status: no-leak in code; ZK soundness fail-closed-pending-review.
  • PULSAR-C5 Partial correctness. Each Partial proves z_i=λ_i y_i + c λ_i s1_i; degenerate c rejected (SampleInBall check). Class: sound-by-reduction (Maurer linear sigma) + tested. Status: sound; registered fail-closed by default.
  • PULSAR-C6 NonceTranscript soundness. W1=HighBits(w) ∧ BoundaryClear(w), full w hidden. Class: fail-closed-pending-review (validator-MPC; debug-oracle today). Status: OPEN — fail-closed.
  • PULSAR-C7 Consensus binding. Signer bitmap, transcript root, nonce cert, and signature bound by the QC. Class: tested (ConsensusCert.Verify). Status: proven by construction + tested.

Corona — threshold Module-LWE (Ringtail/Raccoon)

  • CORONA-C1 Threshold signing correctness (masked-aggregate z_Σ). Class: tested (E2E (2,3)…(7,10) + KAT oracle). Status: tested.
  • CORONA-C2 No aggregate secret-correction leakage (no c·s broadcast; Δ from public aggregate). Class: tested + red-team. Status: no-leak in code.
  • CORONA-C3 sid/nonce uniqueness + non-reuse. Class: tested (256-bit hedge; nonce_reuse_test.go). Status: proven by construction (hedge) + tested.
  • CORONA-C4 Partial-verification soundness. Class: tested. Status: tested.
  • CORONA-C5 DKG/resharing secrecy. Class: tested (Pedersen dkg2, no master reconstruction on production path). Status: tested.
  • CORONA-C6 Transcript simulation. Class: tested. Status: tested.
  • CORONA-C7 Consensus cert bitmap/root binding (reshare/activation.go). Status: tested.
  • CORONA-EC EasyCrypt machine-check. All 14 Corona EasyCrypt theories compile (easycrypt compile, gate ec-machine-check.sh). The combine bridge combine_abs_op_lifted_eq_rlwe (was C11, a whole-signature reconstruct-then-sign axiom) is now a machine-checked LEMMA: combine_abs_op_lifted is defined as the real threshold aggregate, the secret-bearing z-leg is proven via the keystone no_leak_z_aggregate (masks telescope, secret never reconstructed), and the c/Δ-legs are derived. The lone residual is the narrow public-commitment axiom threshold_public_commitment_eq_central (the w = A·y agreement — no c·s; its value is public though the EC op is usk-parameterized). Class: machine-checked modulo one public-commitment residual (down from a secret-bearing whole-bridge). Status: z-leg machine-checked; combine byte-equality rests only on the public w-agreement; still NOT "fully proven" (that residual + the wider C-cone remain).
  • Open: CORONA-EC-RECON-MODEL — the EC byte-equality cone still rests on Bucket-C combine_body_axiom, S_functional_spec, combine_body_spec, and the shrunk threshold_public_commitment_eq_central (the secret-bearing combine_abs_op_lifted_eq_rlwe is now a lemma). OPEN, disclosed, NOT closed.

Magnetar — threshold SLH-DSA (FIPS 205)

  • MAGNETAR-C1 Final signature verifies under unmodified SLH-DSA verifier (standalone leg). Class: interop-tested (circl). Status: tested.
  • MAGNETAR-C2 No FORS/WOTS+ one-time secret reconstructed by aggregator — on the production path. Class: by-construction (production = certification over independent sigs; no shared key). Status: holds for production; THBS-SE research-only DOES reconstruct (disclosed).
  • MAGNETAR-C3 No leaf index reused. Class: standalone signers hold own keys; no committee leaf assignment. Status: N/A for production cert (independent sigs).
  • MAGNETAR-C4 Crash/rollback/concurrency cannot reuse a leaf. Status: N/A for production cert; THBS-SE research-only.
  • MAGNETAR-C5 ADRS/domain separation matches SLH-DSA exactly. Class: tested (circl-backed). Status: tested.
  • MAGNETAR-C6 Threshold transcript reveals only public signature material — production. Status: by-construction (independent sigs). THBS-SE: reconstructs seed, research-only.
  • MAGNETAR-C7 Consensus cert binds signer bitmap + signature. Status: via QUASAR-C* (the quorum cert).
  • Open / honest: true threshold SLH-DSA without reconstruction is open-research (Kondi–Kumar–Vanegas impossibility). Production claim is certification, not threshold signing.

P3Q — STARK/FRI substrate

  • P3Q-C1 verify_air never panics / fails open on malformed proof. Class: tested (f1_*, f2_* catch_unwind → typed error). Status: fixed + regression-tested.
  • P3Q-C2 Zero-constraint AIR rejected. Class: tested (f4_*). Status: fixed + tested.
  • P3Q-C3 Transition-domain semantics explicit + enforced (cyclic contract; is_transition removed). Class: tested (f3_*) + documented. Status: fixed.
  • P3Q-C4 FRI degree bound sound. Class: tested (cheating_final_poly_rejected, high_degree_codeword_rejected) + sound-by-reduction. Assumptions: C (FRI proximity-gap soundness). Status: tested under C.
  • P3Q-C5 OOD/DEEP binding sound. Class: red-team (15 forgeries rejected) + tested. Status: adversarially validated.
  • P3Q-C6 Merkle query binding sound. Class: tested. Status: tested.
  • P3Q-C7 Weighted-quorum AIR encodes finality rules. Status: open-research — the N-FIPS-verification circuit (Keccak-AIR) is STAGED, not built. Until then finality runs full-node-verifiable (QUASAR-C*).

Consensus — weighted quorum certificate

  • QUASAR-C1 Quorum cannot be forged by count/weight inflation. Class: tested (TestRedteam_F1_*; threshold bound into signed message + verifier floor). Status: CRITICAL fixed; PoC fails closed.
  • QUASAR-C2 Duplicate signers rejected. Class: tested (strictly-increasing ids). Status: tested.
  • QUASAR-C3 Out-of-set signers rejected. Class: tested (weighted-Merkle inclusion). Status: tested.
  • QUASAR-C4 Payload/position recomputed internally (Verify owns the envelope). Class: tested (TestRedteam_F3_*). Status: HIGH fixed.
  • QUASAR-C5 Bitmap/signature/root mismatch rejected. Class: tested. Status: tested.
  • QUASAR-C6 Cross-domain replay rejected (every consensus field bound). Class: tested (TestRedteam_F3_PositionTamperRejected). Status: tested.
  • QUASAR-C7 Threshold comparison has no off-by-one / overflow; decode DoS capped. Class: tested (TestRedteam_F2_*, weight-overflow guard). Status: HIGH fixed.

Open Bucket-C assumptions blocking "fully proven"

These are disclosed, not closed. No claim above is labelled "fully proven" while it depends on one. Each must be: discharged · replaced with executable spec+equivalence · or the dependent claim downgraded.

  • combine_body_axiom (pulsar, corona) — extracted threshold combine = central sign on the Lagrange-RECONSTRUCTED secret (byte-walk). Discharge = Jasmin byte-walk.
  • S_functional_spec (pulsar, corona) — single-party module is a faithful FIPS signer. Discharge = libjade byte-walk.
  • corona combine_body_spec, combine_abs_op_lifted_bridge, threshold_public_commitment_eq_central (the narrow public w-agreement; replaced the secret-bearing combine_abs_op_lifted_eq_rlwe, now a lemma), sign_abs_op_lifted_eq_rlwe — reconstruct-then-sign refinement steps 2–6. (The V04 mldsa_sign_ctx_axiom / algebraic_aggregate_ctx_body_axiom were removed with the deleted V04_Sign_Ctx.ec.)
  • P3Q FRI proximity-gap soundness (standard STARK assumption — state, do not "prove").
  • Validator-honest-threshold assumption (consensus).

The honest one-liner: All axioms are discharged, bridged, or disclosed. Open security assumptions remain review blockers.

Merge rule (do not merge until ALL true)

  • Pulsar: axiom inventory complete; C assumptions disclosed; check.sh green.
  • Corona: axiom inventory complete; C assumptions disclosed; check.sh green.
  • Magnetar: threshold SLH-DSA status honest; no circular proof claims; check.sh green.
  • P3Q: F1–F6 fixed; malformed-proof tests green.
  • Consensus: CRITICAL finality PoCs fail closed.
  • Security/compliance: references resolve to luxfi/security/framework.

§wording — the strongest honest language allowed NOW

Review-ready high-assurance release candidate. P3Q and consensus critical findings are fixed and regression-tested. Pulsar, Corona, and Magnetar have family-specific assurance gates, disclosed assumptions, and no known production secret-leak paths. External cryptographic review and the remaining open proof assumptions are the final gates before any production-certified or fully-proven claim.

Unlocked only after EXTERNAL-REVIEW-SIGNOFF.md is signed: "Lux production-certified" (passed Lux gate + external review), "NIST-ready package" (specs+vectors+interop+review packaged), "fully proven under stated assumptions". Never "unconditionally proven" / "NIST approved".

Reference in New Issue View Git Blame Copy Permalink