mirror of
https://github.com/luxfi/pulsar.git
synced 2026-10-30 14:45:29 +00:00
zooqueen
c546d5dc0a
The headline EC byte-equality (pulsar_n1_byte_equality) proved the threshold
combine bit-equals SinglePartyRun, which RECONSTRUCTS the master secret and
signs with it -- exactly the path the production leaderless signer must never
take (PULSAR-V13-HINT-LEAK). This pass re-scopes that cone as IDEALISED
CORRECTNESS and adds the HONEST production model whose residual is a STANDARD
Module-LWE/MSIS reduction, not an implementation reconstruct.
New proofs/easycrypt/Pulsar_N1_NoLeak.ec (written; machine-recheck pending
EasyCrypt -- no `ec` on host, scripts/checks/ec-compile.sh is the CI gate):
- no_leak_z_aggregate: the public masked Lagrange aggregate equals central z
WITHOUT forming the master secret (re-exports the Lean-bridged
threshold_partial_response_identity).
- public_hint_roundtrip [B, Lean-backed]: the hint is recovered from the
PUBLIC w' = A*z - c*t1*2^d via FIPS UseHint; procedure lift of the
machine-checked Lean boundary_clearance + findHintCoeff_unique. No
c*s2/c*t0/r0 anywhere.
- no_leak_reduction [C-standard, OPEN]: under Module-LWE + Module-SIS the
public transcript leaks nothing about (s1,s2,t0) beyond one FIPS 204
signature. The honest replacement for combine_body_axiom -- a reduction to
the SAME lattice assumptions ML-DSA's EUF-CMA uses, secret NEVER formed.
The CORRECTNESS CORE is machine-checked in Lean 4 + Mathlib on this host
(luxfi/proofs: Crypto.Pulsar.NoLeakAggregate / .BoundaryClearance /
Threshold_Lagrange; lake build green, #print axioms shows no sorryAx).
Disclosure updated to match reality: AXIOM-INVENTORY (new Bucket C-standard +
"A is machine-checked in Lean"), PROOF-CLAIMS (two models), BLOCKERS
(PULSAR-EC-RECON-MODEL re-scoped, first criterion now [x]), budget AXIOM
87->89 (the 2 new disclosed standard-assumption axioms). Framework gate PASS
(all 5 checks); ref/go build + tests green.
42 lines
5.3 KiB
Plaintext
42 lines
5.3 KiB
Plaintext
# Axioms that a LOAD-BEARING lemma rests on, reviewed and justified.
|
|
# Format: AXIOM_NAME <bucket> -- <justification>
|
|
#
|
|
# An entry here is an explicit, disclosed trust assumption. The framework
|
|
# (~/work/lux/luxfi/security/framework/checks/circular-proof.sh) HARD-requires only
|
|
# the axioms that a load-bearing-named lemma discharges via apply/exact in a
|
|
# <=12-line proof; today that is `lagrange_inverse_eval` alone. We list MORE
|
|
# than the mechanical minimum on purpose: every axiom in the dependency cone
|
|
# of the headline byte-equality lemma is part of the trust surface and is
|
|
# written down here with its bucket. This is full disclosure, NOT a blanket
|
|
# allow -- only load-bearing / security-cone axioms appear; the pure
|
|
# layout/length B-axioms and the standard-fact A-axioms that feed only
|
|
# structural lemmas are inventoried in AXIOM-INVENTORY.md, not blanket-listed
|
|
# here. Buckets: A standard-math-fact | B serialization/layout | C OPEN
|
|
# security assumption (reconstruct-then-sign; see BLOCKERS.md).
|
|
|
|
# --- A: load-bearing standard-math-fact (mechanically flagged) ---
|
|
lagrange_inverse_eval A -- Lagrange interpolation: P(0) recovered from any t distinct evaluations over a field of order > committee size (spec/pulsar.tex eq. 476). EasyCrypt lacks this over abstract share_t; Lean-bridged to Crypto.Pulsar.Shamir.shamir_correct_at_target (Mathlib polynomial-Lagrange). The algebraic core the threshold reduction USES, NOT the threshold security claim. Used by reconstruct_of_share via `exact:`.
|
|
threshold_partial_response_identity A -- Lagrange-aggregation of per-party partial responses = centralised z on the reconstructed share. Lean-bridged. Load-bearing for combine_body_z_spec (the z-stage derived lemma) -> pulsar_n1_byte_equality.
|
|
reconstruct_linear A -- reconstruction is linear over share-list addition (LinearMap.map_add). Lean-bridged. Load-bearing for the N4 reshare-preservation lemmas.
|
|
shamir_correct A -- reconstruction is a left inverse of fresh sharing (Lagrange-at-zero). Lean-bridged. Load-bearing for honest_reshare_reconstructs / reshare_preserves_secret_honest (N4).
|
|
add_share_zeroR A -- additive identity on share_t (AddCommMonoid). Lean-bridged. Load-bearing for the N4 reshare zero-sharing argument.
|
|
|
|
# --- C: OPEN security assumptions in the IDEALISED-CORRECTNESS byte-equality cone
|
|
# (reconstruct-then-sign). DISCLOSED, NOT closed. These prove the threshold
|
|
# OUTPUT bit-equals central sign on the reconstructed secret -- an idealised
|
|
# CORRECTNESS statement, NOT how production runs. The production no-leak
|
|
# path's residual is the STANDARD-ASSUMPTION reduction in the next block
|
|
# (Pulsar_N1_NoLeak.ec), not these. See BLOCKERS.md PULSAR-EC-RECON-MODEL. ---
|
|
combine_body_axiom C -- OPEN. declare axiom: T.combine ~ CombineAbs.combine on honest-quorum inputs == the extracted threshold combine equals the centralised ML-DSA sign of the LAGRANGE-RECONSTRUCTED secret. Module-contract form of the whole byte-walk; pulsar_n1_byte_equality rests on it via `call combine_body_axiom`. IDEALISED CORRECTNESS model only. Closure = the Jasmin byte-walk (issue #4). NOT proven.
|
|
S_functional_spec C -- OPEN. declare axiom: S.sign ~ FIPS204Sign.sign on accepted inputs == the single-party module is a faithful FIPS 204 signer. pulsar_n1_byte_equality rests on it via single_party_run_refines_fips204. Closure = the libjade byte-walk (issue #3). NOT proven.
|
|
algebraic_aggregate_ctx_body_axiom C -- OPEN. The v0.4 reconstruct-then-sign axiom: AlgebraicAggregateCtx output = FIPS 204 SignCtx(sk_master, ctx, M) where sk_master is the existentially-quantified RECONSTRUCTED master secret. threshold_sign_ctx_equiv_fips204_sign_with_ctx rests on it. Go-discharged by test + AST sweep, NOT by EC. NOT proven.
|
|
|
|
# --- The NO-LEAK model (Pulsar_N1_NoLeak.ec) -- the HONEST production residual.
|
|
# Replaces reconstruct-then-sign as the load-bearing path: the masked Lagrange
|
|
# aggregate equals central z WITHOUT forming the master secret, the hint is
|
|
# recovered from PUBLIC w', and the ONLY open assumption is a STANDARD
|
|
# Module-LWE/MSIS reduction (no implementation reconstruct). The algebraic core
|
|
# is MACHINE-CHECKED in Lean (Crypto.Pulsar.NoLeak / .Boundary; lake build green). ---
|
|
public_hint_roundtrip B -- standard/Lean-backed. Procedure-level lift of the MACHINE-CHECKED (Lean) Crypto.Pulsar.Boundary.boundary_clearance + findHintCoeff_sound/_unique: on a boundary-clear nonce, FindHint over the PUBLIC (w', w1) returns a hint UseHint maps back to w1. References ONLY public quantities (w'=A*z-c*t1*2^d, w1) -- no c*s2/c*t0/r0. Load-bearing for no-leak hint correctness. Recheck pending ec-compile.
|
|
no_leak_reduction C -- OPEN, but STANDARD-ASSUMPTION (NOT reconstruct-then-sign). Under Module-LWE + Module-SIS the public threshold transcript (w1, commit(w), clearance proof, c_tilde, z, h) is simulatable from one single-party FIPS 204 signature's leakage == leaks nothing extra about (s1,s2,t0). The honest replacement for combine_body_axiom: a reduction to the SAME lattice assumptions ML-DSA's EUF-CMA already uses, with the secret NEVER reconstructed. no_leak_under_standard_assumptions rests on it. EC mirror of MACHINE-CHECKED Lean Crypto.Pulsar.NoLeak.NoLeakReduction. Full simulation proof = v0.8 artifact. NOT proven (but a standard reduction, not an impl reconstruct).
|