mirror of
https://github.com/luxfi/threshold.git
synced 2026-10-30 15:15:53 +00:00
zooqueenandHanzo Dev
63d0840958
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 <[email protected]>
113 lines
6.3 KiB
Plaintext
113 lines
6.3 KiB
Plaintext
(* -------------------------------------------------------------------- *)
|
|
(* CGGMP21 -- Paillier MtA layer *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* STATUS: SHELL. The Paillier additive homomorphism is a *)
|
|
(* well-established result; this file pins the EC statement of what *)
|
|
(* the threshold layer relies on and bridges to Lean. *)
|
|
(* *)
|
|
(* Reference: Paillier, P. *Public-Key Cryptosystems Based on Composite *)
|
|
(* Degree Residuosity Classes.* Eurocrypt 1999. *)
|
|
(* *)
|
|
(* CCS '21 §3.2 — Multiplicative-to-Additive (MtA) conversion using *)
|
|
(* Paillier: *)
|
|
(* - Party A has secret a, encrypts under their own Paillier N_A: *)
|
|
(* C_A = enc(N_A, a, r_A) *)
|
|
(* - Party B has secret b, computes (additively-homomorphically): *)
|
|
(* C_B = C_A^b * enc(N_A, -beta, r_B) = enc(N_A, ab - beta, ...) *)
|
|
(* - Party A decrypts C_B to get alpha = ab - beta (mod N_A). *)
|
|
(* - Now alpha + beta = ab (mod N_A), with each party knowing only *)
|
|
(* their additive share. *)
|
|
(* *)
|
|
(* The CCS '21 protocol wraps each MtA in two-sided ZK proofs: *)
|
|
(* - Range proof on a (to prevent N_A-overflow attacks). *)
|
|
(* - Knowledge proof on b (the "MtA in zero knowledge"). *)
|
|
(* See CGGMP21_ZK.ec for the ZK obligation surface. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Paillier types *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
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 the unit group mod N^2). *)
|
|
|
|
(* Operations. *)
|
|
op paillier_N : paillier_pk_t -> int. (* Extract the modulus. *)
|
|
op paillier_enc : paillier_pk_t -> int -> int -> paillier_ct_t.
|
|
op paillier_dec : paillier_sk_t -> paillier_ct_t -> int.
|
|
op paillier_mul : paillier_ct_t -> paillier_ct_t -> paillier_ct_t.
|
|
op paillier_exp : paillier_ct_t -> int -> paillier_ct_t.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Paillier well-formedness axioms *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
(* The modulus is a biprime: N = pq with p, q safe primes. *)
|
|
(* Biprime verification per CCS '21 Appendix C is implemented in *)
|
|
(* `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. *)
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Additive homomorphism (the load-bearing identity) *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
(* enc(pk, a, r_a) * enc(pk, b, r_b) = enc(pk, a+b mod N, r_a*r_b mod N) *)
|
|
(* BRIDGE: Lean `Crypto.CGGMP21.Paillier.add_homomorphism` *)
|
|
(* (`~/work/lux/proofs/lean/Crypto/CGGMP21.lean:200`). *)
|
|
axiom paillier_add_homomorphism :
|
|
forall (pk : paillier_pk_t) (a b r_a r_b : int),
|
|
paillier_mul (paillier_enc pk a r_a) (paillier_enc pk b r_b) =
|
|
paillier_enc pk
|
|
((a + b) %% paillier_N pk)
|
|
((r_a * r_b) %% paillier_N pk).
|
|
|
|
(* enc(pk, a, r)^b = enc(pk, a*b mod N, r^b mod N). *)
|
|
(* This is the "scalar multiplication" derived from the additive *)
|
|
(* homomorphism. Used in MtA Round 2. *)
|
|
(* BRIDGE: Lean `Crypto.CGGMP21.Paillier.mul_homomorphism` *)
|
|
(* (`~/work/lux/proofs/lean/Crypto/CGGMP21.lean:212`). *)
|
|
axiom paillier_scalar_homomorphism :
|
|
forall (pk : paillier_pk_t) (a b r : int),
|
|
paillier_exp (paillier_enc pk a r) b =
|
|
paillier_enc pk
|
|
((a * b) %% paillier_N pk)
|
|
(((r * r) %% paillier_N pk) * b %% paillier_N pk).
|
|
(* Concrete r-exponent form is library-specific; abstracted *)
|
|
(* here as the mathematical identity. *)
|
|
|
|
(* 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)*)
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* MtA correctness (CCS '21 §3.2) *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
(* MtA: party A holds a, party B holds b. After the exchange: *)
|
|
(* - A learns alpha such that alpha = a*b - beta (mod N_A). *)
|
|
(* - B learns beta (which they chose). *)
|
|
(* - alpha + beta = a*b (mod N_A). *)
|
|
(* When N_A >> n (Paillier modulus much larger than ECDSA group order),*)
|
|
(* and after the range proof, alpha + beta = a*b also holds mod n. *)
|
|
|
|
axiom mta_correctness :
|
|
forall (pk_A : paillier_pk_t)
|
|
(sk_A : paillier_sk_t)
|
|
(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 *)
|
|
(* -------------------------------------------------------------------- *)
|