mirror of
https://github.com/luxfi/threshold.git
synced 2026-10-30 15:15:53 +00:00
zeekay
509acb2c26
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.
51 lines
2.0 KiB
Plaintext
51 lines
2.0 KiB
Plaintext
(* -------------------------------------------------------------------- *)
|
|
(* BLS-Threshold -- Constant-time obligations *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* STATUS: SHELL. Same BGL leakage model as FROST / CGGMP21 / Pulsar. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* BLS threshold's secret-touching surface is small: *)
|
|
(* - partial_sign: secret = (share s_i). *)
|
|
(* The only operation is sigma_i = H(m)^{s_i}, a G2 scalar mul. *)
|
|
(* CT depends on the underlying G2 scalar-mul implementation. *)
|
|
(* - aggregate: no secret inputs => trivially CT. *)
|
|
(* *)
|
|
(* CT inheritance: the Lux profile uses `cloudflare/circl` BLS12-381 *)
|
|
(* with its built-in CT G1/G2 scalar multiplication. Stated as the *)
|
|
(* refinement obligation below. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
require import AllCore List Int IntDiv Distr DBool.
|
|
|
|
type leakage_t.
|
|
|
|
type share_t.
|
|
type g2_t.
|
|
type message_t.
|
|
type sig_share_t.
|
|
|
|
module type CTPartialSign = {
|
|
proc partial_sign(share : share_t, msg : message_t)
|
|
: sig_share_t * leakage_t
|
|
}.
|
|
|
|
section PartialSignCT.
|
|
|
|
declare module PS <: CTPartialSign.
|
|
|
|
declare axiom partial_sign_constant_time
|
|
(share1 share2 : share_t)
|
|
(msg : message_t) :
|
|
equiv [ PS.partial_sign ~ PS.partial_sign :
|
|
={msg}
|
|
/\ share{1} = share1 /\ share{2} = share2
|
|
==>
|
|
res{1}.`2 = res{2}.`2 ].
|
|
|
|
end section PartialSignCT.
|
|
|
|
(* aggregate: no secret inputs; trivially CT. Stated for completeness. *)
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* End of BLS_Threshold_CT.ec *)
|
|
(* -------------------------------------------------------------------- *)
|