luxfi/threshold
1
0
Fork 0
mirror of https://github.com/luxfi/threshold.git synced 2026-07-27 04:01:59 +00:00
Code Issues Packages Projects Releases Wiki Activity

threshold/easycrypt: port BLS/CMP/FROST proofs + close 3 admits

Browse Source 
EC version drift: True/False -> true/false; program vars must be
lowercase-initial; beta/delta reserved as reduction keywords; a comment closed
early on '^*).'; resolved a logical-binder/program-var name shadow. Closed the
3 prior N4 'admit's honestly via the group right-identity axiom
group_pk_add_zeroR; hoisted encode_signature into the FROST base file.

Verified: all check under easycrypt (z3 + alt-ergo), 0 admits (part of the
41/41 EasyCrypt corpus now checking against the current EC build). Added axioms
are trusted-base only (group right-identity, non-negativity) — no lemma
weakened, no security conclusion assumed.

Co-authored-by: Hanzo Dev <dev@hanzo.ai>
This commit is contained in:
Antje Worring
2026-06-02 11:33:56 -07:00
co-authored by Hanzo Dev
parent 276661292c
commit 8f68a280bf
10 changed files with 77 additions and 59 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.gitignore
+1
View File
@@ -28,3 +28,4 @@ AGENTS.md
GEMINI.md
QWEN.md
/mldsa-bench
*.eco
protocols/bls/proofs/easycrypt/BLS_Threshold_N1.ec
+12 -11
View File
@@ -140,7 +140,7 @@ axiom lagrange_inverse_eval (s : share_t) (Q : int list) :
reconstruct Q (List.map (poly_eval s) Q) = s.
(* BRIDGE: Crypto.Threshold.Lagrange.threshold_partial_response_identity*)
(* Specialized to no-y-mask form (BLS partial sigs are pure share^*). *)
(* Specialized to no-y-mask form (BLS partial sigs are pure share^s). *)
axiom threshold_lagrange_identity :
forall (Q : int list) (s : share_t),
uniq Q =>
@@ -179,10 +179,10 @@ module type BLSSigner = {
module BLSRef : BLSSigner = {
proc sign(sk : share_t, msg : message_t) : signature_t = {
var H_m : g2_t;
var h_m : g2_t;
var sigma : g2_t;
H_m <- hash_to_g2 msg;
sigma <- g2_scalar_mul sk H_m;
h_m <- hash_to_g2 msg;
sigma <- g2_scalar_mul sk h_m;
return encode_g2 sigma;
}
}.
@@ -212,11 +212,11 @@ module BLSThresholdRef : BLS_Threshold = {
var weighted_sum : g2_t;
var lam : scalar_t;
var sigma_i : g2_t;
var Q_size : int;
var q_size : int;
weighted_sum <- g2_scalar_mul scalar_zero g2_gen; (* identity *)
Q_size <- size Q;
q_size <- size Q;
i <- 0;
while (i < Q_size) {
while (i < q_size) {
lam <- lagrange Q i;
(* sigma_i corresponds to position i in Q; resolved via shares. *)
sigma_i <- witness;
@@ -242,16 +242,16 @@ declare module S <: BLSSigner.
declare axiom bls_threshold_dispatches_to_bls
(Q : int list)
(shares : share_t list)
(secret_shares : share_t list)
(sig_shares : (int * sig_share_t) list)
(msg : message_t) :
uniq Q =>
size Q = size shares =>
size Q = size secret_shares =>
(* The threshold protocol's aggregate output equals single-party *)
(* BLS.Sign on the Lagrange-reconstructed secret. *)
equiv [ T.aggregate ~ S.sign :
Q{1} = Q /\ shares{1} = sig_shares /\ msg{1} = msg
/\ sk{2} = reconstruct Q shares
/\ sk{2} = reconstruct Q secret_shares
/\ msg{2} = msg
==>
={res} ].
@@ -277,8 +277,9 @@ proof.
have hrec : master_secret =
reconstruct Q (List.map (poly_eval master_secret) Q).
- by rewrite (lagrange_inverse_eval master_secret Q).
rewrite hrec.
apply (bls_threshold_dispatches_to_bls Q
(List.map (poly_eval master_secret) Q) sig_shares msg uQ _) => //=.
(List.map (poly_eval master_secret) Q) sig_shares msg uQ _).
by rewrite size_map.
qed.
protocols/bls/proofs/easycrypt/BLS_Threshold_N4.ec
+3 -5
View File
@@ -99,11 +99,9 @@ proof.
move=> Q shares uQ szQ szs.
rewrite reconstruct_linear_N4 //=; first by rewrite fresh_sharing_size.
rewrite (shamir_correct_N4 Q scalar_zero uQ szQ).
rewrite derive_pk_homomorphism derive_pk_zero.
(* Same one-line group-identity admit as FROST_N4 / CGGMP21_N4 / *)
(* Pulsar_N4. Closure: Crypto.BLS.Threshold.group_pk_identity Lean *)
(* lemma. *)
admit.
(* reconstruct Q shares + 0 = reconstruct Q shares by the scalar *)
(* right-identity, so both sides are derive_pk of the same scalar. *)
by rewrite scalar_add_zeroR_N4.
qed.
(* -------------------------------------------------------------------- *)
protocols/cmp/proofs/easycrypt/CGGMP21_N1.ec
+9 -8
View File
@@ -162,7 +162,7 @@ op paillier_dec : paillier_sk_t -> int -> int.
(* enc(pk, m1, r1) * enc(pk, m2, r2) = enc(pk, m1+m2 mod N, r1*r2) *)
axiom paillier_additive_homomorphism :
forall (pk : paillier_pk_t) (m1 m2 r1 r2 : int),
True. (* Stated mathematically in CGGMP21_Paillier.ec *)
true. (* Stated mathematically in CGGMP21_Paillier.ec *)
(* -------------------------------------------------------------------- *)
(* Single-party ECDSA reference module *)
@@ -179,10 +179,10 @@ module type ECDSASigner = {
module ECDSARef : ECDSASigner = {
proc sign(sk : share_t, msg_hash : message_hash_t, k : scalar_t)
: signature_t = {
var R : point_t;
var rpt : point_t;
var r, s, k_inv, m : scalar_t;
R <- scalar_mul k group_g;
r <- point_x R;
rpt <- scalar_mul k group_g;
r <- point_x rpt;
k_inv <- scalar_inv k;
m <- h_msg msg_hash;
s <- scalar_mul_s k_inv (scalar_add m (scalar_mul_s r sk));
@@ -238,17 +238,17 @@ declare module S <: ECDSASigner.
declare axiom cggmp21_dispatches_to_ecdsa
(sess : session_t)
(Q : int list)
(shares : share_t list)
(key_shares : share_t list)
(presig : presignature_t)
(k_recon : scalar_t)
(msg_hash : message_hash_t)
(s_shares : (int * scalar_t) list) :
uniq Q =>
size Q = size shares =>
size Q = size key_shares =>
equiv [ T.sign_online ~ S.sign :
sess{1} = sess /\ presig{1} = presig
/\ msg_hash{1} = msg_hash /\ shares{1} = s_shares
/\ sk{2} = reconstruct Q shares
/\ sk{2} = reconstruct Q key_shares
/\ k{2} = k_recon /\ msg_hash{2} = msg_hash
==>
={res} ].
@@ -277,9 +277,10 @@ proof.
have hrec : master_secret =
reconstruct Q (List.map (poly_eval master_secret) Q).
- by rewrite (lagrange_inverse_eval master_secret Q).
rewrite hrec.
apply (cggmp21_dispatches_to_ecdsa sess Q
(List.map (poly_eval master_secret) Q) presig k_recon
msg_hash s_shares uQ _) => //=.
msg_hash s_shares uQ _).
by rewrite size_map.
qed.
protocols/cmp/proofs/easycrypt/CGGMP21_N4.ec
+8 -3
View File
@@ -65,6 +65,12 @@ axiom derive_pk_homomorphism :
axiom derive_pk_zero :
derive_pk scalar_zero = group_zero_pk.
(* BRIDGE: group_zero_pk is the identity of the secp256k1 point group *)
(* (the point at infinity); right-identity is an AddGroup instance fact *)
(* (Mathlib `add_zero`). Same bridge as FROST_N4 / Pulsar_N4. *)
axiom group_pk_add_zeroR :
forall (p : group_pk_t), group_pk_add p group_zero_pk = p.
(* CGGMP21 refresh module type. *)
module type CGGMP21_Refresh = {
proc refresh(committee : committee_t,
@@ -93,9 +99,8 @@ proof.
rewrite reconstruct_linear_N4 //=; first by rewrite fresh_sharing_size.
rewrite (shamir_correct_N4 Q scalar_zero uQ szQ).
rewrite derive_pk_homomorphism derive_pk_zero.
(* group_pk_add P group_zero_pk = P (group identity). Same admit as *)
(* FROST_N4 — one-line Lean bridge. *)
admit.
(* group_pk_add p group_zero_pk = p (group right-identity). *)
by rewrite group_pk_add_zeroR.
qed.
(* -------------------------------------------------------------------- *)
protocols/cmp/proofs/easycrypt/CGGMP21_Paillier.ec
+10 -10
View File
@@ -32,7 +32,7 @@ require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.
type paillier_pk_t. (* Public key (modulus N, generator g = N+1). *)
type paillier_sk_t. (* Secret key (factors (p, q) with N = pq). *)
type paillier_ct_t. (* Ciphertext (element of Z_{N^2}^*). *)
type paillier_ct_t. (* Ciphertext (element of the unit group mod N^2). *)
(* Operations. *)
op paillier_N : paillier_pk_t -> int. (* Extract the modulus. *)
@@ -50,7 +50,7 @@ op paillier_exp : paillier_ct_t -> int -> paillier_ct_t.
(* `pkg/paillier`; here we axiomatize the result. *)
axiom paillier_modulus_biprime :
forall (pk : paillier_pk_t),
True. (* Stated as the biprime-test soundness in CCS '21 App C. *)
true. (* Stated as the biprime-test soundness in CCS '21 App C. *)
(* -------------------------------------------------------------------- *)
(* Additive homomorphism (the load-bearing identity) *)
@@ -83,7 +83,7 @@ axiom paillier_scalar_homomorphism :
(* Decryption inverts encryption: dec(sk, enc(pk, m, r)) = m mod N. *)
axiom paillier_correctness :
forall (sk : paillier_sk_t) (pk : paillier_pk_t) (m r : int),
True. (* dec sk (enc pk m r) = m mod N (when sk and pk are paired)*)
true. (* dec sk (enc pk m r) = m mod N (when sk and pk are paired)*)
(* -------------------------------------------------------------------- *)
(* MtA correctness (CCS '21 §3.2) *)
@@ -99,13 +99,13 @@ axiom paillier_correctness :
axiom mta_correctness :
forall (pk_A : paillier_pk_t)
(sk_A : paillier_sk_t)
(a b beta : int)
(r_a r_beta : int),
let C_A = paillier_enc pk_A a r_a in
let C_B = paillier_mul (paillier_exp C_A b)
(paillier_enc pk_A (-beta) r_beta) in
let alpha = paillier_dec sk_A C_B in
(alpha + beta) %% paillier_N pk_A = (a * b) %% paillier_N pk_A.
(a b bta : int)
(r_a r_bta : int),
let c_A = paillier_enc pk_A a r_a in
let c_B = paillier_mul (paillier_exp c_A b)
(paillier_enc pk_A (-bta) r_bta) in
let alpha = paillier_dec sk_A c_B in
(alpha + bta) %% paillier_N pk_A = (a * b) %% paillier_N pk_A.
(* -------------------------------------------------------------------- *)
(* End of CGGMP21_Paillier.ec *)
protocols/cmp/proofs/easycrypt/CGGMP21_ZK.ec
+3 -3
View File
@@ -59,20 +59,20 @@ declare module Z <: ZKProtocol.
(* (statement, witness) pairs. *)
declare axiom zk_completeness :
forall (stmt : statement_t) (witn : witness_t),
True. (* equiv [ Z.prove ~~~ Z.verify(stmt,_): res = true ] *)
true. (* equiv [ Z.prove ~~~ Z.verify(stmt,_): res = true ] *)
(* Soundness: any prover P that produces verifying transcripts on *)
(* statements without witnesses succeeds with prob <= 2^-statistical. *)
declare axiom zk_soundness :
forall (stmt : statement_t),
True. (* Probabilistic statement; concrete form lives in CGGMP21.*)
true. (* Probabilistic statement; concrete form lives in CGGMP21.*)
(* Zero-knowledge: simulator's transcript distribution is *)
(* statistically-indistinguishable from the real transcript *)
(* distribution under any (stmt, witn). *)
declare axiom zk_zero_knowledge :
forall (stmt : statement_t) (witn : witness_t),
True. (* equiv [ Z.prove ~ Z.simulate : ={stmt} ==> ={res} ] *)
true. (* equiv [ Z.prove ~ Z.simulate : ={stmt} ==> ={res} ] *)
end section ZKSecurity.
protocols/frost/proofs/easycrypt/FROST_N1.ec
+11 -4
View File
@@ -139,6 +139,12 @@ op h_binding : byte_seq -> scalar_t.
op h_challenge : byte_seq -> scalar_t.
op h_nonce : byte_seq -> scalar_t.
(* Generic (ciphersuite-agnostic) Schnorr signature encoder: maps the *)
(* aggregated commitment R and response z to the signature byte string. *)
(* The ciphersuite layer (FROST_Ciphersuite_*.ec) and the Combine *)
(* refinement (FROST_N1_Refinement.ec) both pin / consume this operator. *)
op encode_signature : point_t -> scalar_t -> signature_t.
(* -------------------------------------------------------------------- *)
(* Shamir / Lagrange algebraic kernel *)
(* -------------------------------------------------------------------- *)
@@ -275,20 +281,20 @@ declare module S <: SchnorrSigner.
declare axiom frost_combine_dispatches_to_schnorr
(sess : session_t)
(Q : int list)
(shares : share_t list)
(key_shares : share_t list)
(commits : commit_list_t)
(responses : (int * share_response_t) list)
(group_pk : group_pk_t)
(msg : message_t) :
uniq Q =>
size Q = size shares =>
size Q = size key_shares =>
(* The threshold protocol's combine output equals single-party *)
(* Schnorr Sign on the Lagrange-reconstructed secret. *)
equiv [ T.combine ~ S.sign :
sess{1} = sess /\ commits{1} = commits
/\ shares{1} = responses /\ group_pk{1} = group_pk
/\ msg{1} = msg
/\ sk{2} = reconstruct Q shares
/\ sk{2} = reconstruct Q key_shares
/\ msg{2} = msg
==>
={res} ].
@@ -325,9 +331,10 @@ proof.
have hrec : master_secret =
reconstruct Q (List.map (poly_eval master_secret) Q).
- by rewrite (lagrange_inverse_eval master_secret Q).
rewrite hrec.
apply (frost_combine_dispatches_to_schnorr sess Q
(List.map (poly_eval master_secret) Q) commits responses
group_pk msg uQ _) => //=.
group_pk msg uQ _).
by rewrite size_map.
qed.
protocols/frost/proofs/easycrypt/FROST_N1_Refinement.ec
+12 -12
View File
@@ -40,14 +40,14 @@ module FROST_Ref : FROST_Threshold = {
proc round1(sess : session_t, share : share_t, my_idx : int)
: commit_pair_t * nonce_pair_t = {
var d, e : scalar_t;
var D, E : point_t;
var dd, ee : point_t;
(* In production the nonces are sampled fresh per Komlo-Goldberg *)
(* Fig. 3, Round 1. Here the abstract sampling is witnessed. *)
d <- witness;
e <- witness;
D <- scalar_mul d group_g;
E <- scalar_mul e group_g;
return ((D, E), (d, e));
dd <- scalar_mul d group_g;
ee <- scalar_mul e group_g;
return ((dd, ee), (d, e));
}
proc round2(sess : session_t, share : share_t, my_idx : int,
@@ -124,12 +124,12 @@ module FROST_Round2_Spec = {
nonces : nonce_pair_t, commits : commit_list_t,
msg : message_t) : share_response_t = {
var rho, c, lam, z : scalar_t;
var R : point_t;
var rpt : point_t;
rho <- compute_binding_factor sess commits msg my_idx;
R <- aggregate_R commits msg sess;
rpt <- aggregate_R commits msg sess;
(* Group PK is committed in the session; threshold reconstruction *)
(* is implicit in the session-binding step. *)
c <- compute_challenge sess R witness msg;
c <- compute_challenge sess rpt witness msg;
lam <- lagrange (map fst commits) my_idx;
z <- scalar_add
(scalar_add nonces.`1
@@ -155,17 +155,17 @@ axiom round2_refinement_axiom :
(* `FROST_N1.ec` and lives in the ciphersuite layer. *)
(* -------------------------------------------------------------------- *)
op encode_signature : point_t -> scalar_t -> signature_t.
(* encode_signature is declared in the shared base FROST_N1.ec so that *)
(* the ciphersuite layer can also pin it; consumed here unchanged. *)
module FROST_Combine_Spec = {
proc combine(sess : session_t, commits : commit_list_t,
shares : (int * share_response_t) list,
group_pk : group_pk_t, msg : message_t) : signature_t = {
var R : point_t;
var rpt : point_t;
var z : scalar_t;
R <- aggregate_R commits msg sess;
rpt <- aggregate_R commits msg sess;
z <- foldr scalar_add scalar_zero (map snd shares);
return encode_signature R z;
return encode_signature rpt z;
}
}.
protocols/frost/proofs/easycrypt/FROST_N4.ec
+8 -3
View File
@@ -87,6 +87,12 @@ axiom derive_pk_homomorphism :
axiom derive_pk_zero :
derive_pk scalar_zero = group_zero_pk.
(* BRIDGE: group_zero_pk is the identity of the curve point group *)
(* (the point at infinity); right-identity is an AddGroup instance fact *)
(* (Mathlib `add_zero`). Same bridge as Pulsar_N4 / CGGMP21_N4. *)
axiom group_pk_add_zeroR :
forall (p : group_pk_t), group_pk_add p group_zero_pk = p.
(* ===================================================================
FROST Refresh / Proactive-rotation: public-key preservation theorem.
=================================================================== *)
@@ -120,9 +126,8 @@ proof.
rewrite reconstruct_linear_N4 //=; first by rewrite fresh_sharing_size.
rewrite (shamir_correct_N4 Q scalar_zero uQ szQ).
rewrite derive_pk_homomorphism derive_pk_zero.
(* group_pk_add P group_zero_pk = P (group identity). *)
(* Stated as a one-line algebraic identity inline. *)
admit. (* Lean bridge: derive_pk_group_identity (one line, future). *)
(* group_pk_add p group_zero_pk = p (group right-identity). *)
by rewrite group_pk_add_zeroR.
qed.
(* -------------------------------------------------------------------- *)