Files
zooqueen b36d13ebd5 release(2026-06-pq-threshold-stack): add FULLY-PQ-AUDIT + STANDARD-ASSUMPTIONS
FULLY-PQ-AUDIT.md: per-production-path PQ-primitive ledger with file:line
evidence, complete classical-crypto reachability list, and the verdict.
Headline finding: QuasarCert.VerifyWithRealKeys required BLS-12-381 on the
finality path (contradicting the cert's pure-PQ contract) -- FOUND AND FIXED
under this audit (consensus: BLS optional + fail-closed >=1-leg guard,
regression-tested). Post-fix verdict: the production consensus/finality/
signature-verification envelope is FULLY POST-QUANTUM. All other classical
crypto (optional BLS fast-path, Corona DKG-ceremony Ed25519/X25519, Verkle
banderwagon point-decode, qzmq ML-KEM stub, gated EVM precompiles, superseded+
forbidden Groth16) is confirmed OFF the finality-cert verification path.

STANDARD-ASSUMPTIONS.md: the irreducible minimal cryptographic-assumption
ledger -- Module-LWE, Module-SIS, SLH-DSA SHAKE hash-family EU-CMA, FRI
proximity-gap soundness (staged), SHAKE/cSHAKE/KMAC as RO, honest-validator
BFT threshold. For each: dependent claims, why standard/accepted, parameter
set + NIST PQ category. The honest 'fully proven UNDER THESE assumptions'
bedrock; explicitly excludes pairing/DLOG/factoring/trusted-setup.
2026-06-21 15:25:24 -07:00

15 KiB
Raw Permalink Blame History

Standard-Assumptions Ledger — Lux PQ Threshold Stack, release 2026-06-pq-threshold-stack

This is the irreducible bedrock: the complete, minimal set of cryptographic assumptions the entire release reduces to. It is the precise meaning of "fully proven under stated assumptions" — strip these and nothing is left to assume; everything else in the stack is a construction, a reduction, or an implementation bridge that rests on top of this list.

Relationship to the other ledgers. This file is the minimal external view (what a cryptographer must accept to trust the release). It is distinct from, and complementary to:

  • ASSUMPTIONS.md — the per-repo A/B/C axiom bucket disclosure (which declared EasyCrypt/Lean axioms are standard-math vs spec-bridge vs open).
  • CLAIMS.md — the claim matrix (each claim ID → evidence class → assumptions → status).
  • per-repo AXIOM-INVENTORY.md + .assurance/reviewed-axioms.txt — the authoritative bucketed source of truth.

Every Bucket-C "open assumption" in those files reduces to one of the assumptions below; this ledger is the closure of that reduction. No assumption here is "proven" — by definition. They are the accepted hardness / soundness substrate. Where the release proves something, it proves it relative to these.

A note on honesty. Two assumptions below (A1–A2 for the lattice families, A4 for FRI) are STANDARD and accepted in the literature and we STATE them rather than prove them — that is correct cryptographic practice, not a gap. What would be a gap is a construction-specific assumption masquerading as standard; we have none of those — every item below is a community-vetted, NIST-standardized or peer-reviewed hardness/soundness assumption, used at a standardized parameter set.


The six irreducible assumptions

# Assumption Family Standardization Used by (claims)
A1 Module-LWE (decisional/search hardness) Lattice FIPS 203 (ML-KEM), FIPS 204 (ML-DSA) ML-DSA sigs, Pulsar, Corona, ML-KEM transport
A2 Module-SIS (short integer solution hardness) Lattice FIPS 204 (ML-DSA EU-CMA) ML-DSA sigs, Pulsar (strong unforgeability)
A3 SLH-DSA hash-family security = preimage/2nd-preimage/collision resistance of SHAKE ⇒ FORS + WOTS+ + hypertree EU-CMA Hash-based FIPS 205 (SLH-DSA) Magnetar standalone + certification, SLH-DSA precompile
A4 FRI proximity-gap soundness (+ Fiat-Shamir in the ROM) Hash-based IOP Peer-reviewed (BBHR18, BCIKS20); not a NIST standard but the accepted STARK assumption P3Q low-degree test (staged finality compression)
A5 SHAKE / cSHAKE / KMAC modeled as a random oracle (and as a collision-resistant / domain-separating hash) Symmetric (sponge) FIPS 202, SP 800-185 every Fiat-Shamir transcript, domain separation, Merkle/commitment binding, KMAC MACs
A6 Honest-validator threshold (BFT majority; ≥ quorum weight is honest) Protocol / system Classical BFT model the weighted quorum certificate = finality

Everything else the release ships — threshold certification, byte-equality to FIPS verifiers, the BCC/CEF no-leak signing transcripts, Merkle inclusion, weighted-quorum binding — is a construction or reduction over A1–A6, not a new assumption.


A1 — Module-LWE

Statement. For the module rank, ring, and modulus of a given parameter set, the decisional Module-LWE distribution (A, A·s + e) is computationally indistinguishable from uniform (and search-MLWE is hard).

Which claims depend on it.

  • ML-DSA per-validator signatures (P1, P4) — the quorum certificate's per-signer ML-DSA verifier; the EVM ML-DSA precompile (P9). EU-CMA of ML-DSA reduces to MLWE (key indistinguishability) + MSIS (A2).
  • Pulsar threshold ML-DSA (P5) — same hardness; the threshold construction is byte-equal to a single-party FIPS 204 signature, so its unforgeability is exactly ML-DSA's under A1+A2 (the threshold layer adds no new hardness assumption — it adds the reconstruct-then-sign / BCC refinement, which is a construction over A1+A2, disclosed Bucket-C, not a hardness assumption).
  • Corona threshold (P6) — Ringtail/Raccoon-family Module-LWE; the masked- aggregate signature's unforgeability reduces to MLWE.
  • ML-KEM-768 transport (P10) — IND-CCA2 of ML-KEM reduces to MLWE.

Why standard. Module-LWE is the hardness assumption NIST standardized in FIPS 203 and FIPS 204 (2024) after the multi-year PQC competition. It is a structured-lattice problem with a worst-case-to-average-case connection (Langlois–Stehlé) and is the most scrutinized post-quantum assumption in deployment.

Parameter sets + security level.

  • ML-DSA-65 (NIST PQ Category 3, ≥ AES-192-equivalent) — production identity / quorum default (ModeP65, pulsar/ref/go/pkg/pulsar/params.go:26; QuorumSchemeMLDSA65 = 0x42).
  • ML-DSA-44 (Cat 2) and ML-DSA-87 (Cat 5) also registered (QuorumSchemeMLDSA44/87).
  • Pulsar production ring/modulus: N = 256 (ring degree), Q = 0x1000000004A01 (48-bit NTT-friendly prime), module M = 8, Dbar = 48, Kappa = 23; parameter tightness classical 2^142 / quantum 2^130 (BDGL sieving + Grover) per proofs/quasar-cert-soundness.tex App. E.
  • Corona production ring/modulus: N = 256, q = 0x1000000004A01 (48-bit) (corona/SECURITY.md:35-36).

A2 — Module-SIS

Statement. For the parameter set, finding a short nonzero z with A·z = 0 (mod q) (short integer solution in the module) is computationally hard.

Which claims depend on it. ML-DSA / Pulsar strong unforgeability (P1, P4, P5): an ML-DSA forgery yields a short MSIS solution. A1 gives key indistinguishability; A2 gives that you cannot forge a short signature vector. Together they are the EU-CMA reduction of FIPS 204.

Why standard. MSIS is the companion assumption to MLWE in the Fiat-Shamir-with-aborts (Lyubashevsky) signature design that FIPS 204 standardizes. Same lattice provenance and scrutiny as A1.

Parameter sets + security level. Same parameter sets as A1; the MSIS bound is set by the ML-DSA-65 (Cat 3) / Pulsar (Dbar=48, Kappa=23) parameters. Security level as A1: NIST Cat 3 for ML-DSA-65; Pulsar 2^142 classical / 2^130 quantum.


A3 — SLH-DSA hash-family security (FORS + WOTS+ + hypertree EU-CMA)

Statement. The SHAKE-based hash functions used by SLH-DSA are preimage-, second-preimage-, and collision-resistant (and behave as random oracles where the proof needs it), so that the FORS few-time signature, the WOTS+ one-time signature, and the XMSS/hypertree authentication structure together give EU-CMA for the stateless hash-based signature.

Which claims depend on it.

  • Magnetar standalone per-validator SLH-DSA signatures (P2, P7) — the quorum certificate's SLH-DSA verifier; the EVM SLH-DSA precompile (P9).
  • Magnetar threshold = certification (MAGNETAR-C1..C7): production Magnetar is N independent FIPS 205 signatures aggregated by a quorum cert; each signature's unforgeability is exactly A3. The certification layer adds no new hardness assumption (it is a count over independent A3 signatures).
  • Not depended on by production: true no-reconstruction threshold SLH-DSA is open research (Kondi–Kumar–Vanegas impossibility for black-box-RO thresholdization). The research-only THBS-SE leg reconstructs the seed and is excluded from production claims.

Why standard. A3 is the security goal of NIST FIPS 205 (2024), inherited from the SPHINCS+ submission (Bernstein et al.). It is the most conservative PQ signature assumption: it rests on symmetric (hash) security only, with no structured-lattice or number-theoretic assumption — which is precisely why Magnetar is the cross-family backstop ("if every lattice family breaks, hash-based one-wayness still secures finality", types.go:115-125).

Parameter sets + security level.

  • SLH-DSA-SHAKE-192s (ModeM192s, QuorumSchemeSLHDSA192s = 0x06) — Magnetar production target, NIST PQ Category 3 (≥ 192-bit classical), smallest signatures at that level (magnetar/SPEC.md §2).
  • SLH-DSA-SHAKE-192f (0x16) and 256s (0x07) also registered.
  • Single-party primitive dispatches to cloudflare/circl/sign/slhdsa v1.6.3 (community-audited FIPS 205 reference).

A4 — FRI proximity-gap soundness (+ Fiat-Shamir in the ROM)

Statement. The FRI low-degree test is sound up to the proximity gap: a prover that passes the FRI verifier with non-negligible probability is, with overwhelming probability, committed to a codeword within the asserted distance of a low-degree polynomial. Combined with Fiat-Shamir (A5) the interactive soundness becomes non-interactive in the random-oracle model.

Which claims depend on it. P3Q STARK/FRI soundness (P3Q-C4, P8). This is the ONE genuinely STARK-specific assumption, and it is stated, not proven — correct practice. P3Q's docs frame it honestly: "64 queries over an LDE of rate ≤ 1/8 gives ≥ 100-bit soundness for the FRI proximity gap" (p3q-fri/src/prover_shared.rs:16); SECURITY.md:16 states a conjectured-security target (≥ 128-bit classical, ≥ NIST PQ Cat 3). No claim of a soundness proof is made.

Scope today. P3Q is staged, not live, for finality (the N-FIPS-verification Keccak-AIR circuit is not built — §4 of FULLY-PQ-AUDIT.md). So A4 currently gates a roadmap path (finality compression), not today's finality verification (which is full-node-verifiable under A1–A3, A5–A6). A4 becomes load-bearing for finality only when the P3Q rollup circuit ships and is audited.

Why standard / accepted. FRI and its proximity-gap soundness are the foundation of every deployed STARK (StarkWare, Plonky3, RISC Zero). The bounds are peer-reviewed (Ben-Sasson–Bentov–Horesh–Riabzev 2018; Ben-Sasson–Carmon– Ishai–Kopparty–Saraf 2020 proximity gaps). It is not a NIST standard, but it is the accepted soundness assumption for hash-based IOPs and depends only on symmetric (hash) security for its commitments, so it is post-quantum.

Parameter set + security level. Goldilocks field p = 2^64 − 2^32 + 1 (p3q-field/src/goldilocks.rs:15); cSHAKE256 Merkle commitments (p3q-sha3, p3q-merkle); 64 FRI queries at LDE rate ≤ 1/8 → ≥ 100-bit FRI soundness; conjectured ≥ 128-bit classical / NIST PQ Cat 3 overall target.


A5 — SHAKE / cSHAKE / KMAC as a random oracle (and collision-resistant hash)

Statement. The Keccak sponge instantiated as SHAKE128/256, cSHAKE256, and KMAC256 behaves as a random oracle where the security proofs need one, and is collision- and preimage-resistant where used as a plain hash; distinct cSHAKE customization strings yield independent oracles (domain separation).

Which claims depend on it. Pervasive — it is the symmetric substrate under everything:

  • Fiat-Shamir for every challenge derivation (Pulsar SampleInBall/transcript, Corona transcript, P3Q challenger, the no-leak BCC/CEF transcripts).
  • Merkle / vector-commitment binding (quorum-cert validator-set Merkle, FRI Merkle, Verkle hash-based proof check verifyIPAOpening).
  • KMAC256 MACs (quasar/bls.go event-horizon attestations, the KMAC envelope-auth patterns).
  • Domain separation: every protocol's distinct customization tags (MAGNETAR-…, PULSAR-…, CORONA-…, LUX-VERKLE-…) rely on SP 800-185's guarantee of no cross-(N,S) collision.

Why standard. FIPS 202 (SHA-3/SHAKE) and SP 800-185 (cSHAKE, KMAC, TupleHash). Keccak is the most analyzed sponge; the random-oracle instantiation of SHAKE is the standard modeling assumption for hash-based and Fiat-Shamir constructions. Post-quantum: best known quantum attacks are generic (Grover/BHT), so the security level halves predictably and the parameter sizes are chosen accordingly.

Parameter set + security level. SHAKE256 / cSHAKE256 / KMAC256 at 256-bit capacity → 128-bit collision / quantum-generic security; KMAC output widths 48 bytes (SHA3-384) canonical for the consensus MAC bundles (32-byte legacy refused under strict-PQ). This is consistent with NIST Cat 3 across the stack.


A6 — Honest-validator threshold (BFT majority)

Statement. A quorum-weight subset of the validator set is honest: at least the configured threshold weight of validators follow the protocol and do not collude to sign conflicting finality.

Which claims depend on it. The weighted quorum certificate = finality (QUASAR-C1..C7, P3). The certificate proves "≥ quorum weight of distinct, in-set validators each produced a valid INDEPENDENT PQ signature over the same domain-separated message"; that this implies finality (no two conflicting blocks finalize) is the BFT-majority argument — a system/protocol assumption, not a cryptographic-hardness one. The cryptography (A1–A3, A5) guarantees the signatures are unforgeable and the count is honest; A6 is what turns an honest count into safety.

Why standard. This is the classical Byzantine-fault-tolerance threshold assumption underlying every BFT consensus (PBFT, Tendermint, HotStuff, Snowman/Avalanche-family). It is not cryptographic and not post-quantum- specific; it is the system trust model. The quorum-cert red-team (QUASAR-C1..C7, all PoCs fail closed) verifies the cryptographic binding that prevents count/weight inflation, duplicate signers, out-of-set signers, and cross-domain replay — i.e. that an adversary cannot manufacture a spurious honest count; A6 is the residual that the genuine count is honest.


The honest one-paragraph statement

The Lux PQ threshold stack is fully proven under exactly these six assumptions: Module-LWE (A1), Module-SIS (A2), the SLH-DSA SHAKE hash-family EU-CMA (A3), FRI proximity-gap soundness (A4, staged), SHAKE/cSHAKE/KMAC as a random oracle (A5), and an honest-validator BFT threshold (A6). A1–A3 and A5 are NIST-standardized (FIPS 202/203/204/205, SP 800-185) at NIST PQ Category 3 parameters; A4 is the peer-reviewed, accepted STARK soundness assumption (hash-based, post-quantum) and currently gates only the staged finality-compression path; A6 is the classical BFT system model. Every other security property the release asserts — threshold certification, FIPS byte-equality, no-leak signing transcripts, Merkle/quorum binding — is a construction or a reduction over this substrate, not a new assumption. Stripping these six leaves nothing to assume. This is the bedrock the "proven under stated assumptions" language refers to.

What is NOT on this list (deliberately): no pairing / co-CDH (the BLS fast-path is optional and off the PQ-finality path — see FULLY-PQ-AUDIT.md §2.1; a pure-PQ cert does not depend on it), no discrete log, no factoring, no elliptic-curve assumption, no trusted setup, no SNARK knowledge-of-exponent / AGM assumption (Groth16/KZG are superseded and forbidden under strict-PQ). Their absence from this ledger is the precise content of "fully PQ".