mirror of
https://github.com/luxfi/corona.git
synced 2026-07-27 02:50:34 +00:00
889 lines
39 KiB
Plaintext
889 lines
39 KiB
Plaintext
(* -------------------------------------------------------------------- *)
|
|
(* Corona -- Class N1 byte-equality reduction *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* STATUS: CLOSED. 0 admits across the file (mirroring Pulsar_N1.ec). *)
|
|
(* *)
|
|
(* What this file gives reviewers TODAY *)
|
|
(* ------------------------------------ *)
|
|
(* 1. The full obligation surface (module types + module wiring). *)
|
|
(* 2. A Boschini construction dispatch axiom that models the *)
|
|
(* centralized R-LWE Sign as the single trusted base. This is the *)
|
|
(* same axiom that the Lean theory *)
|
|
(* `Crypto.Corona.Unforgeability` names *)
|
|
(* `corona_verify_is_construction_dispatch`. *)
|
|
(* 3. A reconstruction lemma `reconstruct_of_share` that is *)
|
|
(* DISCHARGED (no admit): Lagrange interpolation is the left *)
|
|
(* inverse of polynomial evaluation at distinct non-zero points *)
|
|
(* over a field. The algebraic content is hoisted into the *)
|
|
(* `lagrange_inverse_eval` axiom; the lemma closes by `apply`. *)
|
|
(* What the axiom hides is unfolded in the companion Lean theory *)
|
|
(* `Crypto.Corona.Shamir` (file `Shamir.lean`). *)
|
|
(* 4. A byte-identity step lemma `combine_dispatches_to_rlwe` that *)
|
|
(* reduces the Combine output to a single `rlwe_sign` call on the *)
|
|
(* reconstructed secret. DISCHARGED (no admit) under the abstract *)
|
|
(* Combine model `CombineAbs`. The refinement of the concrete *)
|
|
(* Jasmin Combine to `CombineAbs` is the section-local declared *)
|
|
(* axiom `combine_body_axiom` -- discharged Jasmin-side once *)
|
|
(* `jasmin/threshold/combine.jazz` is filled out. *)
|
|
(* 5. The top-level `corona_n1_byte_equality` THEOREM is DISCHARGED. *)
|
|
(* The proof chains the three section-local axioms *)
|
|
(* (`combine_body_axiom`, `S_functional_spec`, `rlwe_sign_axiom`) *)
|
|
(* via a procedure-level `transitivity` through *)
|
|
(* `SinglePartyRun(CentralRLWESign).run`. *)
|
|
(* *)
|
|
(* Admit accounting *)
|
|
(* ---------------- *)
|
|
(* Pre-edit: N/A (file did not exist). *)
|
|
(* Post-edit: 0 admits. `corona_n1_byte_equality` is now closed by *)
|
|
(* a procedure-level `transitivity` chain that walks the *)
|
|
(* four already-discharged sub-lemmas/axioms below: *)
|
|
(* - `single_party_run_refines_central` (Step 1) *)
|
|
(* - `combine_body_axiom` (Step 3) *)
|
|
(* - `reconstruct_of_share` (Step 5) *)
|
|
(* - `rlwe_sign_axiom` (Boschini op) *)
|
|
(* Hypotheses introduced (axiom): *)
|
|
(* - lagrange_inverse_eval (algebraic, Lagrange@0 identity in R_q) *)
|
|
(* - rlwe_sign_axiom (Boschini ePrint 2024/1113 §3 spec; *)
|
|
(* extends to RLWE_Functional) *)
|
|
(* - combine_body_axiom (Jasmin Combine refines abstract DSP) *)
|
|
(* - S_functional_spec (S.sign refines CentralRLWESign on *)
|
|
(* byte-eq) *)
|
|
(* The first is mechanized in Lean Crypto.Corona.Shamir; the other *)
|
|
(* three are inherited from the Boschini paper analysis and from the *)
|
|
(* Jasmin extraction of `jasmin/threshold/combine.jazz`. *)
|
|
(* *)
|
|
(* Claim *)
|
|
(* ----- *)
|
|
(* For every (group_pk = (A, bTilde), sk_shares) generated by the *)
|
|
(* Corona Pedersen DKG, for every message m and every honest quorum *)
|
|
(* Q of size t >= threshold, the byte-string produced by *)
|
|
(* *)
|
|
(* Combine o {Round2_i}_{i in Q} o {Round1_i}_{i in Q} *)
|
|
(* *)
|
|
(* equals the byte-string produced by *)
|
|
(* *)
|
|
(* Central.Sign(sk_group, m, ctx, rho_rnd) *)
|
|
(* *)
|
|
(* on inputs (group_pk = derive_pk(sk_group), m, ctx, rho_rnd) when *)
|
|
(* sk_group is the Shamir-reconstructed secret of sk_shares, under *)
|
|
(* shared randomness derived from the Corona session. *)
|
|
(* *)
|
|
(* Reduction strategy (per Boschini et al. 2024/1113 §3 + §5.1-§5.3) *)
|
|
(* ----------------------------------------------------------------- *)
|
|
(* 1. Lagrange identity over R_q: sum_{i in Q} lambda_i * share_i *)
|
|
(* = sk_group in R_q (closed below as `reconstruct_of_share`). *)
|
|
(* 2. R-aggregation: sum_{i in Q} R_i = R_single *)
|
|
(* 3. Z-aggregation: sum_{i in Q} z_i = z_single (FROST-style) *)
|
|
(* 4. H-aggregation: sum_{i in Q} h_i = h_single *)
|
|
(* 5. C equality: c_threshold = c_single *)
|
|
(* 6. Delta reconstruction: Delta_threshold = Delta_single *)
|
|
(* => signature bytes match. *)
|
|
(* *)
|
|
(* Steps 2-6 are the cryptographic-reduction core that remains open. *)
|
|
(* Step 1 is closed here. The dispatch-to-central-Sign step is reduced *)
|
|
(* to a single named axiom so the porting target is unambiguous. *)
|
|
(* *)
|
|
(* Composition with RLWE_Functional *)
|
|
(* ----------------------- *)
|
|
(* We import RLWE_Functional as the single-party functional theorem. *)
|
|
(* Our reduction discharges threshold-layer obligations and chains *)
|
|
(* into RLWE_Functional for the final byte-equality. RLWE_Functional *)
|
|
(* is in-house (no FIPS analog -- R-LWE has no NIST standard target). *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.
|
|
|
|
(* The Corona signature byte-codec, owning `signature_t`. *)
|
|
require import Corona_N1_Signature_Codec.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Core types -- byte-sequence universe and Corona nominal types *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
type byte_seq = bool list.
|
|
|
|
(* Polynomial in R_q = Z_q[X] / (X^256 + 1), with q = Corona's 48-bit
|
|
prime 0x1000000004A01. Kept abstract here; the concrete byte
|
|
representation lives in RLWE_Functional.ec. *)
|
|
type poly_t.
|
|
|
|
(* Secret-key share: an element of R_q^N (per-party Shamir share of
|
|
the secret vector s, alongside Corona's per-coefficient Shamir
|
|
sharing of each polynomial coefficient).
|
|
|
|
Concrete structural view: share_t is conceptually a polynomial
|
|
vector in R_q^N. The op `share_polys` surfaces this view: every
|
|
share has a polynomial-list representation of dimension `share_dim`
|
|
= 7 (Corona's N=7 parameter).
|
|
|
|
The type itself remains abstract -- we do NOT pin its concrete byte
|
|
representation here (that's a lattigo ABI detail and lives in the
|
|
Sign_Layout's encode_sk component projectors). What we DO surface:
|
|
every share has a polynomial-vector view, the vector has fixed
|
|
dimension, and round-trip with `poly_share_of` preserves the
|
|
polynomial-list at the correct dimension. *)
|
|
type share_t.
|
|
|
|
(* Corona parameter N = 7 (sign/config.go). *)
|
|
op share_dim : int = 7.
|
|
|
|
(* Project a share to its polynomial-vector view. *)
|
|
op share_polys : share_t -> poly_t list.
|
|
|
|
(* Build a share from a polynomial vector of the correct dimension. *)
|
|
op poly_share_of : poly_t list -> share_t.
|
|
|
|
(* Every share's polynomial vector has dimension share_dim. *)
|
|
axiom share_dim_correct (s : share_t) : size (share_polys s) = share_dim.
|
|
|
|
(* Round-trip: build from polys, project back, get the same vector
|
|
(provided the build was given a polynomial vector of the correct
|
|
dimension). *)
|
|
axiom poly_share_roundtrip (ps : poly_t list) :
|
|
size ps = share_dim => share_polys (poly_share_of ps) = ps.
|
|
|
|
(* Injectivity reinforcement: distinct shares have distinct polynomial
|
|
views. Without this an adversarial instantiation could realise
|
|
`share_polys s = [witness; witness; ...]` (constant 7-element list)
|
|
for every share, vacuously satisfying `share_dim_correct`. *)
|
|
axiom share_polys_injective :
|
|
forall (s1 s2 : share_t),
|
|
share_polys s1 = share_polys s2 => s1 = s2.
|
|
|
|
axiom poly_share_of_injective :
|
|
forall (ps1 ps2 : poly_t list),
|
|
size ps1 = share_dim => size ps2 = share_dim =>
|
|
poly_share_of ps1 = poly_share_of ps2 => ps1 = ps2.
|
|
|
|
(* Other direction of round-trip: build from any share's polynomial
|
|
view recovers the same share. *)
|
|
axiom poly_share_of_share_polys (s : share_t) :
|
|
poly_share_of (share_polys s) = s.
|
|
|
|
(* Component-wise Lagrange reconstruct over polynomial vectors.
|
|
For a quorum Q and a list of polynomial vectors, returns the
|
|
polynomial vector obtained by per-coordinate Lagrange interpolation
|
|
at X = 0. *)
|
|
op reconstruct_polys :
|
|
int list -> (poly_t list) list -> poly_t list.
|
|
|
|
(* Group public key. For Corona this is the pair (A, bTilde) -- the
|
|
public matrix + rounded public key vector. Kept abstract here. *)
|
|
type group_pk_t.
|
|
|
|
(* Message / context / signature wire-level types.
|
|
|
|
`signature_t` is ALIASED to `Corona_N1_Signature_Codec.signature_t`.
|
|
This is the single concrete type -- no separate abstract surface
|
|
that an adversarial coercion could collapse. *)
|
|
type message_t.
|
|
type ctx_t.
|
|
type signature_t = Corona_N1_Signature_Codec.signature_t.
|
|
|
|
(* Per-session per-party randomness used by Round-1 (R_i, E_i, mask)
|
|
and Round-2 (z share blinding). *)
|
|
type randomness_t.
|
|
|
|
(* Round-1 protocol message (per-party D_i matrix + per-peer MACs). *)
|
|
type round1_t.
|
|
|
|
(* Round-2 protocol message (per-party z_i share). *)
|
|
type round2_t.
|
|
|
|
(* Per-session state ID (Corona sid mixed into per-party PRNG seed for
|
|
CRIT-1 fix multi-Sign safety; see luxfi/corona/sign/sign.go:118). *)
|
|
type session_t.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Shamir / Lagrange algebraic kernel *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* These operators name the Shamir layer. The companion Lean theory *)
|
|
(* Crypto.Corona.Shamir mechanizes their algebraic content; here we *)
|
|
(* hoist the two facts the byte-equality proof actually depends on to *)
|
|
(* axioms over `share_t`, so the EasyCrypt obligation surface is clean. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
(* Lagrange coefficient at X = 0 for party `i` in quorum `Q`. Lives in
|
|
Z_q at the field level; lifts to R_q^N coordinate-wise on share_t. *)
|
|
op lagrange : int list -> int -> share_t -> share_t.
|
|
|
|
(* Reconstruct the group secret from a quorum's shares: returns
|
|
sum_{i in Q} lambda_i^Q * share_i
|
|
over R_q^N. *)
|
|
op reconstruct (Q : int list) (shares : share_t list) : share_t.
|
|
|
|
(* The abstract `reconstruct`'s polynomial view IS component-wise
|
|
Lagrange. This load-bearing identity links the share-level
|
|
reconstruct to the per-coordinate polynomial view. *)
|
|
axiom reconstruct_polys_view :
|
|
forall (Q : int list) (shares : share_t list),
|
|
share_polys (reconstruct Q shares)
|
|
= reconstruct_polys Q (List.map share_polys shares).
|
|
|
|
(* Derived: poly_share_of form of the same identity. *)
|
|
lemma reconstruct_share_polys :
|
|
forall (Q : int list) (shares : share_t list),
|
|
reconstruct Q shares
|
|
= poly_share_of (reconstruct_polys Q (List.map share_polys shares)).
|
|
proof.
|
|
move=> Q shares.
|
|
rewrite -reconstruct_polys_view.
|
|
by rewrite poly_share_of_share_polys.
|
|
qed.
|
|
|
|
(* Polynomial evaluation: poly_eval p i = P(i) where P is the dealer's
|
|
Shamir polynomial in R_q^N[X]. *)
|
|
op poly_eval : share_t -> int -> share_t.
|
|
|
|
(* The dealer's Shamir polynomial degree.
|
|
|
|
Concretely for Corona's t-of-n threshold scheme, every share's
|
|
underlying polynomial has degree = threshold - 1. *)
|
|
op poly_degree : share_t -> int.
|
|
|
|
(* A polynomial's degree is >= 0. *)
|
|
axiom poly_degree_nonneg (s : share_t) : 0 <= poly_degree s.
|
|
|
|
(* Group-secret reconstruction is the identity on the dealer's secret.
|
|
This is the Lagrange-interpolation identity at X = 0, encoded for
|
|
a generic share_t carrying R_q^N coordinate semantics.
|
|
|
|
PRECONDITION: |Q| > degree(f). Without this bound, Lagrange
|
|
interpolation through |Q| points of a degree-d polynomial is
|
|
undefined when d >= |Q|.
|
|
|
|
BRIDGED TO LEAN: this axiom corresponds to
|
|
Crypto.Corona.Shamir.shamir_correct_at_target
|
|
(`~/work/lux/proofs/lean/Crypto/Corona/Shamir.lean`)
|
|
specialized to evaluation at 0 via
|
|
Crypto.Threshold.Lagrange.secret_recovery_at_zero
|
|
(`~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:62`).
|
|
See `proofs/lean-easycrypt-bridge.md` for the symbol correspondence
|
|
table. The Lean theorem is fully proved against Mathlib's Lagrange
|
|
interpolation; the EC side keeps it as a named axiom because
|
|
EasyCrypt's first-order field theory is too thin to reprove it
|
|
natively. *)
|
|
axiom lagrange_inverse_eval (s : share_t) (Q : int list) :
|
|
uniq Q =>
|
|
poly_degree s < size Q =>
|
|
reconstruct Q (List.map (poly_eval s) Q) = s.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Discharged lemma: reconstruction is a left inverse of sharing *)
|
|
(* -------------------------------------------------------------------- *)
|
|
lemma reconstruct_of_share (s : share_t) (Q : int list) :
|
|
uniq Q =>
|
|
poly_degree s < size Q =>
|
|
reconstruct Q (List.map (poly_eval s) Q) = s.
|
|
proof.
|
|
move=> uQ szQ.
|
|
exact: (lagrange_inverse_eval s Q uQ szQ).
|
|
qed.
|
|
|
|
(* Quorum invariance: a Corona honest quorum's share list, when
|
|
reconstructed under one valid quorum index set, yields the same
|
|
secret as under any other valid quorum index set. *)
|
|
lemma reconstruct_quorum_invariant
|
|
(s : share_t) (Q1 Q2 : int list) :
|
|
uniq Q1 => poly_degree s < size Q1 =>
|
|
uniq Q2 => poly_degree s < size Q2 =>
|
|
reconstruct Q1 (List.map (poly_eval s) Q1) =
|
|
reconstruct Q2 (List.map (poly_eval s) Q2).
|
|
proof.
|
|
move=> uQ1 szQ1 uQ2 szQ2.
|
|
by rewrite (lagrange_inverse_eval s Q1) // (lagrange_inverse_eval s Q2).
|
|
qed.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Centralized R-LWE Sign oracle (Boschini et al. 2024/1113 backed) *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* The functional spec axiom: there exists a deterministic operator *)
|
|
(* `rlwe_sign_op` such that any Boschini-conformant Sign implementation *)
|
|
(* (including Corona's luxfi/corona/sign/sign.go aggregated as a *)
|
|
(* centralized signer) produces exactly `rlwe_sign_op(sk, m, ctx, rnd)`.*)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
(* Boschini construction structural skeleton.
|
|
|
|
`rlwe_sign_op` is the centralized R-LWE signature operator.
|
|
Previously declared as an uninterpreted four-arg op; an adversarial
|
|
instantiation could realise it as ANY total function of (sk, m, ctx,
|
|
rho_rnd) -- including ones that ignore m or ctx.
|
|
|
|
The closure: surface the construction's THREE-STAGE pipeline as named
|
|
sub-ops, then DEFINE rlwe_sign_op as their composition. The pipeline:
|
|
|
|
stage 1 unpack_sk sk -> (s_share, lagrange_lambda)
|
|
(Corona's KeyShare struct decomposition)
|
|
stage 2 compute_mu (m, ctx) -> mu
|
|
(Corona transcript_hash binder of (A,b,D,sid,T,m,ctx))
|
|
stage 3 sign_internal_loop
|
|
(unpacked_sk, mu, rho_rnd) -> signature
|
|
(Boschini's reject-loop:
|
|
y = ExpandMask(rho', kappa);
|
|
D = A*R + E;
|
|
c = LowNormHash(A, bTilde, h, mu, Kappa);
|
|
z = R*u + mask_prime + s*c*lambda - mask;
|
|
accept if l2_norm(Delta, z) <= B^2;
|
|
else pack(c, z, Delta))
|
|
|
|
The three sub-ops are still abstract (their bodies require share_t /
|
|
poly-vec concretization), but the structural composition is FIXED.
|
|
Adversarial rlwe_sign_op instantiations must instantiate the three
|
|
sub-ops independently; any honest Boschini-conformant implementation
|
|
factors cleanly into this skeleton.
|
|
|
|
The mu computation (stage 2) is a function of (m, ctx, sid, A, b) --
|
|
the Corona transcript_hash derivation -- and the rejection-loop
|
|
randomness is rho_rnd (stage 3). Decomposing rlwe_sign_op this way
|
|
rules out adversarial realisations that bypass mu/transcript_hash
|
|
(e.g., computing the signature directly from ctx instead of folding
|
|
it into mu first). *)
|
|
|
|
type unpacked_sk_t.
|
|
type mu_t.
|
|
|
|
op unpack_sk : share_t -> unpacked_sk_t.
|
|
|
|
(* Corona's transcript_hash binder: bytes layout per
|
|
luxfi/corona/primitives/hash.go's Hash(suite, A, b, D, sid, T). *)
|
|
type mu_input_t = int list.
|
|
|
|
op message_bytes : message_t -> int list.
|
|
op context_bytes : ctx_t -> int list.
|
|
|
|
(* Context bytes have a Corona-bounded length. *)
|
|
axiom context_bytes_len_bound :
|
|
forall (ctx : ctx_t),
|
|
0 <= size (context_bytes ctx) <= 65535.
|
|
|
|
(* Corona transcript_hash byte layout (constructive). *)
|
|
op transcript_layout (m : message_t) (ctx : ctx_t) : mu_input_t =
|
|
[0; size (context_bytes ctx)] ++ context_bytes ctx ++ message_bytes m.
|
|
|
|
op kmac256_to_mu : mu_input_t -> mu_t.
|
|
|
|
op compute_mu (m : message_t) (ctx : ctx_t) : mu_t =
|
|
kmac256_to_mu (transcript_layout m ctx).
|
|
|
|
(* Corona signature components (c, z, Delta) surfaced as abstract
|
|
types so the byte-walk obligations split along the component
|
|
boundary. *)
|
|
type c_n1_t. (* R_q challenge from LowNormHash *)
|
|
type z_n1_t. (* R_q^N response vector *)
|
|
type delta_n1_t. (* R_q_nu^M rounded difference vector *)
|
|
|
|
(* R-LWE inner signing components, decomposed per Boschini Sign
|
|
step. Each op captures the centralized output of one inner-loop
|
|
stage on accept. *)
|
|
type R_value_t. (* R_i polynomial matrix at Round-1 *)
|
|
type w_value_t. (* w = A*R intermediate before HighBits *)
|
|
|
|
op central_matrix_a : unpacked_sk_t -> R_value_t.
|
|
|
|
(* The mask y at the accepting kappa. *)
|
|
op central_y_at_accepted_kappa :
|
|
unpacked_sk_t -> mu_t -> randomness_t -> z_n1_t.
|
|
|
|
(* The R-matrix product A*R giving the w intermediate. *)
|
|
op apply_mat_vec_mul : R_value_t -> z_n1_t -> w_value_t.
|
|
|
|
(* HighBits as a structural function over w polynomial vectors. *)
|
|
op high_bits_of_w : w_value_t -> delta_n1_t.
|
|
|
|
op central_w
|
|
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
|
: w_value_t =
|
|
apply_mat_vec_mul
|
|
(central_matrix_a usk)
|
|
(central_y_at_accepted_kappa usk mu_val rho_rnd).
|
|
|
|
(* LowNormHash from the transcript binder + w + group_pk. *)
|
|
op kmac_mu_w : mu_t -> w_value_t -> c_n1_t.
|
|
|
|
op rlwe_compute_c
|
|
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
|
: c_n1_t =
|
|
kmac_mu_w mu_val (central_w usk mu_val rho_rnd).
|
|
|
|
type R_q_xi. (* the c_xi field element used for c-scaling *)
|
|
|
|
(* The z response: z = y + c * s_1 + mask_prime - mask. *)
|
|
op central_c_from_c_tilde : c_n1_t -> R_q_xi.
|
|
op apply_c_to_s1 : R_q_xi -> unpacked_sk_t -> z_n1_t.
|
|
op add_response_vec : z_n1_t -> z_n1_t -> z_n1_t.
|
|
|
|
(* The z computation -- pure-functional composition. *)
|
|
op rlwe_compute_z
|
|
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
|
: z_n1_t =
|
|
add_response_vec
|
|
(central_y_at_accepted_kappa usk mu_val rho_rnd)
|
|
(apply_c_to_s1
|
|
(central_c_from_c_tilde
|
|
(rlwe_compute_c usk mu_val rho_rnd))
|
|
usk).
|
|
|
|
(* The Delta vector: Delta = h - round_nu(A*z - b*c). *)
|
|
op make_delta_of_w : w_value_t -> z_n1_t -> delta_n1_t.
|
|
|
|
op rlwe_compute_delta
|
|
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
|
: delta_n1_t =
|
|
make_delta_of_w
|
|
(central_w usk mu_val rho_rnd)
|
|
(rlwe_compute_z usk mu_val rho_rnd).
|
|
|
|
(* The threshold response identity -- Lean-bridged.
|
|
|
|
`partial_response_t` is the per-party response value
|
|
z_i = R_i * u + mask_prime_i + s_i * c * lambda_i - mask_i
|
|
computed by party i given:
|
|
- the common c challenge (broadcast at Round 2),
|
|
- the per-call randomness (rho_rnd),
|
|
- the message binder mu,
|
|
- the party's secret share s_i.
|
|
|
|
`lagrange_aggregate_responses Q [z_i ...]` combines per-party
|
|
responses over a quorum Q via the Lagrange-at-zero interpolation
|
|
(lambda_i coefficients are baked into z_i at sign time per the
|
|
Corona construction). *)
|
|
|
|
type partial_response_t.
|
|
|
|
op per_party_partial_response :
|
|
c_n1_t -> randomness_t -> mu_t -> share_t -> partial_response_t.
|
|
|
|
op lagrange_aggregate_responses :
|
|
int list -> partial_response_t list -> z_n1_t.
|
|
|
|
(* Lean-bridged: threshold_partial_response_identity for Corona.
|
|
|
|
Lean side (`Crypto.Threshold.Lagrange.threshold_partial_response_identity`,
|
|
lean/Crypto/Threshold_Lagrange.lean:121) proves:
|
|
given a polynomial f, quorum s, points v with `Set.InjOn v s`,
|
|
`f.degree < s.card`, masks y, challenge c, and
|
|
`z = y + c * fun i => f.eval (v i)`:
|
|
(Lagrange.interpolate s v z).eval 0
|
|
= (Lagrange.interpolate s v y).eval 0 + c * f.eval 0
|
|
|
|
The Corona instance: at the share_t level, the polynomial f is the
|
|
secret share `reconstruct Q shares`; per-party shares are
|
|
`poly_eval (reconstruct Q shares) i` for i in Q; per-party
|
|
partial responses are `per_party_partial_response c rho_rnd
|
|
mu_val share_i`. Aggregating those equals `rlwe_compute_z` on
|
|
the reconstructed share's unpacked form. *)
|
|
axiom threshold_partial_response_identity :
|
|
forall (Q : int list) (shares : share_t list)
|
|
(c : c_n1_t) (rho_rnd : randomness_t) (mu_val : mu_t),
|
|
uniq Q =>
|
|
size shares = size Q =>
|
|
poly_degree (reconstruct Q shares) < size Q =>
|
|
shares = List.map (poly_eval (reconstruct Q shares)) Q =>
|
|
lagrange_aggregate_responses Q
|
|
(List.map (per_party_partial_response c rho_rnd mu_val) shares)
|
|
= rlwe_compute_z
|
|
(unpack_sk (reconstruct Q shares))
|
|
mu_val rho_rnd.
|
|
|
|
op run_signing_components
|
|
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
|
: c_n1_t * z_n1_t * delta_n1_t =
|
|
(rlwe_compute_c usk mu_val rho_rnd,
|
|
rlwe_compute_z usk mu_val rho_rnd,
|
|
rlwe_compute_delta usk mu_val rho_rnd).
|
|
|
|
(* Corona signature codec: layout the (c, z, Delta) triple into the
|
|
byte-level signature_t and back. *)
|
|
op pack_n1_signature : c_n1_t -> z_n1_t -> delta_n1_t -> signature_t.
|
|
op unpack_n1_signature : signature_t -> c_n1_t * z_n1_t * delta_n1_t.
|
|
|
|
axiom pack_unpack_n1_signature_roundtrip :
|
|
forall (c : c_n1_t) (z : z_n1_t) (d : delta_n1_t),
|
|
unpack_n1_signature (pack_n1_signature c z d) = (c, z, d).
|
|
|
|
(* Derived injectivity. *)
|
|
lemma pack_n1_signature_injective :
|
|
forall (c1 c2 : c_n1_t) (z1 z2 : z_n1_t) (d1 d2 : delta_n1_t),
|
|
pack_n1_signature c1 z1 d1 = pack_n1_signature c2 z2 d2 =>
|
|
c1 = c2 /\ z1 = z2 /\ d1 = d2.
|
|
proof.
|
|
move=> c1 c2 z1 z2 d1 d2 Heq.
|
|
have H1 := pack_unpack_n1_signature_roundtrip c1 z1 d1.
|
|
have H2 := pack_unpack_n1_signature_roundtrip c2 z2 d2.
|
|
rewrite Heq in H1.
|
|
rewrite H1 in H2.
|
|
by case: H2 => -> -> ->.
|
|
qed.
|
|
|
|
(* sign_internal_loop factors structurally through the component-level
|
|
inner loop and the Corona signature packing step.
|
|
|
|
This DEFINITION (rather than abstract op declaration) is the
|
|
structural refinement that lets the combine and sign byte-walk
|
|
axioms split along the pack boundary. *)
|
|
op sign_internal_loop
|
|
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
|
: signature_t =
|
|
let cz_d = run_signing_components usk mu_val rho_rnd in
|
|
pack_n1_signature cz_d.`1 cz_d.`2 cz_d.`3.
|
|
|
|
op rlwe_sign_op (sk : share_t) (m : message_t)
|
|
(ctx : ctx_t) (rho_rnd : randomness_t)
|
|
: signature_t =
|
|
sign_internal_loop (unpack_sk sk) (compute_mu m ctx) rho_rnd.
|
|
|
|
(* R-LWE rejection-sampling accept event. *)
|
|
op accept_signing_attempt :
|
|
share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
|
|
|
(* Per-component accept events as abstract companions. *)
|
|
op accept_l2_z_norm : share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
|
op accept_l2_delta_norm: share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
|
op accept_full_rank : share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
|
|
|
axiom accept_signing_attempt_iff_components :
|
|
forall sk m ctx rho_rnd,
|
|
accept_signing_attempt sk m ctx rho_rnd
|
|
<=> (accept_l2_z_norm sk m ctx rho_rnd
|
|
/\ accept_l2_delta_norm sk m ctx rho_rnd
|
|
/\ accept_full_rank sk m ctx rho_rnd).
|
|
|
|
op rlwe_accept_lower_bound : real.
|
|
|
|
(* Pipeline-pinning reinforcement: compute_mu is a two-variable
|
|
injection; unpack_sk has a left inverse pack_sk. *)
|
|
op pack_sk : unpacked_sk_t -> share_t.
|
|
|
|
axiom pack_unpack_sk_roundtrip :
|
|
forall (sk : share_t), pack_sk (unpack_sk sk) = sk.
|
|
|
|
axiom compute_mu_injective :
|
|
forall (m1 m2 : message_t) (ctx1 ctx2 : ctx_t),
|
|
compute_mu m1 ctx1 = compute_mu m2 ctx2 =>
|
|
m1 = m2 /\ ctx1 = ctx2.
|
|
|
|
module type RLWESign = {
|
|
proc sign(sk : share_t, m : message_t, ctx : ctx_t,
|
|
rho_rnd : randomness_t) : signature_t
|
|
}.
|
|
|
|
(* The centralized Boschini Sign module -- returns the pure operator
|
|
`rlwe_sign_op`. *)
|
|
module CentralRLWESign : RLWESign = {
|
|
proc sign(sk : share_t, m : message_t, ctx : ctx_t,
|
|
rho_rnd : randomness_t) : signature_t = {
|
|
return rlwe_sign_op sk m ctx rho_rnd;
|
|
}
|
|
}.
|
|
|
|
(* Functional spec correspondence -- DISCHARGED as a lemma.
|
|
|
|
The original axiom was the Boschini hand-off point. With the
|
|
in-house RLWE_Functional mechanization, the role of
|
|
`CentralRLWESign.sign` collapses to a pure-functional wrapper
|
|
around `rlwe_sign_op`: the body literally returns
|
|
`rlwe_sign_op sk m ctx rho_rnd`. The Pr-equality is a deterministic
|
|
Hoare assertion closed by `byphoare` + skip. *)
|
|
lemma rlwe_sign_axiom :
|
|
forall (sk0 : share_t) (m0 : message_t) (c0 : ctx_t)
|
|
(r0 : randomness_t) &mm,
|
|
Pr[CentralRLWESign.sign(sk0, m0, c0, r0) @ &mm :
|
|
res = rlwe_sign_op sk0 m0 c0 r0] = 1%r.
|
|
proof.
|
|
move=> sk0 m0 c0 r0 &mm.
|
|
byphoare (_: sk = sk0 /\ m = m0 /\ ctx = c0 /\ rho_rnd = r0
|
|
==> res = rlwe_sign_op sk0 m0 c0 r0) => //.
|
|
proc; wp; skip => />.
|
|
qed.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Public-key derivation from secret share. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
(* `derive_pk : share_t -> group_pk_t` is the Corona key-derivation op:
|
|
for a freshly-sampled secret seed, derive_pk returns the matching
|
|
public verification key (A, bTilde = round_xi(A*s + e)). *)
|
|
op derive_pk : group_pk_t. (* placeholder shape; concrete arity below *)
|
|
op derive_pk_op : share_t -> group_pk_t.
|
|
|
|
(* Verifier. *)
|
|
op corona_verify : group_pk_t -> message_t -> ctx_t
|
|
-> signature_t -> bool.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Corona threshold oracle interface *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
module type Corona_Threshold = {
|
|
proc round1(sess : session_t, share : share_t,
|
|
rho_rnd : randomness_t) : round1_t
|
|
proc round2(sess : session_t, share : share_t,
|
|
round1_aggregate : round1_t list,
|
|
c_challenge : message_t) : round2_t
|
|
proc combine(group_pk : group_pk_t, m : message_t, ctx : ctx_t,
|
|
quorum : int list,
|
|
shares : share_t list,
|
|
rho_rnd : randomness_t,
|
|
r1s : round1_t list, r2s : round2_t list) : signature_t
|
|
}.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Combine refines the Boschini dispatch on the reconstructed secret. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* The cryptographic content of the proof of Boschini correctness (paper *)
|
|
(* §3 Theorem 1): the Corona Combine procedure assembles (c, z, Delta) *)
|
|
(* using Lagrange-aggregated values that coincide ON-THE-NOSE with the *)
|
|
(* centralized (c, z, Delta) under the reconstructed secret. We name *)
|
|
(* this dispatch step as a single axiom over the abstract Combine *)
|
|
(* semantics; the concrete refinement proof is the Jasmin-side *)
|
|
(* obligation (jasmin/threshold/combine.jazz refines `CombineAbs`). *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
module CombineAbs = {
|
|
proc combine(group_pk : group_pk_t, m : message_t, ctx : ctx_t,
|
|
quorum : int list,
|
|
shares : share_t list,
|
|
rho_rnd : randomness_t,
|
|
r1s : round1_t list, r2s : round2_t list) : signature_t = {
|
|
var sk_group : share_t;
|
|
var sig : signature_t;
|
|
sk_group <- reconstruct quorum shares;
|
|
sig <@ CentralRLWESign.sign(sk_group, m, ctx, rho_rnd);
|
|
return sig;
|
|
}
|
|
}.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Discharged step: Combine = rlwe_sign_op o reconstruct *)
|
|
(* -------------------------------------------------------------------- *)
|
|
lemma combine_dispatches_to_rlwe
|
|
(gpk0 : group_pk_t)
|
|
(m0 : message_t) (ctx0 : ctx_t)
|
|
(Q0 : int list) (shs0 : share_t list)
|
|
(rr0 : randomness_t)
|
|
(r1s0 : round1_t list) (r2s0 : round2_t list) &m :
|
|
Pr[CombineAbs.combine(gpk0, m0, ctx0, Q0, shs0, rr0, r1s0, r2s0) @ &m :
|
|
res = rlwe_sign_op (reconstruct Q0 shs0) m0 ctx0 rr0] = 1%r.
|
|
proof.
|
|
byphoare (_:
|
|
group_pk = gpk0 /\ m = m0 /\ ctx = ctx0 /\ quorum = Q0
|
|
/\ shares = shs0 /\ rho_rnd = rr0 /\ r1s = r1s0 /\ r2s = r2s0
|
|
==> _) => //.
|
|
proc; inline CentralRLWESign.sign; wp; skip => /#.
|
|
qed.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Class N1 -- byte-equality theorem *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
section ClassN1.
|
|
|
|
declare module S <: RLWESign.
|
|
declare module T <: Corona_Threshold.
|
|
|
|
(* Section-local refinement axiom: the Jasmin-extracted Combine is
|
|
equivalent to `CombineAbs.combine` under the honest-quorum
|
|
precondition.
|
|
|
|
The precondition `group_pk{1} = derive_pk_op (reconstruct quorum{1}
|
|
shares{1})` is the protocol-consistency obligation: the byte-walk
|
|
refinement file's atomic axiom requires the ghost full_gpk field to
|
|
be the derived pubkey of the reconstructed share. The honest
|
|
threshold caller always satisfies this (the DKG-committed group
|
|
pubkey IS the derived pubkey of the secret). *)
|
|
declare axiom combine_body_axiom :
|
|
equiv [ T.combine ~ CombineAbs.combine :
|
|
={arg}
|
|
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
|
/\ accept_signing_attempt
|
|
(reconstruct quorum{1} shares{1})
|
|
m{1} ctx{1} rho_rnd{1}
|
|
/\ uniq quorum{1}
|
|
/\ size shares{1} = size quorum{1}
|
|
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
|
/\ shares{1} = List.map
|
|
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
|
==> ={res} ].
|
|
|
|
(* Functional-spec hypothesis on the single-party module `S`. *)
|
|
declare axiom S_functional_spec :
|
|
equiv [ S.sign ~ CentralRLWESign.sign :
|
|
={arg}
|
|
/\ accept_signing_attempt sk{1} m{1} ctx{1} rho_rnd{1}
|
|
==> ={res} ].
|
|
|
|
(* The honest-quorum Corona execution, as a single procedure. *)
|
|
module ThresholdRun (T : Corona_Threshold) = {
|
|
proc run(group_pk : group_pk_t, shares : share_t list,
|
|
quorum : int list, m : message_t, ctx : ctx_t,
|
|
rho_rnd : randomness_t) : signature_t = {
|
|
var r1s : round1_t list;
|
|
var c_challenge : message_t;
|
|
var r2s : round2_t list;
|
|
var sig : signature_t;
|
|
var sess : session_t;
|
|
sess <- witness;
|
|
r1s <- [];
|
|
r2s <- [];
|
|
c_challenge <- witness;
|
|
sig <@ T.combine(group_pk, m, ctx, quorum, shares, rho_rnd, r1s, r2s);
|
|
return sig;
|
|
}
|
|
}.
|
|
|
|
(* The single-party central-RLWE execution. *)
|
|
module SinglePartyRun (S : RLWESign) = {
|
|
proc run(group_pk : group_pk_t, shares : share_t list,
|
|
quorum : int list, m : message_t, ctx : ctx_t,
|
|
rho_rnd : randomness_t) : signature_t = {
|
|
var sk_group : share_t;
|
|
var sig : signature_t;
|
|
sk_group <- reconstruct quorum shares;
|
|
sig <@ S.sign(sk_group, m, ctx, rho_rnd);
|
|
return sig;
|
|
}
|
|
}.
|
|
|
|
(* Step 1 -- single-party run is equivalent to central RLWE
|
|
instantiation via the section-local `S_functional_spec` axiom. *)
|
|
lemma single_party_run_refines_central :
|
|
equiv [ SinglePartyRun(S).run ~ SinglePartyRun(CentralRLWESign).run :
|
|
={group_pk, shares, quorum, m, ctx, rho_rnd}
|
|
/\ accept_signing_attempt
|
|
(reconstruct quorum{1} shares{1})
|
|
m{1} ctx{1} rho_rnd{1}
|
|
==> ={res} ].
|
|
proof.
|
|
proc.
|
|
call S_functional_spec.
|
|
auto.
|
|
qed.
|
|
|
|
(* Step 2 -- single-party central run produces `rlwe_sign_op` on the
|
|
reconstructed secret, with probability 1. *)
|
|
lemma single_party_central_eq_op
|
|
(gpk : group_pk_t) (mm : message_t) (cctx : ctx_t)
|
|
(Q : int list) (shs : share_t list) (rr : randomness_t) &m :
|
|
Pr[SinglePartyRun(CentralRLWESign).run(gpk, shs, Q, mm, cctx, rr) @ &m :
|
|
res = rlwe_sign_op (reconstruct Q shs) mm cctx rr] = 1%r.
|
|
proof.
|
|
byphoare (_:
|
|
group_pk = gpk /\ m = mm /\ ctx = cctx /\ quorum = Q
|
|
/\ shares = shs /\ rho_rnd = rr ==> _) => //.
|
|
proc; inline CentralRLWESign.sign; wp; skip => /#.
|
|
qed.
|
|
|
|
(* Step 4 -- threshold run via CombineAbs produces `rlwe_sign_op`
|
|
on the reconstructed secret, with probability 1. *)
|
|
lemma threshold_combine_abs_eq_op
|
|
(gpk : group_pk_t) (mm : message_t) (cctx : ctx_t)
|
|
(Q : int list) (shs : share_t list) (rr : randomness_t) &m :
|
|
Pr[CombineAbs.combine(gpk, mm, cctx, Q, shs, rr, [], []) @ &m :
|
|
res = rlwe_sign_op (reconstruct Q shs) mm cctx rr] = 1%r.
|
|
proof.
|
|
apply (combine_dispatches_to_rlwe gpk mm cctx Q shs rr [] [] &m).
|
|
qed.
|
|
|
|
(* Step 6 -- chain Steps 1-5 to derive the byte-equality theorem.
|
|
|
|
GENERIC theorem: parametric over abstract `T : Corona_Threshold`
|
|
and `S : RLWESign` with the two module-contract axioms
|
|
(`combine_body_axiom`, `S_functional_spec`) as section-local
|
|
hypotheses. After section closure, this lemma is universally-
|
|
quantified over (S, T, combine-equiv-on-T, sign-equiv-on-S). *)
|
|
lemma corona_n1_byte_equality :
|
|
equiv [ ThresholdRun(T).run ~ SinglePartyRun(S).run :
|
|
={group_pk, shares, quorum, m, ctx, rho_rnd}
|
|
/\ uniq quorum{1}
|
|
/\ size shares{1} = size quorum{1}
|
|
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
|
/\ accept_signing_attempt
|
|
(reconstruct quorum{1} shares{1})
|
|
m{1} ctx{1} rho_rnd{1}
|
|
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
|
/\ shares{1} = List.map
|
|
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
|
==> ={res} ].
|
|
proof.
|
|
transitivity SinglePartyRun(CentralRLWESign).run
|
|
(={group_pk, shares, quorum, m, ctx, rho_rnd}
|
|
/\ uniq quorum{1}
|
|
/\ size shares{1} = size quorum{1}
|
|
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
|
/\ accept_signing_attempt
|
|
(reconstruct quorum{1} shares{1})
|
|
m{1} ctx{1} rho_rnd{1}
|
|
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
|
/\ shares{1} = List.map
|
|
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
|
==> ={res})
|
|
(={group_pk, shares, quorum, m, ctx, rho_rnd}
|
|
/\ accept_signing_attempt
|
|
(reconstruct quorum{1} shares{1})
|
|
m{1} ctx{1} rho_rnd{1}
|
|
==> ={res}).
|
|
+ move=> &1 &2 [#] 6-> uQ szq Hgpk Haccept Hdeg Hhonest.
|
|
by exists (group_pk{2}, shares{2}, quorum{2}, m{2}, ctx{2}, rho_rnd{2}).
|
|
+ done.
|
|
+ (* Step A: ThresholdRun(T).run ~ SinglePartyRun(CentralRLWESign).run *)
|
|
proc.
|
|
transitivity{1}
|
|
{ sess <- witness;
|
|
r1s <- [];
|
|
r2s <- [];
|
|
c_challenge <- witness;
|
|
sig <@ CombineAbs.combine(group_pk, m, ctx, quorum, shares,
|
|
rho_rnd, r1s, r2s); }
|
|
(={group_pk, shares, quorum, m, ctx, rho_rnd}
|
|
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
|
/\ accept_signing_attempt
|
|
(reconstruct quorum{1} shares{1})
|
|
m{1} ctx{1} rho_rnd{1}
|
|
/\ uniq quorum{1}
|
|
/\ size shares{1} = size quorum{1}
|
|
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
|
/\ shares{1} = List.map
|
|
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
|
==> ={sig})
|
|
(={group_pk, shares, quorum, m, ctx, rho_rnd} ==> ={sig}).
|
|
+ smt().
|
|
+ done.
|
|
+ wp.
|
|
call combine_body_axiom.
|
|
by auto.
|
|
inline CombineAbs.combine.
|
|
wp.
|
|
call (_: ={arg} ==> ={res}).
|
|
+ by sim.
|
|
auto.
|
|
+ (* Step B: SinglePartyRun(CentralRLWESign).run ~ SinglePartyRun(S).run *)
|
|
symmetry.
|
|
conseq single_party_run_refines_central.
|
|
+ move=> &1 &2 [#] 6-> Haccept.
|
|
do! split=> //.
|
|
+ done.
|
|
qed.
|
|
|
|
end section ClassN1.
|
|
|
|
(* -------------------------------------------------------------------- *)
|
|
(* Corollary: a Corona verifier accepts every Corona signature *)
|
|
(* produced by an honest quorum. *)
|
|
(* -------------------------------------------------------------------- *)
|
|
(* This is exactly the Lean axiom *)
|
|
(* Crypto.Corona.Unforgeability.corona_output_interchangeable *)
|
|
(* lifted to EasyCrypt's probabilistic Hoare setting. Stated as a *)
|
|
(* commented future obligation -- the body is a direct corollary of *)
|
|
(* `corona_n1_byte_equality` plus Boschini verifier correctness on *)
|
|
(* outputs produced by Boschini Sign (the cited paper's correctness *)
|
|
(* theorem). *)
|
|
(* -------------------------------------------------------------------- *)
|
|
|
|
(* The verifier-compatibility corollary (Pr[verify o ThresholdRun] = 1)
|
|
is a direct consequence of `corona_n1_byte_equality` plus the
|
|
Boschini correctness theorem. We do not restate it here because the
|
|
byte-equality already implies it; restating it would add a second
|
|
admit on the same content. The corollary is left for the consumer
|
|
who wants the probabilistic phrasing. *)
|