mirror of
https://github.com/luxfi/threshold.git
synced 2026-10-30 15:15:53 +00:00
zeekay
e8f154a5b1
Adds the Tier A formal-artifact cluster for protocols/bls (Lux profile of Boldyreva 2003 threshold BLS over BLS12-381). Mirrors luxfi/pulsar's Tier A structure adapted to BLS's algebraically minimal threshold construction (Lagrange + G2-linearity, no nonce sampling, no MtA, no ZK). - proofs/easycrypt/BLS_Threshold_N1.ec — Class N1 byte-equality reduction - proofs/easycrypt/BLS_Threshold_N1_Refinement.ec — partial_sign + aggregate - proofs/easycrypt/BLS_Threshold_N4.ec — DKG public-key preservation - proofs/easycrypt/lemmas/BLS_Threshold_CT.ec — constant-time obligations - proofs/easycrypt/AXIOM-INVENTORY.md — honest enumeration - proofs/lean-easycrypt-bridge.md — Lean↔EC bridge map - jasmin/lib/ + jasmin/single-party/ + jasmin/threshold/ — Jasmin scaffolds BLS-threshold has the smallest formal-methods surface of the three classical threshold protocols. Admit budget: 1/1 (same one-line group-identity admit as FROST_N4, CGGMP21_N4, Pulsar_N4). Production deployment note: ships with trusted-dealer keygen only; DKG gap disclosed in SUBMISSION-STATUS.md §3.3.
Threshold BLS Jasmin high-assurance track
This directory holds Jasmin sources for the BLS12-381 threshold
signature scheme (Lux profile), paired with the EasyCrypt theories
at ../proofs/easycrypt/.
Status — initial track
This is the initial high-assurance scaffolding. BLS-threshold has the smallest Jasmin surface of the three classical threshold protocols (FROST, CGGMP21, BLS):
| Layer | Operation | Status |
|---|---|---|
| Per-party sign | sigma_i = H(m)^{s_i} on G2 | Single G2 scalar mul |
| Aggregate | sigma = sum_i lambda_i * sigma_i | G2 weighted sum |
| Verify | e(sigma, g1) ?= e(H(m), pk) | Standard BLS pairing |
What we commit at this submission cycle:
- Single-party BLS sign / verify Jazz signatures (stubs; libjade does NOT yet provide BLS12-381 Jasmin sources).
- Threshold layer Jazz signatures (stubs; partial_sign and aggregate).
- EasyCrypt theory shells at
../proofs/easycrypt/.
Layout
jasmin/
lib/ — shared helpers (transcript, params)
single-party/ — single-party BLS sign / verify
bls12_381_sign.jazz — H(m)^{sk} on G2 (stub)
threshold/ — threshold layer
partial_sign.jazz — sigma_i = H(m)^{s_i} (stub)
aggregate.jazz — sum_i lambda_i * sigma_i (stub)
Single-party BLS — circl integration
luxfi/crypto/bls wraps cloudflare/circl/ecc/bls12381 which is
documented constant-time. Until libjade or formosa-crypto ships a
Jasmin port of BLS12-381, the Lux profile inherits CT from circl.
Threshold layer — what each .jazz will do
| File | Algorithm | Mirrors Go reference |
|---|---|---|
partial_sign.jazz |
sigma_i = H(m)^{s_i} | protocols/bls/bls.go:46 Sign |
aggregate.jazz |
sigma = sum lambda_i * sigma_i | protocols/bls/bls.go:65 AggregateSignatures |
Constant-time obligations
| Function | Secret input | CT obligation |
|---|---|---|
partial_sign |
share s_i | G2 scalar mul CT |
aggregate |
none | trivially CT |
How to check
~/work/lux/threshold/scripts/check-high-assurance.sh
Citations
- Almeida, Barbosa, Barthe, Blot, Grégoire, Laporte, Oliveira, Pacheco, Schwabe, Strub. The last mile. IEEE S&P 2020.
- Boldyreva, A. Threshold signatures, multisignatures, and blind signatures based on the gap-Diffie-Hellman-group signature scheme. PKC 2003.
- IETF CFRG. draft-irtf-cfrg-bls-signature. Wire-format reference.