From cb00c2db833af79b6c7f3fa9c0b7923e1a99707b Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Tue, 27 Oct 2026 12:38:29 +0000 Subject: [PATCH 1/3] spec(p384): point, scalar and verify contracts The statements of the executable group law, scalar product, key decoding, digest reduction and verify, over the vocabulary of spec.rs. No code yet. Co-Authored-By: Claude Sonnet 5.5 --- crates/clazel-p384/src/lib.rs | 1 + crates/clazel-p384/src/point_contract.rs | 71 ++++++++++++++++++++++++ 2 files changed, 72 insertions(+) create mode 100644 crates/clazel-p384/src/point_contract.rs diff --git a/crates/clazel-p384/src/lib.rs b/crates/clazel-p384/src/lib.rs index e64f716..94322e8 100644 --- a/crates/clazel-p384/src/lib.rs +++ b/crates/clazel-p384/src/lib.rs @@ -28,4 +28,5 @@ pub mod certificates; pub mod contract; pub mod examples; pub mod field; +pub mod point_contract; pub mod spec; diff --git a/crates/clazel-p384/src/point_contract.rs b/crates/clazel-p384/src/point_contract.rs new file mode 100644 index 0000000..1813e2b --- /dev/null +++ b/crates/clazel-p384/src/point_contract.rs @@ -0,0 +1,71 @@ +//! What each executable function above the field is proven to satisfy: the +//! group law, the scalar product, the key decoding and the digest's +//! reduction. As in [`crate::field::contract`], the arguments are the +//! mathematical values the executable objects stand for, so reviewing these +//! predicates and [`crate::spec`] is enough to know what the code +//! guarantees. The statement for `verify` itself is +//! [`crate::contract::verify_ensures`]. +//! +//! The executable point [`Point`](crate::point::Point) is either the point at +//! infinity or an affine pair of [`Fe`](crate::field::Fe)s modulo p; its +//! view `a@` is the spec's [`Point`](crate::spec::Point) with those +//! residues as coordinates. `r@` for an `Option` is the option of the +//! views. A point is *well formed* (`wf`) when its coordinates are residues +//! modulo p (not modulo n); every function below that takes a point requires +//! this and every point it returns is well formed. +//! +//! ```text +//! point::ec_add(&Point, &Point) -> Option +//! requires a.wf(), b.wf() +//! ensures r.wf(), ec_add_ensures(a@, b@, r@) +//! scalar::scalar_mul(&[u8; 48], &Point) -> Option +//! requires pt.wf() +//! ensures r.wf(), scalar_mul_ensures(k@, pt@, r@) +//! point::decode_public_key(&[u8]) -> Option +//! ensures r.wf(), decode_public_key_ensures(q@, r@) +//! scalar::derive_e(&[u8]) -> Fe // e mod n, as a residue mod n +//! requires digest.len() <= 64 +//! ensures r.which() == Which::N, derive_e_ensures(digest@, r.val()) +//! verify::verify(&[u8], &[u8; 48], &[u8; 48], &[u8]) -> bool +//! requires verify_requires(digest@) +//! ensures verify_ensures(digest@, r@, s@, point@, ok) +//! ``` + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// `a + b` on P-384: [`crate::spec::ec_add`], SEC 1 §2.2.1, with `None` +/// exactly when the spec's is `None` (an inversion failed). +pub open spec fn ec_add_ensures(a: Point, b: Point, r: Option) -> bool { + r == ec_add(p384(), a, b) +} + +/// `[k] pt` where `k` is the big-endian octets of the scalar: +/// [`crate::spec::scalar_mul`] of its integer (`os2ip`), MSB-first +/// double-and-add, with `None` exactly when the spec's is `None`. +pub open spec fn scalar_mul_ensures(k: Seq, pt: Point, r: Option) -> bool { + r == scalar_mul(p384(), os2ip(k), pt) +} + +/// The key `q` (an ECPoint, SEC 1 §2.3.4) decoded and validated: +/// [`crate::spec::decode_public_key`]. `None` for anything that function +/// refuses (compressed, hybrid, infinity, wrong length, a coordinate at +/// least p, a point off the curve). +pub open spec fn decode_public_key_ensures(q: Seq, r: Option) -> bool { + r == decode_public_key(p384(), q) +} + +/// FIPS 186-5 §6.4.2 step 3 followed by the reduction of step 5: the +/// residue modulo n of [`crate::spec::derive_e`]. (`derive_e` itself may be +/// at least n, up to 2^384 - 1, which is more than one residue modulo n; step +/// 5 reduces it, and the code returns the reduced value, which is all step 5 +/// uses.) +pub open spec fn derive_e_ensures(h: Seq, r: nat) -> bool { + r == derive_e(p384(), h) % p384().n +} + +} // verus! From f2b440162a8a3c9f71bacaf1375fbb4778825cdc Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Tue, 27 Oct 2026 12:52:35 +0000 Subject: [PATCH 2/3] feat(p384): group law, scalar product and verify, proven against the spec Affine SEC 1 2.2.1 ec_add in the spec's case order, uncompressed key decoding, MSB-first double-and-add against spec::scalar_mul, derive_e with the reduction mod n, and verify meeting verify_ensures, all over the six fiat axioms and no new one. Adds Fe::dup (a copy with the same which/val). Tier stays 0. Co-Authored-By: Claude Sonnet 5.5 --- crates/clazel-p384/Cargo.toml | 7 +- crates/clazel-p384/README.md | 88 ++++-- crates/clazel-p384/src/contract.rs | 11 +- crates/clazel-p384/src/convert.rs | 103 +++++++ crates/clazel-p384/src/field/fe.rs | 13 + crates/clazel-p384/src/lemmas.rs | 387 ++++++++++++++++++++++++ crates/clazel-p384/src/lib.rs | 33 ++- crates/clazel-p384/src/point.rs | 454 +++++++++++++++++++++++++++++ crates/clazel-p384/src/scalar.rs | 218 ++++++++++++++ crates/clazel-p384/src/verify.rs | 88 ++++++ 10 files changed, 1370 insertions(+), 32 deletions(-) create mode 100644 crates/clazel-p384/src/convert.rs create mode 100644 crates/clazel-p384/src/lemmas.rs create mode 100644 crates/clazel-p384/src/point.rs create mode 100644 crates/clazel-p384/src/scalar.rs create mode 100644 crates/clazel-p384/src/verify.rs diff --git a/crates/clazel-p384/Cargo.toml b/crates/clazel-p384/Cargo.toml index 740eaa3..c5ff989 100644 --- a/crates/clazel-p384/Cargo.toml +++ b/crates/clazel-p384/Cargo.toml @@ -11,9 +11,10 @@ vstd = "=0.0.0-2026-10-04-0306" fiat-crypto = { version = "=0.3.0", default-features = false } # Verification tier (docs/VERIFICATION.md). `tier` is what is proven about -# the shipped code today; `target-tier` is what the policy requires. The spec -# and the field arithmetic exist, but there is no `verify` and none of the -# tier 1 or tier 2 evidence yet, so tier 0. +# the shipped code today; `target-tier` is what the policy requires. The spec, +# the field, the group law and `verify` exist and are proven, but none of the +# tier 1 or tier 2 evidence (Kani harnesses, mutations of the code, an +# independent transcription, conformance suites) does yet, so tier 0. [package.metadata.clazel] tier = 0 target-tier = 2 diff --git a/crates/clazel-p384/README.md b/crates/clazel-p384/README.md index 1a15f6b..24694ea 100644 --- a/crates/clazel-p384/README.md +++ b/crates/clazel-p384/README.md @@ -4,10 +4,12 @@ ECDSA signature verification over NIST P-384 (FIPS 186-5 §6.4.2), specified in Verus. Part of [Clazel](../../README.md), a web browser whose parsers of untrusted input carry machine-checked proofs. -## Status: specification and field arithmetic +## Status: specification, field, point arithmetic and `verify` -**Tier 0, target tier 2.** The specification and the field arithmetic are -written; the point arithmetic and `verify` are not. What exists: +**Tier 0, target tier 2.** The specification, the field arithmetic, the +point arithmetic and `verify` are written, and `verify` is proven against +the contract below the six axioms. The tier 1 and tier 2 evidence is not +(see Verification). What exists: - `src/spec.rs`: what "a valid ECDSA P-384 signature" means, transcribed step by step from FIPS 186-5 §6.4.2, with the routines it defers to taken @@ -16,17 +18,24 @@ written; the point arithmetic and `verify` are not. What exists: sources are pinned by SHA-256 in the file's header, which also lists every modelling choice (13 of them) and how the lossy text extraction of the PDFs was read. -- `src/contract.rs`: what the executable `verify(digest, r, s, point)` will - be proven to satisfy, as predicates over the spec. +- `src/contract.rs`: what the executable `verify(digest, r, s, point)` is + proven to satisfy, as predicates over the spec. `src/point_contract.rs`: + the same for the group law, the scalar product, the key decoding and the + digest's reduction. - `src/examples.rs`: known answers, proven by evaluating the spec (`by (compute_only)`), on a toy curve and on P-384. - `src/axioms.rs`, `src/field/`: the field arithmetic, described below. +- `src/point.rs`, `src/scalar.rs`, `src/verify.rs`, `src/convert.rs`, + `src/lemmas.rs`: the executable group law, key decoding, scalar product, + `verify`, and their lemmas, described below. - `tests/field.rs`: known answers for the field, computed with Python. +- `tests/verify.rs`: smoke tests of `verify` (Wycheproof vectors and + hand-damaged inputs), described below. -Nothing here claims verification of `verify`, which does not exist yet. What -is evaluated is the spec itself, which shows the transcription computes what -was worked out independently, not that it matches the standards (a person -reads it against them; [docs/SPEC-STYLE.md](../../docs/SPEC-STYLE.md)). +What is evaluated in `examples.rs` is the spec itself, which shows the +transcription computes what was worked out independently, not that it matches +the standards (a person reads it against them; +[docs/SPEC-STYLE.md](../../docs/SPEC-STYLE.md)). ## The field (modulo p and modulo n) @@ -66,6 +75,48 @@ they stand for. That is the check on the axioms' fit to the real fiat, and on the constants of `field/spec.rs` and `fe.rs` (the moduli, `R^2 mod m`, the exponents). +## The group law, the scalar product and `verify` + +Proven in Verus against `spec.rs`, over the six axioms and nothing else (no +new axiom, no `assume`, no `external_body` outside `axioms.rs`). + +- **`point::Point`** is the point at infinity or an affine pair of `Fe`s + modulo p, with a view to `spec::Point`. `point::ec_add` runs SEC 1 §2.2.1's + rules in the spec's order (rules 1 and 2, then the negation test `x1 == x2 + && (y1 + y2) % p == 0`, then different x, then doubling), each field + operation an `Fe` operation, so its contract is `r == spec::ec_add(p384(), + a, b)`, `None` exactly when the spec's is (a failed `inv`). +- **`point::decode_public_key`** is `spec::decode_public_key`: length 97, first + octet `04`, each coordinate below p by `Fe::from_octets`, and the curve + equation. Compressed, hybrid and infinity encodings are refused. +- **`scalar::scalar_mul`** is MSB-first double-and-add over the 48 octets of + the scalar, one bit at a time; the loop invariant is that after the top `i` + bits the accumulator is `spec::scalar_mul` of the integer they make, from + the spec's own recursion. No associativity is used. +- **`scalar::derive_e`** reads the leftmost `min(|H|, 48)` octets of the digest + and reduces them modulo n by Horner's rule in the field, so `e >= n` is + handled; the proof relates the spec's bit-string `derive_e` to `os2ip`. +- **`verify::verify`** follows the spec's order: the key first, step 1 (`r` + and `s` in `[1, n - 1]` as integers, before any reduction), step 3, step 4 + (`Fe::inv` mod n), step 5, step 6 as the sum of two separately computed + products (infinity and any failed operation reject), and step 9 with + `x_R mod n` reduced properly (`x_R < p` can exceed n). Its contract is + `ok == ecdsa_verify(p384(), digest, os2ip(r), os2ip(s), point)` for a + digest of 0 to 64 octets. +- **Not constant time, by design**, and slow by design: this is the affine + stage, one field inversion (about 768 multiplications) per group + operation. Measured by `tests/verify.rs`'s `timing` test on the development + machine (Apple silicon): about 0.94 s per verification in a debug build and + about 45 ms in a release build. +- **Smoke tests, not conformance.** `tests/verify.rs` accepts eight valid + and rejects six invalid vectors of Wycheproof's + `ecdsa_secp384r1_sha384_test.json` (commit `d17cc89f`; tcIds in the file), + and rejects damaged `r`, `s`, digests and keys. Wycheproof in full, ACVP and + a differential against another engine are later work. +- **One addition to `field::Fe`:** `Fe::dup`, a copy with the same + `which` and `val`. `Fe` is not `Clone` and `Fe`'s contracts and the axioms + are unchanged. + ## What it is, and what it is not **Public-key verification only.** The key, the signature and the digest are @@ -114,16 +165,19 @@ times out on it. Run `cargo verus focus -- -A missing_docs` in this directory. What it proves today is that every spec function terminates (each recursive one has a -`decreases`), that the evaluated examples hold, and that each field function -meets its contract in `field/contract.rs` over the six axioms. +`decreases`), that the evaluated examples hold, that each field function +meets its contract in `field/contract.rs`, and that `ec_add`, +`scalar_mul`, `decode_public_key`, `derive_e` and `verify` meet theirs +(`point_contract.rs`, `contract.rs`), over the six axioms. `mutations.json` holds 26 mutations of `spec.rs`, each killed with a -certificate that contradicts one of those examples; the field code has no -mutations yet. There is no lemma about the spec of the signature itself, no -independent transcription, no conformance test against an official suite and -no Kani harness yet, so the crate stays at tier 0; see +certificate that contradicts one of those examples; the executable code has +no mutations yet. There is no lemma about the spec of the signature itself, +no independent transcription, no conformance test against an official suite +and no Kani harness yet, so the crate stays at tier 0; see [docs/VERIFICATION.md](../../docs/VERIFICATION.md) for what each tier -requires. `verify` is not written, so nothing here proves anything about -ECDSA verification yet. +requires. The proofs cover memory and arithmetic safety of the Verus-checked +code, but the claim is only as good as `spec.rs` (read against the standards +by a person) and the six axioms (fiat-crypto's printed postconditions). ## Licence diff --git a/crates/clazel-p384/src/contract.rs b/crates/clazel-p384/src/contract.rs index feebf56..f8e8fda 100644 --- a/crates/clazel-p384/src/contract.rs +++ b/crates/clazel-p384/src/contract.rs @@ -1,8 +1,9 @@ -//! The contract the executable `verify` must be proven to meet. There is no -//! executable code yet; these predicates are what its `requires` and -//! `ensures` clauses will be, so reviewing them and [`super::spec`] is -//! enough to know what the implementation will guarantee (the same shape as -//! `clazel-pkcs1`'s `contract.rs`). +//! The contract the executable `verify` is proven to meet. These predicates +//! are its `requires` and `ensures` clauses (`src/verify.rs`), so reviewing +//! them and [`super::spec`] is enough to know what the implementation +//! guarantees (the same shape as `clazel-pkcs1`'s `contract.rs`). The +//! contracts of the functions it is built from are in +//! [`super::point_contract`] and [`super::field::contract`]. //! //! ```text //! pub fn verify(digest: &[u8], r: &[u8; 48], s: &[u8; 48], point: &[u8]) -> (ok: bool) diff --git a/crates/clazel-p384/src/convert.rs b/crates/clazel-p384/src/convert.rs new file mode 100644 index 0000000..652aa49 --- /dev/null +++ b/crates/clazel-p384/src/convert.rs @@ -0,0 +1,103 @@ +//! Small conversions the point and scalar code needs: an octet as a +//! residue, and an octet string reduced modulo p or n (Horner's rule over +//! the field operations). Both are proven against [`crate::spec::os2ip`]. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +use crate::field::Fe; + +/// The residue `b`, for an octet `b` (both moduli exceed 255). +pub fn fe_of_byte(w: crate::field::spec::Which, b: u8) -> (r: Fe) + ensures + r.which() == w, + r.val() == b as nat, +{ + let mut o = [0u8;48]; + o[47] = b; + proof { + crate::lemmas::lemma_os2ip_last(o@); + crate::lemmas::lemma_modulus_gt_256(w); + } + match Fe::from_octets(w, &o) { + Some(f) => f, + // Unreachable: os2ip(o) = b < 256 < modulus. + None => { + proof { + assert(false); + } + Fe::one(w) + }, + } +} + +/// The residue 256. +fn fe_256(w: crate::field::spec::Which) -> (r: Fe) + ensures + r.which() == w, + r.val() == 256, +{ + let a = fe_of_byte(w, 255); + let one = Fe::one(w); + proof { + crate::lemmas::lemma_modulus_gt_256(w); + vstd::arithmetic::div_mod::lemma_small_mod(256nat, crate::field::spec::modulus(w)); + } + a.add(&one) +} + +/// The octets `o[0..k]`, big-endian, as an integer reduced modulo the +/// modulus of `w`: `os2ip(o[0..k]) mod m`. Horner's rule in the field, so +/// that no integer ever exceeds the modulus; this is how a value that may be +/// at least the modulus (the digest `e` against n, `x_R` against n) is +/// reduced. +pub fn reduce_prefix(w: crate::field::spec::Which, o: &[u8], k: usize) -> (r: Fe) + requires + k <= o.len(), + ensures + r.which() == w, + r.val() == os2ip(o@.subrange(0, k as int)) % crate::field::spec::modulus(w), +{ + let c256 = fe_256(w); + let mut acc = fe_of_byte(w, 0); + let mut i: usize = 0; + proof { + assert(o@.subrange(0, 0) =~= Seq::::empty()); + crate::lemmas::lemma_modulus_gt_256(w); + vstd::arithmetic::div_mod::lemma_small_mod(0nat, crate::field::spec::modulus(w)); + } + while i < k + invariant + i <= k, + k <= o.len(), + acc.which() == w, + c256.which() == w, + c256.val() == 256, + acc.val() == os2ip(o@.subrange(0, i as int)) % crate::field::spec::modulus(w), + decreases k - i, + { + let byte: u8 = match o.get(i) { + Some(b) => *b, + None => 0, + }; + let b = fe_of_byte(w, byte); + let shifted = acc.mul(&c256); + let next = shifted.add(&b); + proof { + let pre = o@.subrange(0, i as int); + crate::field::lemmas::lemma_os2ip_push(pre, byte); + assert(o@.subrange(0, i as int + 1) =~= pre.push(byte)); + crate::lemmas::lemma_modulus_gt_256(w); + crate::lemmas::lemma_horner_mod(os2ip(pre), byte as nat, crate::field::spec::modulus(w)); + } + acc = next; + i = i.saturating_add(1); + } + acc +} + +} // verus! diff --git a/crates/clazel-p384/src/field/fe.rs b/crates/clazel-p384/src/field/fe.rs index fe373d9..c54b1ab 100644 --- a/crates/clazel-p384/src/field/fe.rs +++ b/crates/clazel-p384/src/field/fe.rs @@ -50,6 +50,19 @@ impl Fe { from_montgomery(self.which, self.limbs@) } + /// A copy: the same limbs, so the same modulus and residue. (`Fe` is not + /// `Clone`: the derive would give no contract.) + pub fn dup(&self) -> (r: Fe) + ensures + r.which() == self.which(), + r.val() == self.val(), + { + proof { + use_type_invariant(self); + } + Fe { which: self.which, limbs: self.limbs } + } + /// The residue is below the modulus. A no-op at run time: it hands the /// type invariant to the caller's proof. pub fn val_lt_modulus(&self) diff --git a/crates/clazel-p384/src/lemmas.rs b/crates/clazel-p384/src/lemmas.rs new file mode 100644 index 0000000..8fa06bb --- /dev/null +++ b/crates/clazel-p384/src/lemmas.rs @@ -0,0 +1,387 @@ +//! Facts the point, scalar and verify code is proven from: about octet +//! strings, the curve constants and the modular arithmetic of the group law. +//! Everything here is proven, none is assumed. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + + +// --------------------------------------------------------------------- +// Octet strings. +// --------------------------------------------------------------------- + +/// An all-zero octet string is the integer 0. +pub proof fn lemma_os2ip_zeros(s: Seq) + requires + forall|i: int| 0 <= i < s.len() ==> s[i] == 0, + ensures + os2ip(s) == 0, + decreases s.len(), +{ + if s.len() > 0 { + let d = s.drop_last(); + assert forall|i: int| 0 <= i < d.len() implies d[i] == 0 by { + assert(d[i] == s[i]); + } + lemma_os2ip_zeros(d); + } +} + +/// An octet string whose last octet is `b` and the rest all zero is the +/// integer `b`. +pub proof fn lemma_os2ip_last(s: Seq) + requires + s.len() > 0, + forall|i: int| 0 <= i < s.len() - 1 ==> s[i] == 0, + ensures + os2ip(s) == s.last() as nat, +{ + let d = s.drop_last(); + assert forall|i: int| 0 <= i < d.len() implies d[i] == 0 by { + assert(d[i] == s[i]); + } + lemma_os2ip_zeros(d); +} + +/// Both moduli exceed 256, so a byte (and 256) is a residue. +pub proof fn lemma_modulus_gt_256(w: crate::field::spec::Which) + ensures + crate::field::spec::modulus(w) > 256, +{ + match w { + crate::field::spec::Which::P => { + assert(p384().p > 256) by (compute_only); + }, + crate::field::spec::Which::N => { + assert(p384().n > 256) by (compute_only); + }, + } +} + +/// Horner's step modulo `m`: reducing before multiplying by 256 and adding +/// the octet `b` gives the residue of the whole. +pub proof fn lemma_horner_mod(x: nat, b: nat, m: nat) + requires + m > 0, + b < m, + ensures + (((x % m) * 256) % m + b) % m == (x * 256 + b) % m, +{ + vstd::arithmetic::div_mod::lemma_mul_mod_noop_left(x as int, 256int, m as int); + vstd::arithmetic::div_mod::lemma_small_mod(b, m); + vstd::arithmetic::div_mod::lemma_add_mod_noop((x * 256) as int, b as int, m as int); +} + +/// A product with a residue reduced first is the residue of the product. +pub proof fn lemma_mul_reduced(x: nat, w: nat, m: nat) + requires + m > 0, + ensures + ((x % m) * w) % m == (x * w) % m, +{ + vstd::arithmetic::div_mod::lemma_mul_mod_noop_left(x as int, w as int, m as int); +} + +// --------------------------------------------------------------------- +// The curve constants. +// --------------------------------------------------------------------- + +/// The coefficient `a` is `p - 3` (SP 800-186 §3.2.1: a = -3). +pub proof fn lemma_curve_a() + ensures + p384().a == p384().p - 3, + p384().a < p384().p, + p384().b < p384().p, + p384().gx < p384().p, + p384().gy < p384().p, +{ + assert(p384().a == p384().p - 3 && p384().a < p384().p && p384().b < p384().p && p384().gx + < p384().p && p384().gy < p384().p) by (compute_only); +} + +// --------------------------------------------------------------------- +// The curve constants as octet strings (SP 800-186 §3.2.1.4). +// --------------------------------------------------------------------- + +/// The 48 big-endian octets of the curve constant `b`. +pub open spec fn b_octets() -> Seq { + seq![0xb3, 0x31, 0x2f, 0xa7, 0xe2, 0x3e, 0xe7, 0xe4, 0x98, 0x8e, 0x05, 0x6b, 0xe3, 0xf8, 0x2d, 0x19, 0x18, 0x1d, 0x9c, 0x6e, 0xfe, 0x81, 0x41, 0x12, 0x03, 0x14, 0x08, 0x8f, 0x50, 0x13, 0x87, 0x5a, 0xc6, 0x56, 0x39, 0x8d, 0x8a, 0x2e, 0xd1, 0x9d, 0x2a, 0x85, 0xc8, 0xed, 0xd3, 0xec, 0x2a, 0xef] +} + +/// `b_octets` is 48 octets and is `b`. +pub proof fn lemma_b_octets() + ensures + b_octets().len() == 48, + os2ip(b_octets()) == p384().b, +{ + assert(b_octets().len() == 48 && os2ip(b_octets()) == p384().b) by (compute_only); +} + +/// The 48 big-endian octets of the curve constant `gx`. +pub open spec fn gx_octets() -> Seq { + seq![0xaa, 0x87, 0xca, 0x22, 0xbe, 0x8b, 0x05, 0x37, 0x8e, 0xb1, 0xc7, 0x1e, 0xf3, 0x20, 0xad, 0x74, 0x6e, 0x1d, 0x3b, 0x62, 0x8b, 0xa7, 0x9b, 0x98, 0x59, 0xf7, 0x41, 0xe0, 0x82, 0x54, 0x2a, 0x38, 0x55, 0x02, 0xf2, 0x5d, 0xbf, 0x55, 0x29, 0x6c, 0x3a, 0x54, 0x5e, 0x38, 0x72, 0x76, 0x0a, 0xb7] +} + +/// `gx_octets` is 48 octets and is `gx`. +pub proof fn lemma_gx_octets() + ensures + gx_octets().len() == 48, + os2ip(gx_octets()) == p384().gx, +{ + assert(gx_octets().len() == 48 && os2ip(gx_octets()) == p384().gx) by (compute_only); +} + +/// The 48 big-endian octets of the curve constant `gy`. +pub open spec fn gy_octets() -> Seq { + seq![0x36, 0x17, 0xde, 0x4a, 0x96, 0x26, 0x2c, 0x6f, 0x5d, 0x9e, 0x98, 0xbf, 0x92, 0x92, 0xdc, 0x29, 0xf8, 0xf4, 0x1d, 0xbd, 0x28, 0x9a, 0x14, 0x7c, 0xe9, 0xda, 0x31, 0x13, 0xb5, 0xf0, 0xb8, 0xc0, 0x0a, 0x60, 0xb1, 0xce, 0x1d, 0x7e, 0x81, 0x9d, 0x7a, 0x43, 0x1d, 0x7c, 0x90, 0xea, 0x0e, 0x5f] +} + +/// `gy_octets` is 48 octets and is `gy`. +pub proof fn lemma_gy_octets() + ensures + gy_octets().len() == 48, + os2ip(gy_octets()) == p384().gy, +{ + assert(gy_octets().len() == 48 && os2ip(gy_octets()) == p384().gy) by (compute_only); +} + +// --------------------------------------------------------------------- +// The doubling's slope numerator, 3 x^2 + a. +// --------------------------------------------------------------------- + +/// What the code computes for `3 x1^2 + a`: three copies of `x1 x1 mod m` +/// added modulo `m`, then `a`. +pub proof fn lemma_dbl_num(m: nat, x: nat, a: nat) + requires + m > 0, + x < m, + a < m, + ensures + ({ + let xx = x * x % m; + let t2 = (xx + xx) % m; + let t3 = (t2 + xx) % m; + (t3 + a) % m == (3 * x * x + a) % m + }), +{ + let xx = x * x % m; + vstd::arithmetic::div_mod::lemma_small_mod(xx, m) ; + // xx < m here since it is a remainder. + assert(xx < m) by { + vstd::arithmetic::div_mod::lemma_mod_bound((x * x) as int, m as int); + } + vstd::arithmetic::div_mod::lemma_small_mod(xx, m); + vstd::arithmetic::div_mod::lemma_add_mod_noop(xx as int, xx as int, m as int); + let t2 = (xx + xx) % m; + vstd::arithmetic::div_mod::lemma_add_mod_noop(t2 as int, xx as int, m as int); + vstd::arithmetic::div_mod::lemma_add_mod_noop((xx + xx) as int, xx as int, m as int); + // t3 = (3 xx) mod m. + let t3 = (t2 + xx) % m; + assert(t3 == (xx + xx + xx) % m); + vstd::arithmetic::div_mod::lemma_small_mod(a, m); + vstd::arithmetic::div_mod::lemma_add_mod_noop((xx + xx + xx) as int, a as int, m as int); + vstd::arithmetic::div_mod::lemma_add_mod_noop(t3 as int, a as int, m as int); + // (3 xx + a) = (3 x x + a) mod m since xx = x x mod m. + assert(3 * x * x == 3 * (x * x)) by (nonlinear_arith); + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right(3int, (x * x) as int, m as int); + assert((xx + xx + xx) == 3 * xx) by (nonlinear_arith) + requires + true, + ; + vstd::arithmetic::div_mod::lemma_add_mod_noop((3 * xx) as int, a as int, m as int); + vstd::arithmetic::div_mod::lemma_add_mod_noop((3 * (x * x)) as int, a as int, m as int); +} + +// --------------------------------------------------------------------- +// The curve equation's right-hand side, x^3 + a x + b. +// --------------------------------------------------------------------- + +/// What the code computes for `x^3 + a x + b`. +pub proof fn lemma_rhs(m: nat, x: nat, a: nat, b: nat) + requires + m > 0, + b < m, + ensures + ({ + let x2 = x * x % m; + let x3 = x2 * x % m; + let ax = a * x % m; + ((x3 + ax) % m + b) % m == (x * x * x + a * x + b) % m + }), +{ + let x2 = x * x % m; + let x3 = x2 * x % m; + let ax = a * x % m; + vstd::arithmetic::div_mod::lemma_mul_mod_noop_left((x * x) as int, x as int, m as int); + assert(x * x * x == (x * x) * x); + // x3 = (x x x) mod m + vstd::arithmetic::div_mod::lemma_add_mod_noop((x * x * x) as int, (a * x) as int, m as int); + vstd::arithmetic::div_mod::lemma_add_mod_noop(x3 as int, ax as int, m as int); + vstd::arithmetic::div_mod::lemma_small_mod(b, m); + vstd::arithmetic::div_mod::lemma_add_mod_noop((x * x * x + a * x) as int, b as int, m as int); + vstd::arithmetic::div_mod::lemma_add_mod_noop(((x3 + ax) % m) as int, b as int, m as int); +} + +// --------------------------------------------------------------------- +// FIPS 186-5 step 3: the digest as bits, and as an integer. +// --------------------------------------------------------------------- + +/// `two_to` at the eight shifts of one octet. +proof fn lemma_two_to_small() + ensures + two_to(0) == 1, + two_to(1) == 2, + two_to(2) == 4, + two_to(3) == 8, + two_to(4) == 16, + two_to(5) == 32, + two_to(6) == 64, + two_to(7) == 128, +{ + assert(two_to(0) == 1 && two_to(1) == 2 && two_to(2) == 4 && two_to(3) == 8 && two_to(4) == 16 + && two_to(5) == 32 && two_to(6) == 64 && two_to(7) == 128) by (compute_only); +} + +/// The eight binary digits of an octet add up to it. +proof fn lemma_octet_digits(b: u32) + requires + b < 256, + ensures + ((b / 128) % 2) * 128 + ((b / 64) % 2) * 64 + ((b / 32) % 2) * 32 + ((b / 16) % 2) * 16 + + ((b / 8) % 2) * 8 + ((b / 4) % 2) * 4 + ((b / 2) % 2) * 2 + b % 2 == b, +{ + assert(((b / 128) % 2) * 128 + ((b / 64) % 2) * 64 + ((b / 32) % 2) * 32 + ((b / 16) % 2) * 16 + + ((b / 8) % 2) * 8 + ((b / 4) % 2) * 4 + ((b / 2) % 2) * 2 + b % 2 == b) by (bit_vector) + requires + b < 256, + ; +} + +/// One more bit is Horner's step. +proof fn lemma_bits_take_step(h: Seq, n: int) + requires + 0 < n <= h.len(), + ensures + bits_to_int(h.take(n)) == bits_to_int(h.take(n - 1)) * 2 + (if h[n - 1] { + 1nat + } else { + 0nat + }), +{ + assert(h.take(n).drop_last() =~= h.take(n - 1)); + assert(h.take(n).last() == h[n - 1]); +} + +/// Appending one octet `b` to `g` appends its eight bits, most significant +/// first, and `bits_to_int` is Horner's rule over them: the integer of the +/// bits of `g` times 256, plus `b`. +proof fn lemma_bits_push_octet(g: Seq, b: u8) + ensures + bits_to_int(octets_to_bits(g.push(b))) == bits_to_int(octets_to_bits(g)) * 256 + b as nat, +{ + lemma_two_to_small(); + let hh = octets_to_bits(g.push(b)); + let l: int = 8 * g.len() as int; + assert(hh.len() == l + 8); + assert(hh.take(l) =~= octets_to_bits(g)) by { + assert forall|i: int| #![auto] 0 <= i < l implies hh.take(l)[i] == octets_to_bits(g)[i] by { + assert(g.push(b)[i / 8] == g[i / 8]); + } + } + lemma_bits_take_step(hh, l + 1); + lemma_bits_take_step(hh, l + 2); + lemma_bits_take_step(hh, l + 3); + lemma_bits_take_step(hh, l + 4); + lemma_bits_take_step(hh, l + 5); + lemma_bits_take_step(hh, l + 6); + lemma_bits_take_step(hh, l + 7); + lemma_bits_take_step(hh, l + 8); + assert(hh.take(l + 8) =~= hh); + // The eight bits are those of b. + assert(g.push(b)[g.len() as int] == b); + assert((l + 0) / 8 == g.len() && (l + 0) % 8 == 0); + assert((l + 1) / 8 == g.len() && (l + 1) % 8 == 1); + assert((l + 2) / 8 == g.len() && (l + 2) % 8 == 2); + assert((l + 3) / 8 == g.len() && (l + 3) % 8 == 3); + assert((l + 4) / 8 == g.len() && (l + 4) % 8 == 4); + assert((l + 5) / 8 == g.len() && (l + 5) % 8 == 5); + assert((l + 6) / 8 == g.len() && (l + 6) % 8 == 6); + assert((l + 7) / 8 == g.len() && (l + 7) % 8 == 7); + let x = bits_to_int(octets_to_bits(g)); + let bb = b as nat; + let d0 = if hh[l] { 1nat } else { 0nat }; + let d1 = if hh[l + 1] { 1nat } else { 0nat }; + let d2 = if hh[l + 2] { 1nat } else { 0nat }; + let d3 = if hh[l + 3] { 1nat } else { 0nat }; + let d4 = if hh[l + 4] { 1nat } else { 0nat }; + let d5 = if hh[l + 5] { 1nat } else { 0nat }; + let d6 = if hh[l + 6] { 1nat } else { 0nat }; + let d7 = if hh[l + 7] { 1nat } else { 0nat }; + assert(d0 == (bb / 128) % 2); + assert(d1 == (bb / 64) % 2); + assert(d2 == (bb / 32) % 2); + assert(d3 == (bb / 16) % 2); + assert(d4 == (bb / 8) % 2); + assert(d5 == (bb / 4) % 2); + assert(d6 == (bb / 2) % 2); + assert(bb / two_to(0) == bb) by (nonlinear_arith) + requires + two_to(0) == 1, + ; + assert(d7 == bb % 2); + lemma_octet_digits(b as u32); + assert(d0 * 128 + d1 * 64 + d2 * 32 + d3 * 16 + d4 * 8 + d5 * 4 + d6 * 2 + d7 == bb); + assert(bits_to_int(hh.take(l)) == x); + assert(bits_to_int(hh) == x * 256 + bb); +} + +/// The bits of an octet string, read as an integer, are its `os2ip` +/// (SEC 1 §2.3.2 followed by FIPS 186-5 B.2.1 is SEC 1 §2.3.8). +pub proof fn lemma_bits_os2ip(h: Seq) + ensures + bits_to_int(octets_to_bits(h)) == os2ip(h), + decreases h.len(), +{ + if h.len() == 0 { + assert(octets_to_bits(h) =~= Seq::::empty()); + } else { + let g = h.drop_last(); + lemma_bits_os2ip(g); + lemma_bits_push_octet(g, h.last()); + assert(g.push(h.last()) =~= h); + } +} + +/// FIPS 186-5 §6.4.2 step 3 for P-384: `derive_e` keeps the first +/// `min(|h|, 48)` octets of the digest and reads them as an integer, which +/// is below 2^384, so it fits in 48 octets. (`⌈log2 n⌉ = 384`.) +pub proof fn lemma_derive_e(h: Seq) + ensures + derive_e(p384(), h) == os2ip(h.subrange(0, if h.len() <= 48 { + h.len() as int + } else { + 48int + })), +{ + assert(ceil_log2(p384().n) == 384) by (compute_only); + let hbits = octets_to_bits(h); + assert(hbits.len() == 8 * h.len()); + if h.len() <= 48 { + assert(h.subrange(0, h.len() as int) =~= h); + lemma_bits_os2ip(h); + } else { + let h48 = h.subrange(0, 48); + assert(hbits.take(384) =~= octets_to_bits(h48)) by { + assert forall|i: int| #![auto] 0 <= i < 384 implies hbits.take(384)[i] == octets_to_bits(h48)[i] by { + assert(h48[i / 8] == h[i / 8]); + } + } + lemma_bits_os2ip(h48); + } +} + +} // verus! diff --git a/crates/clazel-p384/src/lib.rs b/crates/clazel-p384/src/lib.rs index 94322e8..1e47f9e 100644 --- a/crates/clazel-p384/src/lib.rs +++ b/crates/clazel-p384/src/lib.rs @@ -1,11 +1,16 @@ //! ECDSA signature verification over NIST P-384, FIPS 186-5 §6.4.2. //! -//! **Specification and field arithmetic so far.** There is no point code -//! and no `verify` function yet. What is here is the part a person reviews, -//! the meaning of "a valid ECDSA P-384 signature", written in Verus, the -//! contract the later implementation must meet, and the field arithmetic -//! modulo p and n: fiat-crypto's Montgomery code behind six axioms, with the -//! rest (conversions, octet strings, `pow`, `inv`) proven over them. +//! **Specification, field arithmetic, point arithmetic and `verify`.** What +//! is here is the part a person reviews, the meaning of "a valid ECDSA P-384 +//! signature", written in Verus, the contract the implementation is proven +//! to meet, the field arithmetic modulo p and n (fiat-crypto's Montgomery +//! code behind six axioms, with the rest proven over them), and on top of +//! that the affine group law, the scalar product, the key decoding and +//! [`verify::verify`], each proven against [`spec`] over those six axioms and +//! nothing else. The crate is still at tier 0: the evidence tier 1 and tier 2 +//! require beyond these proofs (Kani harnesses, an independent +//! transcription, certified mutations of the code, conformance against +//! Wycheproof and ACVP) is not written yet. //! //! This is public-key *verification* only: the key, the signature and the //! digest are all public, so there is no constant-time requirement and no @@ -16,9 +21,18 @@ //! routines it defers to (SP 800-186 Appendices D.1 and F.1, SEC 1 //! §2.2.1, §2.3, §3.2.2.1 and §4.1.4), the P-384 domain parameters, and a //! toy curve for evaluated examples. -//! - [`contract`]: what the executable `verify` will be proven to satisfy. +//! - [`contract`]: what the executable `verify` is proven to satisfy, and +//! [`point_contract`], the same for the group law, the scalar product, the +//! key decoding and the digest's reduction. //! - [`examples`]: known answers, proven by evaluating the spec. //! - [`field`]: the field arithmetic, over fiat-crypto, with its contracts. +//! - [`point`]: affine points and SEC 1 §2.2.1's group law, and the key +//! decoding (SEC 1 §2.3.4, SP 800-186 D.1.1.1). +//! - [`scalar`]: MSB-first double-and-add against `spec::scalar_mul`, and the +//! digest's step 3 and reduction mod n. +//! - [`verify`]: FIPS 186-5 §6.4.2. +//! - [`convert`] and [`lemmas`]: small conversions and the facts the proofs +//! above use. //! - [`axioms`]: the six calls into fiat-crypto, each an axiom. //! - [`certificates`]: the host module for mutation kill certificates //! (empty until `mutations.json` exists). @@ -26,7 +40,12 @@ pub mod axioms; pub mod certificates; pub mod contract; +pub mod convert; pub mod examples; pub mod field; +pub mod lemmas; +pub mod point; pub mod point_contract; +pub mod scalar; pub mod spec; +pub mod verify; diff --git a/crates/clazel-p384/src/point.rs b/crates/clazel-p384/src/point.rs new file mode 100644 index 0000000..b5bd58b --- /dev/null +++ b/crates/clazel-p384/src/point.rs @@ -0,0 +1,454 @@ +//! Points of P-384 and the group law, executable and proven against +//! [`crate::spec`]. Affine coordinates, SEC 1 §2.2.1's rules in the spec's +//! order; every branch performs the spec's field operations on [`Fe`]s modulo +//! p, so each proof is a composition of the field contracts. The key decoding +//! (SEC 1 §2.3.4, §2.3.6 and SP 800-186 D.1.1.1) is here too. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +use crate::convert::fe_of_byte; +use crate::field::Fe; + +/// A point of the curve: the point at infinity, or an affine pair of +/// residues modulo p. Its view is the spec's [`crate::spec::Point`] with +/// those residues as coordinates. +pub enum Point { + /// The identity element, `O`. + Infinity, + /// `(x, y)`, both residues modulo p (see [`Point::wf`]). + Affine { + /// The x-coordinate. + x: Fe, + /// The y-coordinate. + y: Fe, + }, +} + +impl View for Point { + type V = crate::spec::Point; + + open spec fn view(&self) -> crate::spec::Point { + match self { + Point::Infinity => crate::spec::Point::Infinity, + Point::Affine { x, y } => crate::spec::Point::Affine { x: x.val(), y: y.val() }, + } + } +} + +impl Point { + /// Both coordinates are residues modulo p, not modulo n. (They are below + /// p by the type invariant of [`Fe`], as modelling choice 4 of + /// [`crate::spec`] has it.) + pub open spec fn wf(&self) -> bool { + match self { + Point::Infinity => true, + Point::Affine { x, y } => x.which() == crate::field::spec::Which::P && y.which() == crate::field::spec::Which::P, + } + } + + /// A copy. + pub fn dup(&self) -> (r: Point) + requires + self.wf(), + ensures + r.wf(), + r@ == self@, + { + match self { + Point::Infinity => Point::Infinity, + Point::Affine { x, y } => Point::Affine { x: x.dup(), y: y.dup() }, + } + } +} + +/// The views of an optional point. +pub open spec fn opt_view(o: &Option) -> Option { + match o { + Some(p) => Some(p@), + None => None, + } +} + +/// An optional point is well formed. +pub open spec fn opt_wf(o: &Option) -> bool { + match o { + Some(p) => p.wf(), + None => true, + } +} + +/// The residue 0 modulo p. +fn zero_p() -> (r: Fe) + ensures + r.which() == crate::field::spec::Which::P, + r.val() == 0, +{ + fe_of_byte(crate::field::spec::Which::P, 0) +} + +/// The curve constant b as a residue modulo p. +fn const_b() -> (r: Fe) + ensures + r.which() == crate::field::spec::Which::P, + r.val() == p384().b, +{ + let o: [u8; 48] = [0xb3, 0x31, 0x2f, 0xa7, 0xe2, 0x3e, 0xe7, 0xe4, 0x98, 0x8e, 0x05, 0x6b, 0xe3, 0xf8, 0x2d, 0x19, 0x18, 0x1d, 0x9c, 0x6e, 0xfe, 0x81, 0x41, 0x12, 0x03, 0x14, 0x08, 0x8f, 0x50, 0x13, 0x87, 0x5a, 0xc6, 0x56, 0x39, 0x8d, 0x8a, 0x2e, 0xd1, 0x9d, 0x2a, 0x85, 0xc8, 0xed, 0xd3, 0xec, 0x2a, 0xef]; + proof { + crate::lemmas::lemma_b_octets(); + crate::lemmas::lemma_curve_a(); + assert(o@ =~= crate::lemmas::b_octets()); + } + match Fe::from_octets(crate::field::spec::Which::P, &o) { + Some(f) => f, + // Unreachable: os2ip(o) = b < p. + None => { + proof { + assert(false); + } + Fe::one(crate::field::spec::Which::P) + }, + } +} + +/// The curve constant Gx as a residue modulo p. +fn const_gx() -> (r: Fe) + ensures + r.which() == crate::field::spec::Which::P, + r.val() == p384().gx, +{ + let o: [u8; 48] = [0xaa, 0x87, 0xca, 0x22, 0xbe, 0x8b, 0x05, 0x37, 0x8e, 0xb1, 0xc7, 0x1e, 0xf3, 0x20, 0xad, 0x74, 0x6e, 0x1d, 0x3b, 0x62, 0x8b, 0xa7, 0x9b, 0x98, 0x59, 0xf7, 0x41, 0xe0, 0x82, 0x54, 0x2a, 0x38, 0x55, 0x02, 0xf2, 0x5d, 0xbf, 0x55, 0x29, 0x6c, 0x3a, 0x54, 0x5e, 0x38, 0x72, 0x76, 0x0a, 0xb7]; + proof { + crate::lemmas::lemma_gx_octets(); + crate::lemmas::lemma_curve_a(); + assert(o@ =~= crate::lemmas::gx_octets()); + } + match Fe::from_octets(crate::field::spec::Which::P, &o) { + Some(f) => f, + // Unreachable: os2ip(o) = gx < p. + None => { + proof { + assert(false); + } + Fe::one(crate::field::spec::Which::P) + }, + } +} + +/// The curve constant Gy as a residue modulo p. +fn const_gy() -> (r: Fe) + ensures + r.which() == crate::field::spec::Which::P, + r.val() == p384().gy, +{ + let o: [u8; 48] = [0x36, 0x17, 0xde, 0x4a, 0x96, 0x26, 0x2c, 0x6f, 0x5d, 0x9e, 0x98, 0xbf, 0x92, 0x92, 0xdc, 0x29, 0xf8, 0xf4, 0x1d, 0xbd, 0x28, 0x9a, 0x14, 0x7c, 0xe9, 0xda, 0x31, 0x13, 0xb5, 0xf0, 0xb8, 0xc0, 0x0a, 0x60, 0xb1, 0xce, 0x1d, 0x7e, 0x81, 0x9d, 0x7a, 0x43, 0x1d, 0x7c, 0x90, 0xea, 0x0e, 0x5f]; + proof { + crate::lemmas::lemma_gy_octets(); + crate::lemmas::lemma_curve_a(); + assert(o@ =~= crate::lemmas::gy_octets()); + } + match Fe::from_octets(crate::field::spec::Which::P, &o) { + Some(f) => f, + // Unreachable: os2ip(o) = gy < p. + None => { + proof { + assert(false); + } + Fe::one(crate::field::spec::Which::P) + }, + } +} + +/// The curve coefficient `a = p - 3` as a residue modulo p. +fn const_a() -> (r: Fe) + ensures + r.which() == crate::field::spec::Which::P, + r.val() == p384().a, +{ + let zero = zero_p(); + let three = fe_of_byte(crate::field::spec::Which::P, 3); + proof { + crate::lemmas::lemma_curve_a(); + crate::lemmas::lemma_modulus_gt_256(crate::field::spec::Which::P); + vstd::arithmetic::div_mod::lemma_small_mod( + (p384().p - 3) as nat, + p384().p, + ); + } + zero.sub(&three) +} + +/// The base point `G` (SP 800-186 §3.2.1.4). +pub fn base() -> (r: Point) + ensures + r.wf(), + r@ == base_point(p384()), +{ + Point::Affine { x: const_gx(), y: const_gy() } +} + +/// Rule 4 of SEC 1 §2.2.1: two points with different x-coordinates. +fn add_distinct(x1: &Fe, y1: &Fe, x2: &Fe, y2: &Fe) -> (r: Option) + requires + x1.which() == crate::field::spec::Which::P, + y1.which() == crate::field::spec::Which::P, + x2.which() == crate::field::spec::Which::P, + y2.which() == crate::field::spec::Which::P, + x1.val() != x2.val(), + ensures + opt_wf(&r), + crate::point_contract::ec_add_ensures( + crate::spec::Point::Affine { x: x1.val(), y: y1.val() }, + crate::spec::Point::Affine { x: x2.val(), y: y2.val() }, + opt_view(&r), + ), +{ + let d = x2.sub(x1); + match d.inv() { + None => None, + Some(w) => { + let num = y2.sub(y1); + let lambda = num.mul(&w); + let l2 = lambda.mul(&lambda); + let t = l2.sub(x1); + let x3 = t.sub(x2); + let u = x1.sub(&x3); + let lu = lambda.mul(&u); + let y3 = lu.sub(y1); + Some(Point::Affine { x: x3, y: y3 }) + }, + } +} + +/// Rule 5 of SEC 1 §2.2.1: a point added to itself (the case of equal +/// x-coordinates that is not rule 3). +fn add_double(x1: &Fe, y1: &Fe, _x2: &Fe, _y2: &Fe) -> (r: Option) + requires + x1.which() == crate::field::spec::Which::P, + y1.which() == crate::field::spec::Which::P, + _x2.which() == crate::field::spec::Which::P, + _y2.which() == crate::field::spec::Which::P, + x1.val() == _x2.val(), + (y1.val() + _y2.val()) % crate::field::spec::modulus(crate::field::spec::Which::P) != 0, + ensures + opt_wf(&r), + crate::point_contract::ec_add_ensures( + crate::spec::Point::Affine { x: x1.val(), y: y1.val() }, + crate::spec::Point::Affine { x: _x2.val(), y: _y2.val() }, + opt_view(&r), + ), +{ + let two_y = y1.add(y1); + match two_y.inv() { + None => None, + Some(w) => { + let xx = x1.mul(x1); + let xx2 = xx.add(&xx); + let xx3 = xx2.add(&xx); + let ca = const_a(); + let num = xx3.add(&ca); + let lambda = num.mul(&w); + let l2 = lambda.mul(&lambda); + let two_x = x1.add(x1); + let x3 = l2.sub(&two_x); + let u = x1.sub(&x3); + let lu = lambda.mul(&u); + let y3 = lu.sub(y1); + x1.val_lt_modulus(); + proof { + crate::lemmas::lemma_curve_a(); + crate::lemmas::lemma_dbl_num(crate::field::spec::modulus(crate::field::spec::Which::P), x1.val(), p384().a); + } + Some(Point::Affine { x: x3, y: y3 }) + }, + } +} + +/// `a + b`: SEC 1 §2.2.1, [`crate::spec::ec_add`]. +pub fn ec_add(a: &Point, b: &Point) -> (r: Option) + requires + a.wf(), + b.wf(), + ensures + opt_wf(&r), + crate::point_contract::ec_add_ensures(a@, b@, opt_view(&r)), +{ + match (a, b) { + // SEC 1 §2.2.1 rule 1: O + O = O. + (Point::Infinity, Point::Infinity) => Some(Point::Infinity), + // Rule 2: (x, y) + O = O + (x, y) = (x, y). + (Point::Infinity, Point::Affine { .. }) => Some(b.dup()), + (Point::Affine { .. }, Point::Infinity) => Some(a.dup()), + (Point::Affine { x: x1, y: y1 }, Point::Affine { x: x2, y: y2 }) => { + let zero = zero_p(); + let same_x = x1.equals(x2); + let ysum = y1.add(y2); + let ysum_zero = ysum.equals(&zero); + if same_x && ysum_zero { + // Rule 3: (x, y) + (x, -y) = O. + Some(Point::Infinity) + } else if !same_x { + add_distinct(x1, y1, x2, y2) + } else { + add_double(x1, y1, x2, y2) + } + }, + } +} + +/// The octet `q[i]` (a zero if there is none, which `requires` rules out). +fn at(q: &[u8], i: usize) -> (b: u8) + requires + i < q.len(), + ensures + b == q@[i as int], +{ + match q.get(i) { + Some(b) => *b, + None => 0, + } +} + +/// The 48 octets `q[off..off + 48]`. +fn copy48(q: &[u8], off: usize) -> (o: [u8; 48]) + requires + off + 48 <= q.len(), + ensures + o@ == q@.subrange(off as int, off as int + 48), +{ + let o = [ + at(q, off.saturating_add(0)), + at(q, off.saturating_add(1)), + at(q, off.saturating_add(2)), + at(q, off.saturating_add(3)), + at(q, off.saturating_add(4)), + at(q, off.saturating_add(5)), + at(q, off.saturating_add(6)), + at(q, off.saturating_add(7)), + at(q, off.saturating_add(8)), + at(q, off.saturating_add(9)), + at(q, off.saturating_add(10)), + at(q, off.saturating_add(11)), + at(q, off.saturating_add(12)), + at(q, off.saturating_add(13)), + at(q, off.saturating_add(14)), + at(q, off.saturating_add(15)), + at(q, off.saturating_add(16)), + at(q, off.saturating_add(17)), + at(q, off.saturating_add(18)), + at(q, off.saturating_add(19)), + at(q, off.saturating_add(20)), + at(q, off.saturating_add(21)), + at(q, off.saturating_add(22)), + at(q, off.saturating_add(23)), + at(q, off.saturating_add(24)), + at(q, off.saturating_add(25)), + at(q, off.saturating_add(26)), + at(q, off.saturating_add(27)), + at(q, off.saturating_add(28)), + at(q, off.saturating_add(29)), + at(q, off.saturating_add(30)), + at(q, off.saturating_add(31)), + at(q, off.saturating_add(32)), + at(q, off.saturating_add(33)), + at(q, off.saturating_add(34)), + at(q, off.saturating_add(35)), + at(q, off.saturating_add(36)), + at(q, off.saturating_add(37)), + at(q, off.saturating_add(38)), + at(q, off.saturating_add(39)), + at(q, off.saturating_add(40)), + at(q, off.saturating_add(41)), + at(q, off.saturating_add(42)), + at(q, off.saturating_add(43)), + at(q, off.saturating_add(44)), + at(q, off.saturating_add(45)), + at(q, off.saturating_add(46)), + at(q, off.saturating_add(47)), + ]; + proof { + assert(o@ =~= q@.subrange(off as int, off as int + 48)); + } + o +} + +/// `x^3 + a x + b` modulo p: [`crate::spec::curve_rhs`]. +fn rhs_fe(x: &Fe) -> (r: Fe) + requires + x.which() == crate::field::spec::Which::P, + ensures + r.which() == crate::field::spec::Which::P, + r.val() == curve_rhs(p384(), x.val()), +{ + let x2 = x.mul(x); + let x3 = x2.mul(x); + let ca = const_a(); + let ax = ca.mul(x); + let s = x3.add(&ax); + let cb = const_b(); + let r = s.add(&cb); + proof { + crate::lemmas::lemma_curve_a(); + crate::lemmas::lemma_rhs(crate::field::spec::modulus(crate::field::spec::Which::P), x.val(), p384().a, p384().b); + } + r +} + +/// `y^2 = x^3 + a x + b` modulo p: [`crate::spec::satisfies_equation`]. +fn on_curve(x: &Fe, y: &Fe) -> (r: bool) + requires + x.which() == crate::field::spec::Which::P, + y.which() == crate::field::spec::Which::P, + ensures + r == satisfies_equation(p384(), x.val(), y.val()), +{ + let lhs = y.mul(y); + let rhs = rhs_fe(x); + lhs.equals(&rhs) +} + +/// The key `q` decoded and validated: SEC 1 §2.3.4 (octet string to point, +/// uncompressed form only: choice 7 of [`crate::spec`]) and SP 800-186 +/// D.1.1.1, [`crate::spec::decode_public_key`]. +pub fn decode_public_key(q: &[u8]) -> (r: Option) + ensures + opt_wf(&r), + crate::point_contract::decode_public_key_ensures(q@, opt_view(&r)), +{ + // SEC 1 §2.3.4: the input has one of three lengths; the point at + // infinity (`00`, length 1), the compressed form (length 49) and any + // other length give no valid key. + if q.len() != 97 { + return None; + } + // Step 3.2: W must be 04. + let w: u8 = at(q, 0); + if w != 4 { + return None; + } + // Step 3.1: parse W || X || Y. + let xs = copy48(q, 1); + let ys = copy48(q, 49); + // Steps 3.3 and 3.4: X and Y are field elements (§2.3.6). + let x = Fe::from_octets(crate::field::spec::Which::P, &xs); + let y = Fe::from_octets(crate::field::spec::Which::P, &ys); + match (x, y) { + (Some(x), Some(y)) => { + // Step 3.5: the defining equation. + if on_curve(&x, &y) { + // Step 3.6, and the validation of D.1.1.1 (infinity is + // refused by construction, the coordinates are below p). + Some(Point::Affine { x, y }) + } else { + None + } + }, + _ => None, + } +} + +} // verus! diff --git a/crates/clazel-p384/src/scalar.rs b/crates/clazel-p384/src/scalar.rs new file mode 100644 index 0000000..5e83488 --- /dev/null +++ b/crates/clazel-p384/src/scalar.rs @@ -0,0 +1,218 @@ +//! The scalar product `[k] P` and the reduction of the digest, executable +//! and proven against [`crate::spec`]. `[k] P` is MSB-first double-and-add +//! over [`crate::point::ec_add`], one bit at a time, exactly the recursion of +//! [`crate::spec::scalar_mul`] (`[2q + b] P = ([q] P + [q] P) + b P`), so the +//! invariant of the loop is that after the top `i` bits the accumulator is +//! the spec's product by the integer those bits make, and nothing about the +//! group law beyond its own definition is used. Every input is public, so +//! the loop branches on the bits. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +use crate::field::Fe; +use crate::point::{ec_add, Point}; + +/// A bit as a number. +spec fn bit_nat(b: bool) -> nat { + if b { + 1 + } else { + 0 + } +} + +/// The spec's recursion for `[2q + b] P`, in terms of `[q] P`: a doubling, +/// then the addition of `P` if the bit is set. +pub open spec fn mul_step_spec(h: Option, pt: crate::spec::Point, bit: bool) -> Option< + crate::spec::Point, +> { + match h { + None => None, + Some(h) => match crate::spec::ec_add(p384(), h, h) { + None => None, + Some(twice) => if bit { + crate::spec::ec_add(p384(), twice, pt) + } else { + Some(twice) + }, + }, + } +} + +/// `[2q + b] P` is one step from `[q] P`: the definition of `scalar_mul`, +/// including for `q = 0` and `b = 0`, where both sides are `O` (`O + O = O`). +proof fn lemma_mul_step(q: nat, bit: bool, pt: crate::spec::Point) + ensures + crate::spec::scalar_mul(p384(), 2 * q + bit_nat(bit), pt) == mul_step_spec( + crate::spec::scalar_mul(p384(), q, pt), + pt, + bit, + ), +{ + let k = 2 * q + bit_nat(bit); + if k == 0 { + assert(q == 0 && !bit); + assert(crate::spec::scalar_mul(p384(), 0, pt) == Some(crate::spec::Point::Infinity)); + } else { + assert(k / 2 == q); + assert(k % 2 == bit_nat(bit)); + } +} + +/// Take the bit worth `t` off `rem`: whether `rem >= t`, and `rem` without it. +fn split_bit(rem: u8, t: u8) -> (r: (bool, u8)) + ensures + r.0 == (rem >= t), + rem as nat == r.1 as nat + (if r.0 { + t as nat + } else { + 0nat + }), + r.1 <= rem, +{ + if rem >= t { + (true, rem.wrapping_sub(t)) + } else { + (false, rem) + } +} + +/// One bit: the accumulator `[q] P` becomes `[2q + bit] P`. +fn mul_step(acc: Option, pt: &Point, bit: bool, Ghost(q): Ghost) -> (r: Option) + requires + pt.wf(), + crate::point::opt_wf(&acc), + crate::point::opt_view(&acc) == crate::spec::scalar_mul(p384(), q, pt@), + ensures + crate::point::opt_wf(&r), + crate::point::opt_view(&r) == crate::spec::scalar_mul(p384(), 2 * q + bit_nat(bit), pt@), +{ + proof { + lemma_mul_step(q, bit, pt@); + } + match acc { + None => None, + Some(h) => match ec_add(&h, &h) { + None => None, + Some(twice) => if bit { + ec_add(&twice, pt) + } else { + Some(twice) + }, + }, + } +} + +/// Eight bits, most significant first: `[256 q + byte] P` from `[q] P`. +fn mul_byte(acc: Option, pt: &Point, byte: u8, Ghost(q): Ghost) -> (r: Option) + requires + pt.wf(), + crate::point::opt_wf(&acc), + crate::point::opt_view(&acc) == crate::spec::scalar_mul(p384(), q, pt@), + ensures + crate::point::opt_wf(&r), + crate::point::opt_view(&r) == crate::spec::scalar_mul(p384(), q * 256 + byte as nat, pt@), +{ + let (b7, rem) = split_bit(byte, 128); + let acc = mul_step(acc, pt, b7, Ghost(q)); + let ghost q1: nat = 2 * q + bit_nat(b7); + let (b6, rem) = split_bit(rem, 64); + let acc = mul_step(acc, pt, b6, Ghost(q1)); + let ghost q2: nat = 2 * q1 + bit_nat(b6); + let (b5, rem) = split_bit(rem, 32); + let acc = mul_step(acc, pt, b5, Ghost(q2)); + let ghost q3: nat = 2 * q2 + bit_nat(b5); + let (b4, rem) = split_bit(rem, 16); + let acc = mul_step(acc, pt, b4, Ghost(q3)); + let ghost q4: nat = 2 * q3 + bit_nat(b4); + let (b3, rem) = split_bit(rem, 8); + let acc = mul_step(acc, pt, b3, Ghost(q4)); + let ghost q5: nat = 2 * q4 + bit_nat(b3); + let (b2, rem) = split_bit(rem, 4); + let acc = mul_step(acc, pt, b2, Ghost(q5)); + let ghost q6: nat = 2 * q5 + bit_nat(b2); + let (b1, rem) = split_bit(rem, 2); + let acc = mul_step(acc, pt, b1, Ghost(q6)); + let ghost q7: nat = 2 * q6 + bit_nat(b1); + let last = split_bit(rem, 1); + let b0 = last.0; + let acc = mul_step(acc, pt, b0, Ghost(q7)); + proof { + // rem is now 0, and byte = 128 b7 + 64 b6 + ... + b0. + assert(last.1 == 0); + assert(2 * q7 + bit_nat(b0) == q * 256 + byte as nat); + } + acc +} + +/// `[k] pt`, `k` the integer of the 48 big-endian octets: MSB-first +/// double-and-add, [`crate::spec::scalar_mul`]. +pub fn scalar_mul(k: &[u8; 48], pt: &Point) -> (r: Option) + requires + pt.wf(), + ensures + crate::point::opt_wf(&r), + crate::point_contract::scalar_mul_ensures(k@, pt@, crate::point::opt_view(&r)), +{ + let mut acc: Option = Some(Point::Infinity); + let mut i: usize = 0; + let ghost mut q: nat = 0; + proof { + assert(k@.subrange(0, 0) =~= Seq::::empty()); + assert(crate::spec::scalar_mul(p384(), 0, pt@) == Some(crate::spec::Point::Infinity)); + } + while i < 48 + invariant + i <= 48, + pt.wf(), + crate::point::opt_wf(&acc), + q == os2ip(k@.subrange(0, i as int)), + crate::point::opt_view(&acc) == crate::spec::scalar_mul(p384(), q, pt@), + decreases 48 - i, + { + let byte: u8 = match k.get(i) { + Some(b) => *b, + None => 0, + }; + let next = mul_byte(acc, pt, byte, Ghost(q)); + proof { + let pre = k@.subrange(0, i as int); + crate::field::lemmas::lemma_os2ip_push(pre, byte); + assert(k@.subrange(0, i as int + 1) =~= pre.push(byte)); + q = q * 256 + byte as nat; + } + acc = next; + i = i.saturating_add(1); + } + proof { + assert(k@.subrange(0, 48) =~= k@); + } + acc +} + +/// FIPS 186-5 §6.4.2 step 3, with the reduction modulo n that step 5 applies: +/// the integer `e` of [`crate::spec::derive_e`] (the leftmost +/// `min(|H|, 384)` bits of the digest, read as an integer, so below 2^384 and +/// possibly at least n) as a residue modulo n. +pub fn derive_e(digest: &[u8]) -> (r: Fe) + ensures + r.which() == crate::field::spec::Which::N, + crate::point_contract::derive_e_ensures(digest@, r.val()), +{ + let k = if digest.len() <= 48 { + digest.len() + } else { + 48 + }; + proof { + crate::lemmas::lemma_derive_e(digest@); + } + crate::convert::reduce_prefix(crate::field::spec::Which::N, digest, k) +} + +} // verus! diff --git a/crates/clazel-p384/src/verify.rs b/crates/clazel-p384/src/verify.rs new file mode 100644 index 0000000..99bfb7e --- /dev/null +++ b/crates/clazel-p384/src/verify.rs @@ -0,0 +1,88 @@ +//! ECDSA signature verification over NIST P-384, FIPS 186-5 §6.4.2, proven +//! to meet [`crate::contract::verify_ensures`], that is [`crate::spec`]'s +//! `ecdsa_verify`, over the six axioms of [`crate::axioms`]. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +use crate::convert::{fe_of_byte, reduce_prefix}; +use crate::field::Fe; +use crate::point::Point; + +/// `verify(digest, r, s, point)`: FIPS 186-5 §6.4.2 for P-384. +/// +/// `digest` is the hash `H` of step 2 (0 to 64 octets), `r` and `s` are the +/// big-endian octets of the signature integers, and `point` is the key's +/// ECPoint `04 || X || Y`. Returns whether the signature is valid; a key +/// that does not decode (or is not on the curve) is invalid. +pub fn verify(digest: &[u8], r: &[u8; 48], s: &[u8; 48], point: &[u8]) -> (ok: bool) + requires + crate::contract::verify_requires(digest@), + ensures + crate::contract::verify_ensures(digest@, r@, s@, point@, ok), +{ + // The public key, decoded and validated first (modelling choice 8). + let q = match crate::point::decode_public_key(point) { + None => return false, + Some(q) => q, + }; + // Step 1: r and s are integers in [1, n - 1]. `from_octets` refuses an + // integer that is at least n; zero is refused below. + let r_fe = match Fe::from_octets(crate::field::spec::Which::N, r) { + None => return false, + Some(f) => f, + }; + let s_fe = match Fe::from_octets(crate::field::spec::Which::N, s) { + None => return false, + Some(f) => f, + }; + let zero = fe_of_byte(crate::field::spec::Which::N, 0); + if r_fe.equals(&zero) || s_fe.equals(&zero) { + return false; + } + // Step 3: e, reduced modulo n (step 5 reduces it). + let e = crate::scalar::derive_e(digest); + // Step 4: w = s^-1 mod n. + let w = match s_fe.inv() { + None => return false, + Some(w) => w, + }; + // Step 5: u = e w mod n and v = r w mod n. + let u = e.mul(&w); + let v = r_fe.mul(&w); + proof { + crate::field::lemmas::lemma_modulus(crate::field::spec::Which::N); + crate::lemmas::lemma_mul_reduced(derive_e(p384(), digest@), w.val(), p384().n); + } + // Step 6: R1 = [u]G + [v]Q, two separate products. + let uo = u.to_octets(); + let vo = v.to_octets(); + let g = crate::point::base(); + let ug = crate::scalar::scalar_mul(&uo, &g); + let vq = crate::scalar::scalar_mul(&vo, &q); + let r1 = match (ug, vq) { + (Some(a), Some(b)) => crate::point::ec_add(&a, &b), + _ => None, + }; + match r1 { + // Step 6: the identity, or a failed operation, rejects. + None => false, + Some(Point::Infinity) => false, + // Step 7: x_R. Step 8: its integer is itself (F.1). + Some(Point::Affine { x, y: _ }) => { + // Step 9: r = x_R mod n. x_R < p may exceed n, so reduce it. + let xo = x.to_octets(); + let xr = reduce_prefix(crate::field::spec::Which::N, &xo, 48); + proof { + assert(xo@.subrange(0, 48) =~= xo@); + } + xr.equals(&r_fe) + }, + } +} + +} // verus! From f6a97f11fd6da6deddd3b99fd94a7849f2408af8 Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Tue, 27 Oct 2026 12:52:35 +0000 Subject: [PATCH 3/3] test(p384): verify smoke tests with Wycheproof vectors Eight valid and six invalid vectors of ecdsa_secp384r1_sha384_test.json (d17cc89f), plus damaged r, s, digests and keys. Co-Authored-By: Claude Sonnet 5.5 --- crates/clazel-p384/tests/verify.rs | 465 +++++++++++++++++++++++++++++ 1 file changed, 465 insertions(+) create mode 100644 crates/clazel-p384/tests/verify.rs diff --git a/crates/clazel-p384/tests/verify.rs b/crates/clazel-p384/tests/verify.rs new file mode 100644 index 0000000..b52b933 --- /dev/null +++ b/crates/clazel-p384/tests/verify.rs @@ -0,0 +1,465 @@ +//! `clazel_p384::verify::verify` smoke tests: Wycheproof's valid signatures +//! are accepted, and signatures and keys that are damaged in one known way +//! are rejected. Full conformance (every Wycheproof vector, ACVP, a +//! differential against another engine) is for a later change. +//! +//! # Source of the vectors +//! +//! Wycheproof `testvectors_v1/ecdsa_secp384r1_sha384_test.json` at commit +//! `d17cc89fa5c8f4f4d378b5385ebf75da5d0926c9` of +//! (the commit `clazel-pkcs1` pins; +//! Apache-2.0; the file's SHA-256 is +//! `8a5b3ae1760975143414811f13588c24d951d9d8c904195087ba327591dfe9cc`). +//! Each [`Vector`] below is one test of that file, named by its `tcId`: +//! +//! - `key` is the group's `publicKey.uncompressed`, the 97-octet ECPoint; +//! - `digest` is SHA-384 of the test's `msg`, computed with Python's +//! `hashlib` (the verifier takes the digest, not the message, and no hash +//! crate is a test dependency of this crate); +//! - `r` and `s` are the two integers of the test's DER `sig`, parsed with +//! a strict Python DER reader and left-padded to 48 octets. +//! +//! The 14 vectors were chosen to reach different code: pseudorandom and +//! malleable signatures (1, 2, 5, 7), the Shamir edge case (295), digests +//! that are special (296, 297, 300: all-zero, all-one and similar), and, as +//! invalid ones, a changed first octet of r (102), `r = 0` (109), `s = 0` +//! (151), `r = 0, s = n` (171), `r = n, s = n` (195) and `r = n - 1, s = n - 1` +//! (204). The valid ones are `"valid"` in the file and the invalid ones are +//! `"invalid"`; none is `"acceptable"`. + +use clazel_p384::verify::verify; +use std::time::Instant; + +type TestResult = Result<(), String>; + +/// One Wycheproof test, as hexadecimal strings. +struct Vector { + tc_id: u32, + comment: &'static str, + key: &'static str, + digest: &'static str, + r: &'static str, + s: &'static str, +} + +const VALID: &[Vector] = &[ + Vector { + tc_id: 1, + comment: "pseudorandom signature", + key: "0429bdb76d5fa741bfd70233cb3a66cc7d44beb3b0663d92a8136650478bcefb61ef182e155a54345a5e8e5e88f064e5bc9a525ab7f764dad3dae1468c2b419f3b62b9ba917d5e8c4fb1ec47404a3fc76474b2713081be9db4c00e043ada9fc4a3", + digest: "38b060a751ac96384cd9327eb1b1e36a21fdb71114be07434c0cc7bf63f6e1da274edebfe76f65fbd51ad2f14898b95b", + r: "32401249714e9091f05a5e109d5c1216fdc05e98614261aa0dbd9e9cd4415dee29238afbd3b103c1e40ee5c9144aee0f", + s: "4326756fb2c4fd726360dd6479b5849478c7a9d054a833a58c1631c33b63c3441336ddf2c7fe0ed129aae6d4ddfeb753", + }, + Vector { + tc_id: 2, + comment: "pseudorandom signature", + key: "0429bdb76d5fa741bfd70233cb3a66cc7d44beb3b0663d92a8136650478bcefb61ef182e155a54345a5e8e5e88f064e5bc9a525ab7f764dad3dae1468c2b419f3b62b9ba917d5e8c4fb1ec47404a3fc76474b2713081be9db4c00e043ada9fc4a3", + digest: "5340980991c93d7111312700b83e9e61eed0977c5bca41d5dc9e26a7af4dbef3908df6661e32e039842176176609ba8f", + r: "d7143a836608b25599a7f28dec6635494c2992ad1e2bbeecb7ef601a9c01746e710ce0d9c48accb38a79ede5b9638f34", + s: "80f9e165e8c61035bf8aa7b5533960e46dd0e211c904a064edb6de41f797c0eae4e327612ee3f816f4157272bb4fabc9", + }, + Vector { + tc_id: 5, + comment: "signature malleability", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "12b30abef6b5476fe6b612ae557c0425661e26b44b1bfe19daf2ca28e3113083ba8e4ae4cc45a0320abd3394f1c548d7", + s: "1840da9fc1d2f8f8900cf485d5413b8c2574ee3a8d4ca03995ca30240e09513805bf6209b58ac7aa9cff54eecd82b9f1", + }, + Vector { + tc_id: 7, + comment: "valid", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "12b30abef6b5476fe6b612ae557c0425661e26b44b1bfe19daf2ca28e3113083ba8e4ae4cc45a0320abd3394f1c548d7", + s: "e7bf25603e2d07076ff30b7a2abec473da8b11c572b35fc631991d5de62ddca7525aaba89325dfd04fecc47bff426f82", + }, + Vector { + tc_id: 295, + comment: "Edge case for Shamir multiplication", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "1ea4d7e33dd2cad2b412822fb60c29b7280cae718af25c51f907eb101cca981ac86a9d1a9186a1b630fb6e7079385911", + r: "ac042e13ab83394692019170707bc21dd3d7b8d233d11b651757085bdd5767eabbb85322984f14437335de0cdf565684", + s: "bd770d3ee4beadbabe7ca46e8c4702783435228d46e2dd360e322fe61c86926fa49c8116ec940f72ac8c30d9beb3e12f", + }, + Vector { + tc_id: 296, + comment: "special case hash", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "00000000505a3d306890ad438d155166987fcd0d78a44fa79272ef4dcade39c852dcd5a4b23075d7651bb5c57629f198", + r: "d3298a0193c4316b34e3833ff764a82cff4ef57b5dd79ed6237b51ff76ceab13bf92131f41030515b7e012d2ba857830", + s: "bfc7518d2ad20ed5f58f3be79720f1866f7a23b3bd1bf913d3916819d008497a071046311d3c2fd05fc284c964a39617", + }, + Vector { + tc_id: 297, + comment: "special case hash", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "fc000000009322da48a8586f26f148003932f6d4c0d1ce3a21798f7b651dab7642188c9061a66dc9b190e00b0290e264", + r: "e14f41a5fc83aa4725a9ea60ab5b0b9de27f519af4b557a601f1fee0243f8eee5180f8c531414f3473f4457430cb7a26", + s: "1047ed2bf1f98e3ce93e8fdbdc63cc79f238998fee74e1bb6cd708694950bbffe3945066064da043f04d7083d0a596ec", + }, + Vector { + tc_id: 300, + comment: "special case hash", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "3b0f107e00000000c33f3c4431329dc9f62a724c34d1f01d3b3520b01647570625a5d84e7f7770d88ad6b3f195324d65", + r: "9ad363a1bbc67c57c82a378e988cc083cc91f8b32739ec647c0cb348fb5c86472015131a7d9083bf4740af3351755195", + s: "d310dc1509f8c00281efe571768d488027ea760fe32971f6cb7b57cdf90621b7d0086e26443d3761df7aa3a4eccc6c58", + }, +]; + +const INVALID: &[Vector] = &[ + Vector { + tc_id: 102, + comment: "modifying first byte of r", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "10b30abef6b5476fe6b612ae557c0425661e26b44b1bfe19daf2ca28e3113083ba8e4ae4cc45a0320abd3394f1c548d7", + s: "e7bf25603e2d07076ff30b7a2abec473da8b11c572b35fc631991d5de62ddca7525aaba89325dfd04fecc47bff426f82", + }, + Vector { + tc_id: 109, + comment: "replacing r with zero", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + s: "e7bf25603e2d07076ff30b7a2abec473da8b11c572b35fc631991d5de62ddca7525aaba89325dfd04fecc47bff426f82", + }, + Vector { + tc_id: 151, + comment: "replacing s with zero", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "12b30abef6b5476fe6b612ae557c0425661e26b44b1bfe19daf2ca28e3113083ba8e4ae4cc45a0320abd3394f1c548d7", + s: "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + }, + Vector { + tc_id: 171, + comment: "Signature with special case values r=0 and s=n", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + s: "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973", + }, + Vector { + tc_id: 195, + comment: "Signature with special case values r=n and s=n", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973", + s: "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973", + }, + Vector { + tc_id: 204, + comment: "Signature with special case values r=n - 1 and s=n - 1", + key: "042da57dda1089276a543f9ffdac0bff0d976cad71eb7280e7d9bfd9fee4bdb2f20f47ff888274389772d98cc5752138aa4b6d054d69dcf3e25ec49df870715e34883b1836197d76f8ad962e78f6571bbc7407b0d6091f9e4d88f014274406174f", + digest: "f9b127f0d81ebcd17b7ba0ea131c660d340b05ce557c82160e0f793de07d38179023942871acb7002dfafdfffc8deace", + r: "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + s: "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + }, +]; + +/// The order n of P-384 (SP 800-186 §3.2.1.4), 48 octets. +const N: &str = "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973"; +/// The field prime p. +const P: &str = "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff"; + +fn unhex(h: &str) -> Result, String> { + let digits = h.as_bytes(); + if !digits.len().is_multiple_of(2) { + return Err(format!("odd number of hex digits in {h}")); + } + digits + .chunks(2) + .map(|pair| { + let pair = std::str::from_utf8(pair).map_err(|e| e.to_string())?; + u8::from_str_radix(pair, 16).map_err(|e| format!("{pair}: {e}")) + }) + .collect() +} + +fn arr48(h: &str) -> Result<[u8; 48], String> { + let v = unhex(h)?; + <[u8; 48]>::try_from(v.as_slice()).map_err(|_| format!("{} octets, want 48", v.len())) +} + +/// A vector decoded: `(key, digest, r, s)`. +type Decoded = (Vec, Vec, [u8; 48], [u8; 48]); + +fn decode(v: &Vector) -> Result { + Ok((unhex(v.key)?, unhex(v.digest)?, arr48(v.r)?, arr48(v.s)?)) +} + +fn expect(what: &str, got: bool, want: bool) -> TestResult { + if got == want { + Ok(()) + } else { + Err(format!("{what}: verify returned {got}, want {want}")) + } +} + +fn first(set: &'static [Vector]) -> Result<&'static Vector, String> { + set.first().ok_or_else(|| "no vectors".to_string()) +} + +fn vector(set: &'static [Vector], tc_id: u32) -> Result<&'static Vector, String> { + set.iter() + .find(|v| v.tc_id == tc_id) + .ok_or_else(|| format!("no tcId {tc_id}")) +} + +/// Flip one bit of the octet at `at`. +fn flip(o: &mut [u8], at: usize) -> TestResult { + let b = o.get_mut(at).ok_or_else(|| format!("no octet {at}"))?; + *b ^= 0x01; + Ok(()) +} + +#[test] +#[cfg_attr( + miri, + ignore = "a verification is about 1,150 group operations, too slow under Miri" +)] +fn wycheproof_valid_signatures_are_accepted() -> TestResult { + for v in VALID { + let (key, digest, r, s) = decode(v)?; + let start = Instant::now(); + let ok = verify(&digest, &r, &s, &key); + eprintln!("tcId {} ({}): {:?}", v.tc_id, v.comment, start.elapsed()); + expect(&format!("tcId {} ({})", v.tc_id, v.comment), ok, true)?; + } + Ok(()) +} + +#[test] +#[cfg_attr( + miri, + ignore = "a verification is about 1,150 group operations, too slow under Miri" +)] +fn wycheproof_invalid_signatures_are_rejected() -> TestResult { + for v in INVALID { + let (key, digest, r, s) = decode(v)?; + expect( + &format!("tcId {} ({})", v.tc_id, v.comment), + verify(&digest, &r, &s, &key), + false, + )?; + } + Ok(()) +} + +#[test] +#[cfg_attr( + miri, + ignore = "a verification is about 1,150 group operations, too slow under Miri" +)] +fn tampered_r_and_s_are_rejected() -> TestResult { + let v = first(VALID)?; + let (key, digest, r, s) = decode(v)?; + expect("untouched", verify(&digest, &r, &s, &key), true)?; + for at in [0, 23, 47] { + let mut r2 = r; + flip(&mut r2, at)?; + expect( + &format!("r octet {at} flipped"), + verify(&digest, &r2, &s, &key), + false, + )?; + let mut s2 = s; + flip(&mut s2, at)?; + expect( + &format!("s octet {at} flipped"), + verify(&digest, &r, &s2, &key), + false, + )?; + } + Ok(()) +} + +#[test] +#[cfg_attr( + miri, + ignore = "a verification is about 1,150 group operations, too slow under Miri" +)] +fn a_wrong_digest_is_rejected() -> TestResult { + let v = first(VALID)?; + let (key, digest, r, s) = decode(v)?; + let mut d2 = digest.clone(); + flip(&mut d2, 0)?; + expect( + "first bit of the digest flipped", + verify(&d2, &r, &s, &key), + false, + )?; + let mut d3 = digest.clone(); + flip(&mut d3, 47)?; + expect( + "last bit of the digest flipped", + verify(&d3, &r, &s, &key), + false, + )?; + // A digest cut short is another digest. + let short = digest.get(..47).ok_or("short")?; + expect("one octet short", verify(short, &r, &s, &key), false)?; + // One with an octet put in front is another digest too. + let mut front = vec![0u8]; + front.extend_from_slice(&digest); + expect("one octet in front", verify(&front, &r, &s, &key), false)?; + expect("empty digest", verify(&[], &r, &s, &key), false)?; + Ok(()) +} + +/// FIPS 186-5 §6.4.2 step 3: only the leftmost 384 bits of a longer digest +/// are used, so octets after the 48th change nothing (SHA-512's 64 octets are +/// cut to 48). +#[test] +#[cfg_attr( + miri, + ignore = "a verification is about 1,150 group operations, too slow under Miri" +)] +fn a_longer_digest_is_cut_to_its_leftmost_384_bits() -> TestResult { + let v = first(VALID)?; + let (key, digest, r, s) = decode(v)?; + let mut long = digest.clone(); + long.extend_from_slice(&[0xa5; 16]); + expect( + "64 octets, first 48 as signed", + verify(&long, &r, &s, &key), + true, + )?; + let mut changed = long.clone(); + flip(&mut changed, 47)?; + expect( + "64 octets, 48th octet changed", + verify(&changed, &r, &s, &key), + false, + )?; + Ok(()) +} + +#[test] +fn r_and_s_outside_one_to_n_minus_one_are_rejected() -> TestResult { + let v = first(VALID)?; + let (key, digest, r, s) = decode(v)?; + let zero = [0u8; 48]; + let n = arr48(N)?; + let ff = [0xffu8; 48]; + let mut n_plus_1 = n; + // n ends in ...2973, so n + 1 does not carry. + let last = n_plus_1.last_mut().ok_or("n")?; + *last = last.wrapping_add(1); + for (name, bad) in [ + ("0", zero), + ("n", n), + ("n + 1", n_plus_1), + ("2^384 - 1", ff), + ] { + expect( + &format!("r = {name}"), + verify(&digest, &bad, &s, &key), + false, + )?; + expect( + &format!("s = {name}"), + verify(&digest, &r, &bad, &key), + false, + )?; + expect( + &format!("r = s = {name}"), + verify(&digest, &bad, &bad, &key), + false, + )?; + } + Ok(()) +} + +#[test] +fn keys_that_do_not_decode_are_rejected() -> TestResult { + let v = first(VALID)?; + let (key, digest, r, s) = decode(v)?; + // Off the curve: y changed by one bit. + let mut off = key.clone(); + let last = off.last_mut().ok_or("key")?; + *last ^= 1; + expect("off the curve", verify(&digest, &r, &s, &off), false)?; + // Compressed form (`02`/`03` || X), which the specification refuses. + let x = key.get(1..49).ok_or("x")?; + for tag in [2u8, 3] { + let mut c = vec![tag]; + c.extend_from_slice(x); + expect( + &format!("compressed {tag:02x}"), + verify(&digest, &r, &s, &c), + false, + )?; + } + // Hybrid forms (`06`/`07`), a first octet other than `04`, and the point + // at infinity. + for tag in [0u8, 1, 5, 6, 7, 0xff] { + let mut h = key.clone(); + let first = h.first_mut().ok_or("key")?; + *first = tag; + expect( + &format!("first octet {tag:02x}"), + verify(&digest, &r, &s, &h), + false, + )?; + } + expect("point at infinity", verify(&digest, &r, &s, &[0]), false)?; + // Wrong lengths. + expect("empty key", verify(&digest, &r, &s, &[]), false)?; + expect( + "one octet short", + verify(&digest, &r, &s, key.get(..96).ok_or("k")?), + false, + )?; + let mut long = key.clone(); + long.push(0); + expect("one octet more", verify(&digest, &r, &s, &long), false)?; + // A coordinate that is at least p (X = p, then Y = p). + let p = unhex(P)?; + let mut big_x = vec![4u8]; + big_x.extend_from_slice(&p); + big_x.extend_from_slice(key.get(49..).ok_or("y")?); + expect("X = p", verify(&digest, &r, &s, &big_x), false)?; + let mut big_y = key.get(..49).ok_or("x")?.to_vec(); + big_y.extend_from_slice(&p); + expect("Y = p", verify(&digest, &r, &s, &big_y), false)?; + Ok(()) +} + +#[test] +#[cfg_attr( + miri, + ignore = "a verification is about 1,150 group operations, too slow under Miri" +)] +fn a_signature_does_not_verify_under_another_key() -> TestResult { + let v = first(VALID)?; + let (_, digest, r, s) = decode(v)?; + let other = vector(VALID, 5)?; + let (other_key, _, _, _) = decode(other)?; + expect("another key", verify(&digest, &r, &s, &other_key), false) +} + +/// Not an assertion about speed: it prints how long one verification takes +/// (`cargo test -p clazel-p384 --test verify timing -- --nocapture`). +#[test] +#[cfg_attr( + miri, + ignore = "a verification is about 1,150 group operations, too slow under Miri" +)] +fn timing() -> TestResult { + let v = first(VALID)?; + let (key, digest, r, s) = decode(v)?; + let start = Instant::now(); + let runs = 3; + for _ in 0..runs { + expect("tcId 1", verify(&digest, &r, &s, &key), true)?; + } + eprintln!( + "verify: {:?} per verification (mean of {runs})", + start.elapsed() / runs + ); + Ok(()) +}