mirror of https://github.com/luxfi/threshold.git synced 2026-10-30 15:15:53 +00:00

Files

T

zeekay e8f154a5b1 proofs/bls: Tier A EC theories + Lean bridges + Jasmin CT scaffolds

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.

2026-05-19 08:34:32 -07:00

2.4 KiB

Raw Permalink Blame History

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.

2.4 KiB Raw Permalink Blame History