diff --git a/Cargo.lock b/Cargo.lock index e865e5b..9a3aea1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -277,6 +277,13 @@ dependencies = [ "vstd", ] +[[package]] +name = "clazel-p384" +version = "0.0.0" +dependencies = [ + "vstd", +] + [[package]] name = "clazel-percent" version = "0.0.0" diff --git a/crates/clazel-p384/Cargo.toml b/crates/clazel-p384/Cargo.toml new file mode 100644 index 0000000..50a5059 --- /dev/null +++ b/crates/clazel-p384/Cargo.toml @@ -0,0 +1,23 @@ +[package] +name = "clazel-p384" +version = "0.0.0" +edition.workspace = true +license.workspace = true +publish.workspace = true +description = "ECDSA signature verification over NIST P-384 (FIPS 186-5 §6.4.2), specified in Verus." + +[dependencies] +vstd = "=0.0.0-2026-10-04-0306" + +# Verification tier (docs/VERIFICATION.md). `tier` is what is proven about +# the shipped code today; `target-tier` is what the policy requires. This +# crate is specification only so far: nothing is implemented, so tier 0. +[package.metadata.clazel] +tier = 0 +target-tier = 2 + +[package.metadata.verus] +verify = true + +[lints] +workspace = true diff --git a/crates/clazel-p384/README.md b/crates/clazel-p384/README.md new file mode 100644 index 0000000..8f2f9b7 --- /dev/null +++ b/crates/clazel-p384/README.md @@ -0,0 +1,87 @@ +# clazel-p384 + +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 only + +**Tier 0, target tier 2.** Nothing is implemented. This crate has no +executable code: no field arithmetic, no point arithmetic and no `verify` +function. What exists is the part a person reviews: + +- `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 + from SP 800-186 (Appendices D.1.1.1 and F.1, and B.1 of FIPS 186-5) and + SEC 1 v2 (§2.2.1 the group law, §2.3 conversions, §3.2.2.1, §4.1.4). The + 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/examples.rs`: known answers, proven by evaluating the spec + (`by (compute_only)`), on a toy curve and on P-384. + +Nothing here claims verification of any code. 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 it is, and what it is not + +**Public-key verification only.** The key, the signature and the digest are +public, so nothing here has a constant-time requirement, and none is claimed. +No signing, no private key. + +**The input is the digest**, 0 to 64 octets, not the message. Hashing is done +by `clazel-crypto`, so this crate has **no axiom**. The key is the full +97-octet ECPoint `04 || X || Y`; decoding and validation are inside the +verified code (uncompressed form only; the compressed form is refused). + +## The spec's shape + +- `ecdsa_verify_steps` returns `Ok(())` or `Err(step)`, the numbered step + that rejected, so that a deliberate bug in one check can be told from a bug + elsewhere. `ecdsa_verify` is "accept". +- The group law is SEC 1 §2.2.1's affine rules in its order, with the point + at infinity a distinct value. `[k]P` is MSB-first double-and-add. Division + is Fermat with a checked result (`inv`); FIPS 186-5 Appendix B.1 is + transcribed too (`b1_inverse`) and the examples evaluate both. +- **Cited, not proven:** associativity of the group law (so that double-and-add + is the k-fold sum) and Fermat's little theorem for P-384's p and n (so that + the `None` branch of `inv` is unreachable). The primality of p and n is + SP 800-186's statement. +- The public key is always validated (SP 800-186 D.1.1.1). The `nQ = O` check + is omitted because the cofactor is 1 (SEC 1 §3.2.2.1 says why that is + sound). +- `toy()` is a 7-bit curve (p = 83, n = 67, h = 1, a = -3) used only for + evaluated examples. No standard defines it and no executable code can reach + it. + +## What is evaluated + +Known answers on the toy curve: a valid signature (with `x_R >= n`, so step +9's reduction matters, and a digest cut at a bit that is not an octet +boundary), rejections at steps 1, 6 and 9, and an invalid key (off the +curve, compressed, hybrid, a coordinate at least p, the point at infinity, +wrong lengths). On P-384: the constants' consequences (G is on the curve), +`2G` and `3G`, key decoding, and whole verifications whose scalars are small +by construction. A verification with full-size scalars (about 1,150 group +operations) is **not** evaluated: the interpreter of `by (compute_only)` +times out on it. + +## Verification + +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`) and that the evaluated examples hold. `mutations.json` holds 26 +mutations of `spec.rs`, each killed with a certificate that contradicts one +of those examples. There is no lemma about the spec, no independent +transcription, no conformance test and no Kani harness yet, so the crate +stays at tier 0; see +[docs/VERIFICATION.md](../../docs/VERIFICATION.md) for what each tier +requires. + +## Licence + +MIT, as in the repository's [LICENSE](../../LICENSE). diff --git a/crates/clazel-p384/mutations.json b/crates/clazel-p384/mutations.json new file mode 100644 index 0000000..9e371a0 --- /dev/null +++ b/crates/clazel-p384/mutations.json @@ -0,0 +1,342 @@ +{ + "mutations": [ + { + "id": "step1-r-upper", + "file": "src/spec.rs", + "find": "r <= c.n - 1 && 1 <= s", + "replace": "r <= c.n && 1 <= s", + "expect": "killed", + "reason": "Step 1 bounds r by n - 1; r = n would pass.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_verify_examples()", + "witness": "!crate::examples::ex_rejects(toy(), seq![0xB5u8, 0x12u8], 67nat, 5nat, crate::examples::toy_q(), Step::S1)" + } + }, + { + "id": "step1-r-lower", + "file": "src/spec.rs", + "find": "if !(1 <= r && r <= c.n - 1", + "replace": "if !(0 <= r && r <= c.n - 1", + "expect": "killed", + "reason": "Step 1 refuses r = 0.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_verify_examples()", + "witness": "!crate::examples::ex_rejects(toy(), seq![0xB5u8, 0x12u8], 0nat, 5nat, crate::examples::toy_q(), Step::S1)" + } + }, + { + "id": "step1-s-upper", + "file": "src/spec.rs", + "find": "&& s <= c.n - 1)", + "replace": "&& s <= c.n)", + "expect": "killed", + "reason": "Step 1 bounds s by n - 1.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_verify_examples()", + "witness": "!crate::examples::ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 67nat, crate::examples::toy_q(), Step::S1)" + } + }, + { + "id": "step9-no-reduction", + "file": "src/spec.rs", + "find": "if r == r1 % c.n {", + "replace": "if r == r1 {", + "expect": "killed", + "reason": "Step 9 compares r with r1 mod n; the toy signature has x_R = 81 > n.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_verify_examples()", + "witness": "!ecdsa_verify(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, crate::examples::toy_q())" + } + }, + { + "id": "step5-u-uses-r", + "file": "src/spec.rs", + "find": "let u = e * w % c.n;", + "replace": "let u = r * w % c.n;", + "expect": "killed", + "reason": "Step 5: u = e·s⁻¹; with r the digest is ignored.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_verify_examples()", + "witness": "!ecdsa_verify(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, crate::examples::toy_q())" + } + }, + { + "id": "step5-v-uses-e", + "file": "src/spec.rs", + "find": "let v = r * w % c.n;", + "replace": "let v = e * w % c.n;", + "expect": "killed", + "reason": "Step 5: v = r·s⁻¹.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_verify_examples()", + "witness": "!ecdsa_verify(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, crate::examples::toy_q())" + } + }, + { + "id": "step6-infinity-accepted", + "file": "src/spec.rs", + "find": "Some(Point::Infinity) => Err(Step::S6),", + "replace": "Some(Point::Infinity) => Ok(()),", + "expect": "killed", + "reason": "Step 6 rejects R1 = O.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_verify_examples()", + "witness": "!crate::examples::ex_rejects(toy(), seq![0x02u8], 32nat, 5nat, crate::examples::toy_q(), Step::S6)" + } + }, + { + "id": "step3-truncation", + "file": "src/spec.rs", + "find": "hbits.take(ceil_log2(c.n) as int)", + "replace": "hbits.take((ceil_log2(c.n) - 1) as int)", + "expect": "killed", + "reason": "Step 3a keeps the leftmost ⌈log2 n⌉ bits, 7 for the toy curve; 6 halves e.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_derive_e_examples()", + "witness": "derive_e(toy(), seq![0xB5u8]) == 45nat" + } + }, + { + "id": "ceil-log2-halving", + "file": "src/spec.rs", + "find": "1 + ceil_log2((n + 1) / 2)", + "replace": "1 + ceil_log2(n / 2)", + "expect": "killed", + "reason": "Rounds down: ⌈log2 5⌉ would be 2.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_conversion_examples()", + "witness": "ceil_log2(5nat) == 2nat" + } + }, + { + "id": "bits-to-int-base", + "file": "src/spec.rs", + "find": "bits_to_int(b.drop_last()) * 2 +", + "replace": "bits_to_int(b.drop_last()) * 3 +", + "expect": "killed", + "reason": "B.2.1 is base 2.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_conversion_examples()", + "witness": "bits_to_int(seq![true, false, true]) == 10nat" + } + }, + { + "id": "octet-bit-order", + "file": "src/spec.rs", + "find": "two_to((7 - i % 8) as nat)", + "replace": "two_to((i % 8) as nat)", + "expect": "killed", + "reason": "SEC 1 §2.3.2 writes each octet most significant bit first.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_conversion_examples()", + "witness": "octets_to_bits(seq![0xB5u8]) == seq![true, false, true, false, true, true, false, true]" + } + }, + { + "id": "os2ip-base", + "file": "src/spec.rs", + "find": "os2ip(m.drop_last()) * 256 + m.last() as nat", + "replace": "os2ip(m.drop_last()) * 255 + m.last() as nat", + "expect": "killed", + "reason": "SEC 1 §2.3.8 is base 256.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_conversion_examples()", + "witness": "os2ip(seq![1u8, 2u8]) == 257nat" + } + }, + { + "id": "os2fe-range", + "file": "src/spec.rs", + "find": "if a < c.p {", + "replace": "if true {", + "expect": "killed", + "reason": "SEC 1 §2.3.6 refuses a coordinate of p or more; 127 = 44 + 83 would alias x = 44.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_decode_examples()", + "witness": "os2p(toy(), seq![0x04u8, 127u8, 39u8]) is Some" + } + }, + { + "id": "os2p-hybrid", + "file": "src/spec.rs", + "find": "if w != 0x04 {", + "replace": "if w != 0x04 && w != 0x06 {", + "expect": "killed", + "reason": "SEC 1 §2.3.4 step 3.2 accepts only W = 04.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_decode_examples()", + "witness": "os2p(toy(), seq![0x06u8, 44u8, 39u8]) is Some" + } + }, + { + "id": "os2p-on-curve", + "file": "src/spec.rs", + "find": "if satisfies_equation(c, x, y) {", + "replace": "if true {", + "expect": "killed", + "reason": "SEC 1 §2.3.4 step 3.5 checks the curve equation; (0, 0) is not on the toy curve.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_decode_examples()", + "witness": "os2p(toy(), seq![0x04u8, 0u8, 0u8]) is Some" + } + }, + { + "id": "key-infinity", + "file": "src/spec.rs", + "find": "Point::Infinity => false,", + "replace": "Point::Infinity => true,", + "expect": "killed", + "reason": "SP 800-186 D.1.1.1 step 1 rejects the point at infinity.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_decode_examples()", + "witness": "decode_public_key(toy(), seq![0x00u8]) is Some" + } + }, + { + "id": "double-uses-b", + "file": "src/spec.rs", + "find": "(3 * x1 * x1 + c.a)", + "replace": "(3 * x1 * x1 + c.b)", + "expect": "killed", + "reason": "SEC 1 rule 5: λ = (3x² + a)/(2y).", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_group_examples()", + "witness": "!(ec_add(toy(), crate::examples::toy_g(), crate::examples::toy_g()) == Some(Point::Affine { x: 81nat, y: 52nat }))" + } + }, + { + "id": "add-slope-sign", + "file": "src/spec.rs", + "find": "let lambda = fe_sub(c.p, y2, y1) * w % c.p;", + "replace": "let lambda = fe_sub(c.p, y1, y2) * w % c.p;", + "expect": "killed", + "reason": "SEC 1 rule 4: λ = (y2 - y1)/(x2 - x1).", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_group_examples()", + "witness": "!(ec_add(toy(), Point::Affine { x: 81nat, y: 52nat }, crate::examples::toy_g()) == Some(Point::Affine { x: 50nat, y: 63nat }))" + } + }, + { + "id": "add-x3", + "file": "src/spec.rs", + "find": "let x3 = fe_sub(c.p, fe_sub(c.p, lambda * lambda % c.p, x1), x2);", + "replace": "let x3 = fe_sub(c.p, fe_sub(c.p, lambda * lambda % c.p, x1), x1);", + "expect": "killed", + "reason": "SEC 1 rule 4: x3 = λ² - x1 - x2.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_group_examples()", + "witness": "!(ec_add(toy(), Point::Affine { x: 81nat, y: 52nat }, crate::examples::toy_g()) == Some(Point::Affine { x: 50nat, y: 63nat }))" + } + }, + { + "id": "negation-rule", + "file": "src/spec.rs", + "find": "if x1 == x2 && (y1 + y2) % c.p == 0 {", + "replace": "if x1 == x2 && (y1 + y2) % c.p == 1 {", + "expect": "killed", + "reason": "SEC 1 rule 3: (x, y) + (x, -y) = O.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_group_examples()", + "witness": "!(ec_add(toy(), crate::examples::toy_g(), Point::Affine { x: 1nat, y: 52nat }) == Some(Point::Infinity))" + } + }, + { + "id": "scalar-odd-bit", + "file": "src/spec.rs", + "find": "Some(twice) => if k % 2 == 1 {", + "replace": "Some(twice) => if k % 2 == 0 {", + "expect": "killed", + "reason": "Double-and-add adds P on a one bit.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_toy_group_examples()", + "witness": "!(scalar_mul(toy(), 2nat, crate::examples::toy_g()) == Some(Point::Affine { x: 81nat, y: 52nat }))" + } + }, + { + "id": "inv-unchecked", + "file": "src/spec.rs", + "find": "if (a % m) * w % m == 1 {", + "replace": "if true {", + "expect": "killed", + "reason": "The inverse is accepted only when it is checked to be one; 0 has none.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_inverse_examples()", + "witness": "inv(83nat, 0nat) is Some" + } + }, + { + "id": "b1-step5-sign", + "file": "src/spec.rs", + "find": "let y = y2 - y1 * quotient;", + "replace": "let y = y2 + y1 * quotient;", + "expect": "killed", + "reason": "FIPS 186-5 B.1 step 5: y = y2 - y1·quotient; with + the inverse of 2 mod 83 comes out 41, not 42.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_inverse_examples()", + "witness": "b1_inverse(2nat, 83nat) == Some(41nat)" + } + }, + { + "id": "p384-gx", + "file": "src/spec.rs", + "find": "gx: 0xaa87ca22_", + "replace": "gx: 0xaa87ca23_", + "expect": "killed", + "reason": "SP 800-186 §3.2.1.4's Gx; changed, G is off the curve.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_p384_group_examples()", + "witness": "!satisfies_equation(p384(), p384().gx, p384().gy)" + } + }, + { + "id": "p384-b", + "file": "src/spec.rs", + "find": "b: 0xb3312fa7_", + "replace": "b: 0xb3312fa6_", + "expect": "killed", + "reason": "SP 800-186 §3.2.1.4's b; changed, G is off the curve.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_p384_group_examples()", + "witness": "!satisfies_equation(p384(), p384().gx, p384().gy)" + } + }, + { + "id": "p384-n", + "file": "src/spec.rs", + "find": "ffffffff_c7634d81_f4372ddf", + "replace": "ffffffff_c7634d82_f4372ddf", + "expect": "killed", + "reason": "SP 800-186 §3.2.1.4's n; the changed value is composite, so 2 has no Fermat inverse.", + "certificate": { + "file": "src/certificates.rs", + "lemma": "crate::examples::lemma_inverse_examples()", + "witness": "inv(p384().n, 2nat) is None" + } + } + ] +} diff --git a/crates/clazel-p384/src/certificates.rs b/crates/clazel-p384/src/certificates.rs new file mode 100644 index 0000000..98aafd5 --- /dev/null +++ b/crates/clazel-p384/src/certificates.rs @@ -0,0 +1,14 @@ +//! The module that hosts the kill certificates of `mutations.json` +//! (xtask/src/mutate.rs adds one proof function here per certified +//! mutation, at run time, to a copy of the crate). The module is +//! empty on purpose: +//! a certificate is run alone in this module, and the evaluated examples in +//! [`super::examples`] (which a mutated spec makes fail) must not be in the +//! module being verified. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! {} // verus! diff --git a/crates/clazel-p384/src/contract.rs b/crates/clazel-p384/src/contract.rs new file mode 100644 index 0000000..feebf56 --- /dev/null +++ b/crates/clazel-p384/src/contract.rs @@ -0,0 +1,42 @@ +//! 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`). +//! +//! ```text +//! pub fn verify(digest: &[u8], r: &[u8; 48], s: &[u8; 48], point: &[u8]) -> (ok: 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! { + +/// What the caller owes `verify`: a digest of 0 to 64 octets (so SHA-256, +/// SHA-384 and SHA-512 are all accepted; modelling choice 1 of the spec). +/// `r` and `s` are `[u8; 48]` arrays, so their length is in the type, and +/// `point` may be any octet string: decoding is inside the verifier. +pub open spec fn verify_requires(digest: Seq) -> bool { + digest.len() <= 64 +} + +/// `verify(digest, r, s, point)`: ECDSA verification over P-384 (FIPS 186-5 +/// §6.4.2). `r` and `s` are the big-endian octets of the signature integers, +/// and `point` is the 97-octet ECPoint `04 || X || Y` of the public key (any +/// other string is rejected by the spec's decoding). +pub open spec fn verify_ensures( + digest: Seq, + r: Seq, + s: Seq, + point: Seq, + ok: bool, +) -> bool { + ok == ecdsa_verify(p384(), digest, os2ip(r), os2ip(s), point) +} + +} // verus! diff --git a/crates/clazel-p384/src/examples.rs b/crates/clazel-p384/src/examples.rs new file mode 100644 index 0000000..b88a4a8 --- /dev/null +++ b/crates/clazel-p384/src/examples.rs @@ -0,0 +1,614 @@ +//! Known answers, evaluated: small cases of the spec's functions whose +//! results were worked out independently of the spec (with a script that +//! re-implements the same rules in Python, see the commit notes) and are +//! proven here by evaluating the spec (`by (compute_only)`). They are facts +//! about the spec itself, evidence that the transcription computes what the +//! standards define, and the theorems the mutation certificates in +//! `mutations.json` will contradict. +//! +//! Most of them are on [`toy`], a 7-bit curve small enough for a whole +//! verification to be evaluated. On [`p384`] only what the evaluator can do +//! in reasonable time is here: the constants' consequences, a point +//! doubling, public key decoding, and verifications whose scalars `u` and +//! `v` are small, chosen first (a signature is built backwards from `u`, `v` +//! and a key, so that step 6 needs a handful of group operations and not +//! about 1,150). + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// `x` as `len` big-endian octets (SEC 1 §2.3.7 Integer-to-Octet-String; the +/// caller ensures `x < 256^len`, and the examples check `os2ip` of the +/// result). +pub open spec fn ex_octets(x: nat, len: nat) -> Seq { + Seq::new(len, |i: int| ((x / two_to(8 * (len - 1 - i) as nat)) % 256) as u8) +} + +/// The ECPoint `04 || X || Y` of the affine point (x, y) with `len` octets +/// per coordinate. +pub open spec fn ex_ecpoint(x: nat, y: nat, len: nat) -> Seq { + seq![0x04u8] + ex_octets(x, len) + ex_octets(y, len) +} + +/// The base point of [`toy`], (1, 31). +pub open spec fn toy_g() -> Point { + Point::Affine { x: 1, y: 31 } +} + +/// The toy public key Q = [23]G = (44, 39) as an ECPoint. +pub open spec fn toy_q() -> Seq { + seq![0x04u8, 44u8, 39u8] +} + + +/// Conversions: SEC 1 §2.3.8, §2.3.2, FIPS 186-5 B.2.1, `⌈log2 n⌉`. +pub proof fn lemma_conversion_examples() + ensures + os2ip(seq![1u8, 2u8]) == 258nat, + os2ip(seq![0x12u8, 0x34u8, 0x56u8]) == 0x123456nat, + os2ip(Seq::::empty()) == 0nat, + os2ip(ex_octets(0x0102nat, 2nat)) == 0x0102nat, + octets_to_bits(seq![0xB5u8]) == seq![true, false, true, true, false, true, false, true], + octets_to_bits(Seq::::empty()) == Seq::::empty(), + bits_to_int(seq![true, false, true]) == 5nat, + bits_to_int(Seq::::empty()) == 0nat, + ceil_log2(1nat) == 0nat, + ceil_log2(2nat) == 1nat, + ceil_log2(3nat) == 2nat, + ceil_log2(4nat) == 2nat, + ceil_log2(5nat) == 3nat, + ceil_log2(64nat) == 6nat, + ceil_log2(65nat) == 7nat, + ceil_log2(toy().n) == 7nat, +{ + assert(os2ip(seq![1u8, 2u8]) == 258nat) by (compute_only); + assert(os2ip(seq![0x12u8, 0x34u8, 0x56u8]) == 0x123456nat) by (compute_only); + assert(os2ip(Seq::::empty()) == 0nat) by (compute_only); + assert(os2ip(ex_octets(0x0102nat, 2nat)) == 0x0102nat) by (compute_only); + assert(octets_to_bits(seq![0xB5u8]) == seq![true, false, true, true, false, true, false, true]) + by (compute_only); + assert(octets_to_bits(Seq::::empty()) == Seq::::empty()) by (compute_only); + assert(bits_to_int(seq![true, false, true]) == 5nat) by (compute_only); + assert(bits_to_int(Seq::::empty()) == 0nat) by (compute_only); + assert(ceil_log2(1nat) == 0nat) by (compute_only); + assert(ceil_log2(2nat) == 1nat) by (compute_only); + assert(ceil_log2(3nat) == 2nat) by (compute_only); + assert(ceil_log2(4nat) == 2nat) by (compute_only); + assert(ceil_log2(5nat) == 3nat) by (compute_only); + assert(ceil_log2(64nat) == 6nat) by (compute_only); + assert(ceil_log2(65nat) == 7nat) by (compute_only); + assert(ceil_log2(toy().n) == 7nat) by (compute_only); +} + + +/// Step 3 on [`toy`] (n has 7 bits, so a digest is cut to its leftmost 7 +/// bits, not to whole octets) and on [`p384`] (a 48-octet digest is kept +/// whole, a 64-octet one is cut to its leftmost 384 bits, a shorter one is +/// kept whole). `0xB5 = 1011 0101`, whose leftmost 7 bits `1011010` are 90. +pub proof fn lemma_derive_e_examples() + ensures + derive_e(toy(), seq![0xB5u8]) == 90nat, + derive_e(toy(), seq![0xB4u8]) == 90nat, + derive_e(toy(), seq![0xB5u8, 0x12u8]) == 90nat, + derive_e(toy(), seq![0xB4u8, 0x00u8]) == 90nat, + derive_e(toy(), seq![0xB6u8]) == 91nat, + derive_e(toy(), seq![0x01u8]) == 0nat, + derive_e(toy(), seq![0x02u8]) == 1nat, + derive_e(toy(), seq![0x7Fu8]) == 63nat, + derive_e(toy(), seq![0xFFu8, 0xFFu8]) == 127nat, + derive_e(toy(), Seq::::empty()) == 0nat, + derive_e(p384(), ex_octets(0x0123456789abcdefnat, 48nat)) == 0x0123456789abcdefnat, + derive_e(p384(), ex_octets(0x0123456789abcdefnat, 32nat)) == 0x0123456789abcdefnat, + derive_e(p384(), Seq::::empty()) == 0nat, + derive_e(p384(), ex_octets(two_to(500nat) + 12345nat, 64nat)) == two_to(372nat), + derive_e(p384(), ex_octets(two_to(500nat) + 12345nat, 64nat) + seq![0xFFu8]) + == two_to(372nat), +{ + assert(derive_e(toy(), seq![0xB5u8]) == 90nat) by (compute_only); + assert(derive_e(toy(), seq![0xB4u8]) == 90nat) by (compute_only); + assert(derive_e(toy(), seq![0xB5u8, 0x12u8]) == 90nat) by (compute_only); + assert(derive_e(toy(), seq![0xB4u8, 0x00u8]) == 90nat) by (compute_only); + assert(derive_e(toy(), seq![0xB6u8]) == 91nat) by (compute_only); + assert(derive_e(toy(), seq![0x01u8]) == 0nat) by (compute_only); + assert(derive_e(toy(), seq![0x02u8]) == 1nat) by (compute_only); + assert(derive_e(toy(), seq![0x7Fu8]) == 63nat) by (compute_only); + assert(derive_e(toy(), seq![0xFFu8, 0xFFu8]) == 127nat) by (compute_only); + assert(derive_e(toy(), Seq::::empty()) == 0nat) by (compute_only); + assert(derive_e(p384(), ex_octets(0x0123456789abcdefnat, 48nat)) == 0x0123456789abcdefnat) + by (compute_only); + assert(derive_e(p384(), ex_octets(0x0123456789abcdefnat, 32nat)) == 0x0123456789abcdefnat) + by (compute_only); + assert(derive_e(p384(), Seq::::empty()) == 0nat) by (compute_only); + assert(derive_e(p384(), ex_octets(two_to(500nat) + 12345nat, 64nat)) == two_to(372nat)) + by (compute_only); + assert(derive_e(p384(), ex_octets(two_to(500nat) + 12345nat, 64nat) + seq![0xFFu8]) + == two_to(372nat)) by (compute_only); +} + +/// The inverse (modelling choice 3): [`inv`] and the reference routine +/// [`b1_inverse`] (FIPS 186-5 B.1) agree, and both refuse 0 and the modulus. +/// `5 · 27 = 135 = 2 · 67 + 1`, `2 · 42 = 84 = 83 + 1`. +pub proof fn lemma_inverse_examples() + ensures + inv(67nat, 5nat) == Some(27nat), + b1_inverse(5nat, 67nat) == Some(27nat), + inv(83nat, 2nat) == Some(42nat), + b1_inverse(2nat, 83nat) == Some(42nat), + inv(83nat, 1nat) == Some(1nat), + b1_inverse(1nat, 83nat) == Some(1nat), + inv(83nat, 82nat) == Some(82nat), + b1_inverse(82nat, 83nat) == Some(82nat), + inv(83nat, 0nat) is None, + inv(83nat, 83nat) is None, + b1_inverse(0nat, 83nat) is None, + b1_inverse(83nat, 83nat) is None, + b1_inverse(1nat, 1nat) is None, + // A composite modulus: 6 has no inverse mod 9, and neither routine + // finds one (Fermat's check fails; B.1 step 8). + b1_inverse(6nat, 9nat) is None, + inv(9nat, 6nat) is None, + inv(p384().p, 2nat) == Some((p384().p + 1) / 2), + b1_inverse(2nat, p384().p) == Some((p384().p + 1) / 2), + inv(p384().n, 2nat) == Some((p384().n + 1) / 2), + b1_inverse(2nat, p384().n) == Some((p384().n + 1) / 2), +{ + assert(inv(67nat, 5nat) == Some(27nat)) by (compute_only); + assert(b1_inverse(5nat, 67nat) == Some(27nat)) by (compute_only); + assert(inv(83nat, 2nat) == Some(42nat)) by (compute_only); + assert(b1_inverse(2nat, 83nat) == Some(42nat)) by (compute_only); + assert(inv(83nat, 1nat) == Some(1nat)) by (compute_only); + assert(b1_inverse(1nat, 83nat) == Some(1nat)) by (compute_only); + assert(inv(83nat, 82nat) == Some(82nat)) by (compute_only); + assert(b1_inverse(82nat, 83nat) == Some(82nat)) by (compute_only); + assert(inv(83nat, 0nat) is None) by (compute_only); + assert(inv(83nat, 83nat) is None) by (compute_only); + assert(b1_inverse(0nat, 83nat) is None) by (compute_only); + assert(b1_inverse(83nat, 83nat) is None) by (compute_only); + assert(b1_inverse(1nat, 1nat) is None) by (compute_only); + assert(b1_inverse(6nat, 9nat) is None) by (compute_only); + assert(inv(9nat, 6nat) is None) by (compute_only); + assert(inv(p384().p, 2nat) == Some((p384().p + 1) / 2)) by (compute_only); + assert(b1_inverse(2nat, p384().p) == Some((p384().p + 1) / 2)) by (compute_only); + assert(inv(p384().n, 2nat) == Some((p384().n + 1) / 2)) by (compute_only); + assert(b1_inverse(2nat, p384().n) == Some((p384().n + 1) / 2)) by (compute_only); +} + + +/// The group law and scalar multiplication on [`toy`], and the facts a +/// reader can check by hand: `2G`, `3G` from rules 5 and 4, `G + (-G) = O` +/// (rule 3), the identity rules (1 and 2), `[0]G = O`, `[66]G = -G` and +/// `[67]G = O` (so G has order n), and `[23]G = Q`. The multiples were +/// computed with an independent script. +pub proof fn lemma_toy_group_examples() + ensures + ({ + &&& base_point(toy()) == toy_g() + // 5. doubling. + &&& ec_add(toy(), toy_g(), toy_g()) == Some(Point::Affine { x: 81nat, y: 52nat }) + // 4. different x-coordinates. + &&& ec_add(toy(), Point::Affine { x: 81nat, y: 52nat }, toy_g()) + == Some(Point::Affine { x: 50nat, y: 63nat }) + &&& ec_add(toy(), toy_g(), Point::Affine { x: 81nat, y: 52nat }) + == Some(Point::Affine { x: 50nat, y: 63nat }) + // 3. P + (-P) = O. + &&& ec_add(toy(), toy_g(), Point::Affine { x: 1nat, y: 52nat }) == Some(Point::Infinity) + &&& ec_add(toy(), Point::Affine { x: 1nat, y: 52nat }, toy_g()) == Some(Point::Infinity) + // 1. and 2. + &&& ec_add(toy(), Point::Infinity, Point::Infinity) == Some(Point::Infinity) + &&& ec_add(toy(), Point::Infinity, toy_g()) == Some(toy_g()) + &&& ec_add(toy(), toy_g(), Point::Infinity) == Some(toy_g()) + // [k]G. + &&& scalar_mul(toy(), 0nat, toy_g()) == Some(Point::Infinity) + &&& scalar_mul(toy(), 1nat, toy_g()) == Some(toy_g()) + &&& scalar_mul(toy(), 2nat, toy_g()) == Some(Point::Affine { x: 81nat, y: 52nat }) + &&& scalar_mul(toy(), 3nat, toy_g()) == Some(Point::Affine { x: 50nat, y: 63nat }) + &&& scalar_mul(toy(), 4nat, toy_g()) == Some(Point::Affine { x: 55nat, y: 54nat }) + &&& scalar_mul(toy(), 5nat, toy_g()) == Some(Point::Affine { x: 60nat, y: 53nat }) + &&& scalar_mul(toy(), 23nat, toy_g()) == Some(Point::Affine { x: 44nat, y: 39nat }) + &&& scalar_mul(toy(), 66nat, toy_g()) == Some(Point::Affine { x: 1nat, y: 52nat }) + &&& scalar_mul(toy(), 67nat, toy_g()) == Some(Point::Infinity) + &&& scalar_mul(toy(), 68nat, toy_g()) == Some(toy_g()) + &&& scalar_mul(toy(), 5nat, Point::Infinity) == Some(Point::Infinity) + }), +{ + assert(base_point(toy()) == toy_g()) by (compute_only); + assert(ec_add(toy(), toy_g(), toy_g()) == Some(Point::Affine { x: 81nat, y: 52nat })) by (compute_only); + assert(ec_add(toy(), Point::Affine { x: 81nat, y: 52nat }, toy_g()) + == Some(Point::Affine { x: 50nat, y: 63nat })) by (compute_only); + assert(ec_add(toy(), toy_g(), Point::Affine { x: 81nat, y: 52nat }) + == Some(Point::Affine { x: 50nat, y: 63nat })) by (compute_only); + assert(ec_add(toy(), toy_g(), Point::Affine { x: 1nat, y: 52nat }) == Some(Point::Infinity)) by (compute_only); + assert(ec_add(toy(), Point::Affine { x: 1nat, y: 52nat }, toy_g()) == Some(Point::Infinity)) by (compute_only); + assert(ec_add(toy(), Point::Infinity, Point::Infinity) == Some(Point::Infinity)) by (compute_only); + assert(ec_add(toy(), Point::Infinity, toy_g()) == Some(toy_g())) by (compute_only); + assert(ec_add(toy(), toy_g(), Point::Infinity) == Some(toy_g())) by (compute_only); + assert(scalar_mul(toy(), 0nat, toy_g()) == Some(Point::Infinity)) by (compute_only); + assert(scalar_mul(toy(), 1nat, toy_g()) == Some(toy_g())) by (compute_only); + assert(scalar_mul(toy(), 2nat, toy_g()) == Some(Point::Affine { x: 81nat, y: 52nat })) + by (compute_only); + assert(scalar_mul(toy(), 3nat, toy_g()) == Some(Point::Affine { x: 50nat, y: 63nat })) + by (compute_only); + assert(scalar_mul(toy(), 4nat, toy_g()) == Some(Point::Affine { x: 55nat, y: 54nat })) + by (compute_only); + assert(scalar_mul(toy(), 5nat, toy_g()) == Some(Point::Affine { x: 60nat, y: 53nat })) + by (compute_only); + assert(scalar_mul(toy(), 23nat, toy_g()) == Some(Point::Affine { x: 44nat, y: 39nat })) + by (compute_only); + assert(scalar_mul(toy(), 66nat, toy_g()) == Some(Point::Affine { x: 1nat, y: 52nat })) + by (compute_only); + assert(scalar_mul(toy(), 67nat, toy_g()) == Some(Point::Infinity)) by (compute_only); + assert(scalar_mul(toy(), 68nat, toy_g()) == Some(toy_g())) by (compute_only); + assert(scalar_mul(toy(), 5nat, Point::Infinity) == Some(Point::Infinity)) by (compute_only); +} + +/// The group law on [`p384`]: G satisfies the curve equation and is a valid +/// public key, and `2G` and `3G` (computed with an independent script, also +/// checked there against `[n]G = O`). +pub proof fn lemma_p384_group_examples() + ensures + satisfies_equation(p384(), p384().gx, p384().gy), + public_key_valid(p384(), base_point(p384())), + ec_add(p384(), base_point(p384()), base_point(p384())) == Some( + Point::Affine { + x: 0x8d999057ba3d2d969260045c55b97f089025959a6f434d651d207d19fb96e9e4fe0e86ebe0e64f85b96a9c75295df61nat, + y: 0x8e80f1fa5b1b3cedb7bfe8dffd6dba74b275d875bc6cc43e904e505f256ab4255ffd43e94d39e22d61501e700a940e80nat, + }, + ), + scalar_mul(p384(), 3nat, base_point(p384())) == Some( + Point::Affine { + x: 0x077a41d4606ffa1464793c7e5fdc7d98cb9d3910202dcd06bea4f240d3566da6b408bbae5026580d02d7e5c70500c831nat, + y: 0xc995f7ca0b0c42837d0bbe9602a9fc998520b41c85115aa5f7684c0edc111eacc24abd6be4b5d298b65f28600a2f1df1nat, + }, + ), +{ + assert(satisfies_equation(p384(), p384().gx, p384().gy)) by (compute_only); + assert(public_key_valid(p384(), base_point(p384()))) by (compute_only); + assert(ec_add(p384(), base_point(p384()), base_point(p384())) == Some( + Point::Affine { + x: 0x8d999057ba3d2d969260045c55b97f089025959a6f434d651d207d19fb96e9e4fe0e86ebe0e64f85b96a9c75295df61nat, + y: 0x8e80f1fa5b1b3cedb7bfe8dffd6dba74b275d875bc6cc43e904e505f256ab4255ffd43e94d39e22d61501e700a940e80nat, + }, + )) by (compute_only); + assert(scalar_mul(p384(), 3nat, base_point(p384())) == Some( + Point::Affine { + x: 0x077a41d4606ffa1464793c7e5fdc7d98cb9d3910202dcd06bea4f240d3566da6b408bbae5026580d02d7e5c70500c831nat, + y: 0xc995f7ca0b0c42837d0bbe9602a9fc998520b41c85115aa5f7684c0edc111eacc24abd6be4b5d298b65f28600a2f1df1nat, + }, + )) by (compute_only); +} + + +/// Public key decoding on [`toy`] (SEC 1 §2.3.4, §2.3.6; SP 800-186 D.1.1.1). +/// `Q = (44, 39)` decodes. Refused: the point at infinity (`00`, decoded by +/// §2.3.4 step 1 and refused by D.1.1.1 step 1), compressed points +/// (`02`, `03`, modelling choice 7), hybrid `06` (§2.3.4 step 3.2), a +/// coordinate not below p (`127 = 44 + 83` and `122 = 39 + 83` satisfy the +/// equation mod p, but §2.3.6 requires [0, p-1]), a point off the curve, and +/// strings of the wrong length. +pub proof fn lemma_toy_decode_examples() + ensures + decode_public_key(toy(), toy_q()) == Some(Point::Affine { x: 44nat, y: 39nat }), + decode_public_key(toy(), seq![0x04u8, 1u8, 31u8]) == Some(toy_g()), + // -Q = (44, 44) is a valid key too. + decode_public_key(toy(), seq![0x04u8, 44u8, 44u8]) == Some(Point::Affine { x: 44nat, y: 44nat }), + // (0, 0) is in range but not on the curve (0 != 50). + os2p(toy(), seq![0x04u8, 0u8, 0u8]) is None, + os2p(toy(), seq![0x00u8]) == Some(Point::Infinity), + decode_public_key(toy(), seq![0x00u8]) is None, + os2p(toy(), seq![0x02u8, 44u8]) is None, + os2p(toy(), seq![0x03u8, 44u8]) is None, + os2p(toy(), seq![0x06u8, 44u8, 39u8]) is None, + os2p(toy(), seq![0x07u8, 44u8, 39u8]) is None, + os2p(toy(), seq![0x05u8, 44u8, 39u8]) is None, + os2p(toy(), seq![0x04u8, 127u8, 39u8]) is None, + os2p(toy(), seq![0x04u8, 44u8, 122u8]) is None, + os2p(toy(), seq![0x04u8, 83u8, 39u8]) is None, + os2p(toy(), seq![0x04u8, 255u8, 255u8]) is None, + decode_public_key(toy(), seq![0x04u8, 44u8, 40u8]) is None, + decode_public_key(toy(), seq![0x04u8, 44u8, 45u8]) is None, + os2p(toy(), seq![0x04u8, 44u8]) is None, + os2p(toy(), seq![0x04u8, 44u8, 39u8, 0u8]) is None, + os2p(toy(), Seq::::empty()) is None, + os2p(toy(), seq![0x00u8, 0x00u8]) is None, +{ + assert(decode_public_key(toy(), toy_q()) == Some(Point::Affine { x: 44nat, y: 39nat })) + by (compute_only); + assert(decode_public_key(toy(), seq![0x04u8, 1u8, 31u8]) == Some(toy_g())) by (compute_only); + assert(decode_public_key(toy(), seq![0x04u8, 44u8, 44u8]) + == Some(Point::Affine { x: 44nat, y: 44nat })) by (compute_only); + assert(os2p(toy(), seq![0x04u8, 0u8, 0u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x00u8]) == Some(Point::Infinity)) by (compute_only); + assert(decode_public_key(toy(), seq![0x00u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x02u8, 44u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x03u8, 44u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x06u8, 44u8, 39u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x07u8, 44u8, 39u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x05u8, 44u8, 39u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x04u8, 127u8, 39u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x04u8, 44u8, 122u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x04u8, 83u8, 39u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x04u8, 255u8, 255u8]) is None) by (compute_only); + assert(decode_public_key(toy(), seq![0x04u8, 44u8, 40u8]) is None) by (compute_only); + assert(decode_public_key(toy(), seq![0x04u8, 44u8, 45u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x04u8, 44u8]) is None) by (compute_only); + assert(os2p(toy(), seq![0x04u8, 44u8, 39u8, 0u8]) is None) by (compute_only); + assert(os2p(toy(), Seq::::empty()) is None) by (compute_only); + assert(os2p(toy(), seq![0x00u8, 0x00u8]) is None) by (compute_only); +} + +/// Public key decoding on [`p384`]: G decodes; a coordinate equal to p is +/// refused (the largest 48-octet value is `2^384 - 1 ≥ p`), as is a point off +/// the curve, a compressed point, a hybrid point, and the wrong lengths. +pub proof fn lemma_p384_decode_examples() + ensures + decode_public_key(p384(), ex_ecpoint(p384().gx, p384().gy, 48nat)) + == Some(base_point(p384())), + ex_ecpoint(p384().gx, p384().gy, 48nat).len() == 97nat, + decode_public_key(p384(), ex_ecpoint(0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffffnat, p384().gy, 48nat)) is None, + decode_public_key(p384(), ex_ecpoint(p384().gx, 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffffnat, 48nat)) is None, + decode_public_key(p384(), ex_ecpoint(p384().gx, (p384().gy + 1) as nat, 48nat)) is None, + decode_public_key(p384(), ex_ecpoint(p384().gx, p384().gy, 48nat).subrange(0, 96)) is None, + decode_public_key(p384(), ex_ecpoint(p384().gx, p384().gy, 48nat).subrange(0, 49)) is None, + decode_public_key(p384(), seq![0x00u8]) is None, + decode_public_key( + p384(), + seq![0x06u8] + ex_octets(p384().gx, 48nat) + ex_octets(p384().gy, 48nat), + ) is None, + decode_public_key(p384(), seq![0x02u8] + ex_octets(p384().gx, 48nat)) is None, +{ + assert(decode_public_key(p384(), ex_ecpoint(p384().gx, p384().gy, 48nat)) + == Some(base_point(p384()))) by (compute_only); + assert(ex_ecpoint(p384().gx, p384().gy, 48nat).len() == 97nat) by (compute_only); + assert(decode_public_key(p384(), ex_ecpoint(0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffffnat, p384().gy, 48nat)) is None) by (compute_only); + assert(decode_public_key(p384(), ex_ecpoint(p384().gx, 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffffnat, 48nat)) is None) by (compute_only); + assert(decode_public_key(p384(), ex_ecpoint(p384().gx, (p384().gy + 1) as nat, 48nat)) is None) + by (compute_only); + assert(decode_public_key(p384(), ex_ecpoint(p384().gx, p384().gy, 48nat).subrange(0, 96)) + is None) by (compute_only); + assert(decode_public_key(p384(), ex_ecpoint(p384().gx, p384().gy, 48nat).subrange(0, 49)) + is None) by (compute_only); + assert(decode_public_key(p384(), seq![0x00u8]) is None) by (compute_only); + assert(decode_public_key( + p384(), + seq![0x06u8] + ex_octets(p384().gx, 48nat) + ex_octets(p384().gy, 48nat), + ) is None) by (compute_only); + assert(decode_public_key(p384(), seq![0x02u8] + ex_octets(p384().gx, 48nat)) is None) + by (compute_only); +} + +/// Whether `ecdsa_verify_steps` rejects at exactly `step`. +pub open spec fn ex_rejects(c: Curve, h: Seq, r: nat, s: nat, q: Seq, step: Step) -> bool { + ecdsa_verify_steps(c, h, r, s, q) == Result::<(), Step>::Err(step) +} + +/// Whole verifications on [`toy`] (FIPS 186-5 §6.4.2), with the step that +/// rejects. The key is Q = [23]G = (44, 39). The signature was made with +/// k = 2 (R = (81, 52)): digest `B5 12`, so `e = 90` (leftmost 7 bits), +/// `r = 81 mod 67 = 14` (step 9 reduces x_R = 81, which is at least n = 67, +/// so `r1 mod n` matters), and `s = k^-1 (e + r d) mod 67 = 5`. Then +/// `w = 5^-1 = 27`, `u = 90 · 27 mod 67 = 18`, `v = 14 · 27 mod 67 = 43`, and +/// `[18]G + [43]Q = [18 + 43 · 23]G = [1007 mod 67]G = [2]G = R`. +/// +/// The other digests `B5` and `B4 00` have the same `e = 90`. Step 9 rejects +/// a digest with another `e`, another s, and another r. Step 1 rejects r or +/// s equal to 0, n or more than n (r = 81 = 14 + n would pass step 9 if the +/// range were not checked). Step 6 rejects `R1 = O`: with digest `02` (e = 1), +/// r = 32 and s = 5 we get w = 27, u = 27, v = 60, and `27 + 60 · 23 = 21 · 67`, +/// so `[27]G + [60]Q = O`. An invalid Q is `Key` whatever r and s are. +pub proof fn lemma_toy_verify_examples() + ensures + inv(67nat, 5nat) == Some(27nat), + derive_e(toy(), seq![0xB5u8, 0x12u8]) * 27 % 67 == 18nat, + 14nat * 27 % 67 == 43nat, + compute_r1(toy(), 18nat, 43nat, Point::Affine { x: 44nat, y: 39nat }) + == Some(Point::Affine { x: 81nat, y: 52nat }), + ecdsa_verify_steps(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, toy_q()) + == Result::<(), Step>::Ok(()), + // The R = O example's intermediate values. + 32nat * 27 % 67 == 60nat, + compute_r1(toy(), 27nat, 60nat, Point::Affine { x: 44nat, y: 39nat }) == Some(Point::Infinity), + ecdsa_verify(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, toy_q()), + ecdsa_verify(toy(), seq![0xB5u8], 14nat, 5nat, toy_q()), + ecdsa_verify(toy(), seq![0xB4u8, 0x00u8], 14nat, 5nat, toy_q()), + ex_rejects(toy(), seq![0xB6u8], 14nat, 5nat, toy_q(), Step::S9), + ex_rejects(toy(), Seq::::empty(), 14nat, 5nat, toy_q(), Step::S9), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 6nat, toy_q(), Step::S9), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 13nat, 5nat, toy_q(), Step::S9), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 15nat, 5nat, toy_q(), Step::S9), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 0nat, 5nat, toy_q(), Step::S1), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 67nat, 5nat, toy_q(), Step::S1), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 68nat, 5nat, toy_q(), Step::S1), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 81nat, 5nat, toy_q(), Step::S1), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 0nat, toy_q(), Step::S1), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 67nat, toy_q(), Step::S1), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 72nat, toy_q(), Step::S1), + ex_rejects(toy(), seq![0x02u8], 32nat, 5nat, toy_q(), Step::S6), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 44u8, 40u8], Step::Key), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 0nat, 5nat, seq![0x04u8, 44u8, 40u8], Step::Key), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 127u8, 39u8], Step::Key), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 44u8, 122u8], Step::Key), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x02u8, 44u8], Step::Key), + ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x00u8], Step::Key), + !ecdsa_verify(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 44u8, 40u8]), +{ + assert(inv(67nat, 5nat) == Some(27nat)) by (compute_only); + assert(derive_e(toy(), seq![0xB5u8, 0x12u8]) * 27 % 67 == 18nat) by (compute_only); + assert(14nat * 27 % 67 == 43nat) by (compute_only); + assert(compute_r1(toy(), 18nat, 43nat, Point::Affine { x: 44nat, y: 39nat }) + == Some(Point::Affine { x: 81nat, y: 52nat })) by (compute_only); + assert(ecdsa_verify_steps(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, toy_q()) + == Result::<(), Step>::Ok(())) by (compute_only); + assert(32nat * 27 % 67 == 60nat) by (compute_only); + assert(compute_r1(toy(), 27nat, 60nat, Point::Affine { x: 44nat, y: 39nat }) + == Some(Point::Infinity)) by (compute_only); + assert(ecdsa_verify(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, toy_q())) by (compute_only); + assert(ecdsa_verify(toy(), seq![0xB5u8], 14nat, 5nat, toy_q())) by (compute_only); + assert(ecdsa_verify(toy(), seq![0xB4u8, 0x00u8], 14nat, 5nat, toy_q())) by (compute_only); + assert(ex_rejects(toy(), seq![0xB6u8], 14nat, 5nat, toy_q(), Step::S9)) by (compute_only); + assert(ex_rejects(toy(), Seq::::empty(), 14nat, 5nat, toy_q(), Step::S9)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 6nat, toy_q(), Step::S9)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 13nat, 5nat, toy_q(), Step::S9)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 15nat, 5nat, toy_q(), Step::S9)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 0nat, 5nat, toy_q(), Step::S1)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 67nat, 5nat, toy_q(), Step::S1)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 68nat, 5nat, toy_q(), Step::S1)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 81nat, 5nat, toy_q(), Step::S1)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 0nat, toy_q(), Step::S1)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 67nat, toy_q(), Step::S1)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 72nat, toy_q(), Step::S1)) by (compute_only); + assert(ex_rejects(toy(), seq![0x02u8], 32nat, 5nat, toy_q(), Step::S6)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 44u8, 40u8], Step::Key)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 0nat, 5nat, seq![0x04u8, 44u8, 40u8], Step::Key)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 127u8, 39u8], Step::Key)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 44u8, 122u8], Step::Key)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x02u8, 44u8], Step::Key)) by (compute_only); + assert(ex_rejects(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x00u8], Step::Key)) by (compute_only); + assert(!ecdsa_verify(toy(), seq![0xB5u8, 0x12u8], 14nat, 5nat, seq![0x04u8, 44u8, 40u8])) by (compute_only); +} + +/// The public key Q = [d]G on [`p384`], d = 2^300 + 0x123456789abcdef +/// (computed with an independent script), as an ECPoint. +pub open spec fn p384_q() -> Seq { + ex_ecpoint( + 0xf39445b953b052427d51cf8cf3b54cc01a88c516b6830b70b06bc59889871d4a24959921750eed4d695f0c049726386cnat, + 0x9d5d3ebe919597b047016925f5fd77eee99357c9ce0012650574fdd0f0cb9476541e7cc797332396ce321e452e735232nat, + 48, + ) +} + +/// The key `-G = (Gx, p - Gy)`, as an ECPoint. +pub open spec fn p384_minus_g() -> Seq { + ex_ecpoint(p384().gx, (p384().p - p384().gy) as nat, 48) +} + +/// The signature `(r, s)` and the digest integer `e` made from `u = 3`, +/// `v = 2` and Q (see [`lemma_p384_verify_examples`]). +pub open spec fn p384_r() -> nat { + 0x682ab6965e1b69801aa65c3f7f4e123299a18cfa4336e3caeebb8b3fcb07a210e3c6b29f1ace36c95d0199d9fe4e2086nat +} + +/// See [`p384_r`]. +pub open spec fn p384_s() -> nat { + 0x34155b4b2f0db4c00d532e1fbfa709194cd0c67d219b71e5775dc59fe583d10871e3594f8d671b64ae80ccecff271043nat +} + +/// See [`p384_r`]: the digest, as 48 octets. +pub open spec fn p384_digest() -> Seq { + ex_octets( + 0x9c4011e18d291e4027f98a5f3ef51b4be672537764d255b0661950dfb08b731955aa0beea835522e0b8266c6fd7530c9nat, + 48, + ) +} + +/// Whole verifications on [`p384`]. A signature is built backwards, so that +/// step 6 takes a handful of group operations and not about 1,150: pick +/// `u = 3` and `v = 2`, then `R = [3]G + [2]Q`, `r = x_R mod n` (here +/// `x_R < n`), `s = r · v^-1 mod n` and `e = u · s mod n`. The digest is `e` +/// as 48 octets (the leftmost 384 bits of a longer digest give the same +/// `e`). Steps 4 and 5 then give back `w = s^-1`, `e w = u` and `r w = v`. +/// It is a valid signature by the key Q for per-message secret +/// `k = u + v d mod n`, though no hash function produced the digest. +/// +/// Rejections, equally cheap: step 9 for an `r` that is not `x_R` (built the +/// same way from `u = 3`, `v = 2` and another `r`, so that `[3]G + [2]Q` is +/// computed and is not `r`); step 6 for Q = -G with `u = v = 1` +/// (`[1]G + [1](-G) = O`, rule 3, no inversion); step 1 for r or s equal to +/// 0, n or n + 1; and a Q that is invalid. +pub proof fn lemma_p384_verify_examples() + ensures + ecdsa_verify_steps(p384(), p384_digest(), p384_r(), p384_s(), p384_q()) + == Result::<(), Step>::Ok(()), + // A 64-octet digest with the same leftmost 48 octets has the same e. + ecdsa_verify( + p384(), + p384_digest() + ex_octets(0x0123456789abcdefnat, 16), + p384_r(), + p384_s(), + p384_q(), + ), + // Step 9. + ex_rejects( + p384(), + ex_octets( + 0x7fffffffffffffffffffffffffffffffffffffffffffffffe3b1a6c0fa1b96efc75b888dfd5a08a411c48e6a3f6449a0nat, + 48, + ), + 0x1234567890abcdef1234567890abcdefnat, + 0x7fffffffffffffffffffffffffffffffffffffffffffffffe3b1a6c0fa1b96efb52732156cae3ab4ff9037f1aeb87bb1nat, + p384_q(), + Step::S9, + ), + // Step 6. + ex_rejects( + p384(), + ex_octets(0xabcdefnat, 48), + 0xabcdefnat, + 0xabcdefnat, + p384_minus_g(), + Step::S6, + ), + // Step 1. + ex_rejects(p384(), p384_digest(), 0nat, p384_s(), p384_q(), Step::S1), + ex_rejects(p384(), p384_digest(), p384_r(), 0nat, p384_q(), Step::S1), + ex_rejects(p384(), p384_digest(), p384().n, p384_s(), p384_q(), Step::S1), + ex_rejects(p384(), p384_digest(), p384_r(), p384().n, p384_q(), Step::S1), + ex_rejects(p384(), p384_digest(), p384_r(), (p384().n + 1) as nat, p384_q(), Step::S1), + // The public key. + ex_rejects(p384(), p384_digest(), p384_r(), p384_s(), p384_q().subrange(0, 96), Step::Key), + ex_rejects(p384(), p384_digest(), p384_r(), p384_s(), seq![0x00u8], Step::Key), + ex_rejects(p384(), p384_digest(), 0nat, 0nat, seq![0x00u8], Step::Key), +{ + assert(ecdsa_verify_steps(p384(), p384_digest(), p384_r(), p384_s(), p384_q()) + == Result::<(), Step>::Ok(())) by (compute_only); + assert(ecdsa_verify( + p384(), + p384_digest() + ex_octets(0x0123456789abcdefnat, 16), + p384_r(), + p384_s(), + p384_q(), + )) by (compute_only); + assert(ex_rejects( + p384(), + ex_octets( + 0x7fffffffffffffffffffffffffffffffffffffffffffffffe3b1a6c0fa1b96efc75b888dfd5a08a411c48e6a3f6449a0nat, + 48, + ), + 0x1234567890abcdef1234567890abcdefnat, + 0x7fffffffffffffffffffffffffffffffffffffffffffffffe3b1a6c0fa1b96efb52732156cae3ab4ff9037f1aeb87bb1nat, + p384_q(), + Step::S9, + )) by (compute_only); + assert(ex_rejects( + p384(), + ex_octets(0xabcdefnat, 48), + 0xabcdefnat, + 0xabcdefnat, + p384_minus_g(), + Step::S6, + )) by (compute_only); + assert(ex_rejects(p384(), p384_digest(), 0nat, p384_s(), p384_q(), Step::S1)) by (compute_only); + assert(ex_rejects(p384(), p384_digest(), p384_r(), 0nat, p384_q(), Step::S1)) by (compute_only); + assert(ex_rejects(p384(), p384_digest(), p384().n, p384_s(), p384_q(), Step::S1)) + by (compute_only); + assert(ex_rejects(p384(), p384_digest(), p384_r(), p384().n, p384_q(), Step::S1)) + by (compute_only); + assert(ex_rejects(p384(), p384_digest(), p384_r(), (p384().n + 1) as nat, p384_q(), Step::S1)) + by (compute_only); + assert(ex_rejects( + p384(), + p384_digest(), + p384_r(), + p384_s(), + p384_q().subrange(0, 96), + Step::Key, + )) by (compute_only); + assert(ex_rejects(p384(), p384_digest(), p384_r(), p384_s(), seq![0x00u8], Step::Key)) + by (compute_only); + assert(ex_rejects(p384(), p384_digest(), 0nat, 0nat, seq![0x00u8], Step::Key)) by (compute_only); +} + +} // verus! diff --git a/crates/clazel-p384/src/lib.rs b/crates/clazel-p384/src/lib.rs new file mode 100644 index 0000000..42e4007 --- /dev/null +++ b/crates/clazel-p384/src/lib.rs @@ -0,0 +1,26 @@ +//! ECDSA signature verification over NIST P-384, FIPS 186-5 §6.4.2. +//! +//! **Specification only so far.** This crate has no executable code: no +//! field arithmetic, no point code and no `verify` function exist yet. What +//! is here is the part a person reviews, the meaning of "a valid ECDSA +//! P-384 signature", written in Verus, and the contract the later +//! implementation must meet. +//! +//! 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 +//! side-channel claim. Signing and any private-key operation are out of +//! scope. +//! +//! - [`spec`]: a step-by-step transcription of FIPS 186-5 §6.4.2, with the +//! 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. +//! - [`examples`]: known answers, proven by evaluating the spec. +//! - [`certificates`]: the host module for mutation kill certificates +//! (empty until `mutations.json` exists). + +pub mod certificates; +pub mod contract; +pub mod examples; +pub mod spec; diff --git a/crates/clazel-p384/src/spec.rs b/crates/clazel-p384/src/spec.rs new file mode 100644 index 0000000..e3746d5 --- /dev/null +++ b/crates/clazel-p384/src/spec.rs @@ -0,0 +1,696 @@ +//! Executable-style specification of ECDSA signature verification over +//! NIST P-384. Nothing here runs; it defines what "correct" means. +//! +//! # Sources (pinned) +//! +//! Each is the NIST or SECG PDF, identified by the SHA-256 of the file that +//! was transcribed. Step numbers below are those of these texts, read from +//! the text extracted from the PDFs, and for FIPS 186-5 §6.4.2 and B.1 also +//! from the rendered pages; they were not recalled. +//! +//! - **FIPS 186-5**, *Digital Signature Standard (DSS)*, published +//! 3 February 2023, , PDF SHA-256 +//! `fbb9c7c2ba442f03c57b63b43c888311903c9d0f29f89b06efdebd9b619140c5`. +//! §6.4.2 "ECDSA Signature Verification Algorithm" (printed page 25, nine +//! steps), Appendix B.1 "Computation of the Inverse Value" (page 53) and +//! B.2.1 "Conversion of a Bit String to an Integer" (page 54). +//! - **NIST SP 800-186**, *Recommendations for Discrete Logarithm-based +//! Cryptography: Elliptic Curve Domain Parameters*, February 2023, +//! , PDF SHA-256 +//! `53c7cf3340528aaa0a7bbeaef947f2099568192367d4341a7d4abceb55f78432`. +//! §3.2.1 (the Weierstrass equation, a = -3, h = 1), §3.2.1.4 (the P-384 +//! parameters), Appendix D.1.1.1 "Partial Public Key Validation" and +//! Appendix F.1 "Conversion of a Field Element to an Integer". +//! - **SEC 1: Elliptic Curve Cryptography**, version 2.0, 21 May 2009, +//! , PDF SHA-256 +//! `54687189af3de645756a30a801b596fd14c6566992c13bfd58eede399f324a89`. +//! §2.2.1 (the group law), §2.3.1, §2.3.2, §2.3.4, §2.3.6, §2.3.8 and +//! §2.3.9 (conversions), §3.2.2.1 (public key validation) and §4.1.4 +//! (the verifying operation). +//! +//! FIPS 186-5 is the algorithm. Where it defers to "the routine" (Appendix +//! B.1 for the inverse, SP 800-186 Appendix F.1 for the field element to +//! integer conversion, SP 800-186 Appendix D.1 for the public key) the +//! function says which source it follows. FIPS 186-5 gives no group law and +//! no point decoding; those are SEC 1's. +//! +//! # How the extracted text was read +//! +//! The text extracted from the PDFs loses typography, so the pages were +//! also rendered and read. Two losses matter. +//! +//! - FIPS 186-5 §6.4.2 step 3a prints `⌈log2(n)⌉` (ceiling brackets). The +//! extracted text shows `log2(n)`. The brackets are in the PDF, and SEC 1 +//! §4.1.4 step 3.2 prints `⌈log2 n⌉` too. So the number of bits kept is +//! `⌈log2 n⌉`, the bit length `len(n)` of FIPS 186-5 §6.4.1 step 2a and +//! §6.1.1 ("the leftmost len(n) bits"). For a prime n > 2 the two agree, +//! and for P-384 both are 384. A floor reading would give 383 and is not +//! what any of the three texts says. +//! - Step 8 names the integer `r1`, which the extraction prints as `p 1`. +//! +//! # Modelling choices +//! +//! Each one is a deliberate, listed deviation in form or in domain. +//! +//! 1. **The input is the digest H, not the message M.** Step 2 ("Compute H +//! = Hash(M)") is the only use of M, so the meaning is unchanged. The hash +//! is computed by `clazel-crypto`, which holds the hash axioms; **this +//! crate therefore has no axiom.** H is an octet string of any length +//! (the contract limits it to 0 to 64 octets). The bit string "H" of the +//! standard, with `hashlen` bits, is those octets read most significant +//! bit first (SEC 1 §2.3.2), so `hashlen = 8 |H|`. +//! 2. **The domain parameters D are a [`Curve`] value.** FIPS 186-5 is +//! itself parameterised by D. [`p384`] is transcribed from SP 800-186 +//! §3.2.1.4. [`toy`] is a small curve that no standard defines, used +//! only by `examples.rs` and the mutation certificates. The cofactor +//! h = 1 is not a field: both curves have it, and choice 8 uses it. The +//! coefficient a is stored as the residue `p - 3`. FIPS 186-5 §6.4.2 +//! says the validity of D "shall be assured" before verification +//! (§6.2.2 item 1). That is a precondition, not a step: this file +//! transcribes D and does not re-check it at run time. That the +//! transcribed constants satisfy their stated properties is for +//! `lemmas.rs`, and that p and n are prime is cited from SP 800-186. +//! 3. **Division mod m (m = p or m = n) is [`inv`]**: Fermat's +//! `a^(m-2) mod m`, accepted only if it is checked to be an inverse, and +//! `None` (which makes the signature invalid) otherwise. FIPS 186-5 step +//! 4 says "using the routine in Appendix B.1", and B.1 itself says +//! "Other (constant time) algorithms that produce an equivalent result +//! may be used". B.1 is also transcribed here, as [`b1_inverse`], and +//! `examples.rs` evaluates both on the same inputs. For a prime modulus +//! and `0 < z < m` they agree (Fermat's little theorem for [`inv`]; +//! B.1's correctness for [`b1_inverse`]); that is cited, not proven, and +//! the `None` branch of [`inv`] is reachable only for `a ≡ 0`, which +//! steps 1 and 4 and SEC 1 §2.2.1's own case split rule out. +//! 4. **The group law is SEC 1 §2.2.1's affine rules, in its order.** The +//! point at infinity is the distinct [`Point::Infinity`]. SEC 1's rule 3 +//! ("two points with the same x-coordinates when the points are either +//! distinct or have y-coordinate 0") is recognised as `x1 = x2` and +//! `y1 + y2 ≡ 0`, and rule 5 (doubling) is the remaining `x1 = x2` case. +//! On the curve these are the same cases; for points not on the curve +//! SEC 1 defines nothing, and [`ec_add`] is not claimed to mean anything +//! there (the verification never reaches that case, because every point +//! comes from a validated Q or from G). Points are kept with both +//! coordinates in [0, p-1], so `x1 = x2` compares field elements. +//! [`ec_add`] returns `Option` because [`inv`] can fail. +//! 5. **`[k]P` is [`scalar_mul`], MSB-first double-and-add** over [`ec_add`]. +//! SEC 1 §2.2.1 defines kP as P added to itself k times and says it is +//! computed "using the addition rule together with the double-and-add +//! algorithm or one of its variants". That the two are equal follows from +//! the associativity of the group law, which SEC 1 asserts ("The set of +//! points on E(Fp) forms a group") and which is cited, not proven. +//! 6. **`[u]G + [v]Q` is the sum of two separately computed products** +//! (step 6), not a joint ladder. Equal by the same associativity. +//! 7. **Only the uncompressed form is accepted.** SEC 1 §2.3.4 step 2 +//! (compressed points `02`/`03`) is refused: [`os2p`] returns `None`. +//! RFC 5480 §2.2 requires support for the uncompressed form only. SEC 1 +//! §2.3.4 itself refuses every other first octet (step 3.2), so hybrid +//! `06`/`07` is invalid there too, and the point at infinity `00` +//! (§2.3.4 step 1) is decoded and then refused by [`public_key_valid`]. +//! An input whose length is none of the three that §2.3.4 admits is +//! invalid (§2.3.4's input condition is not met). +//! 8. **The public key is always validated, with partial validation.** +//! FIPS 186-5 §6.4.2 says the validity of Q "should also be checked (see +//! Appendix D.1 of SP 800-186)". "Should" does not oblige; this +//! specification rejects an invalid Q. [`public_key_valid`] is SP 800-186 +//! D.1.1.1 steps 1 to 3 (equivalently SEC 1 §3.2.2.1 steps 1 and 2). The +//! check `nQ = O` (SP 800-186 D.1.1.2 step 2, SEC 1 §3.2.2.1 step 4) is +//! omitted. SEC 1 §3.2.2.1 says why that is sound: "if h = 1, then nQ = O +//! is implied by the checks in Steps 2 and 3". P-384 has h = 1 (SP 800-186 +//! §3.2.1.4), so partial validation is full validation. This is checked +//! first, before step 1, following the preamble of §6.4.2 ("validity ... +//! prior to the verification"); the order changes only which [`Step`] is +//! reported, not the verdict. +//! 9. **r and s are integers.** FIPS 186-5 inputs (r, s) are "a pair of +//! integers". The executable code takes 48-octet big-endian strings +//! and converts them with [`os2ip`]; the range check is step 1, here, +//! not a DER rule. +//! 10. **Step 3 is done on bit strings, as printed.** [`derive_e`] reads H +//! as a bit string (SEC 1 §2.3.2), keeps all of it if `⌈log2 n⌉ ≥ hashlen` +//! and otherwise its leftmost `⌈log2 n⌉` bits (SEC 1 §4.1.4 step 3.2), +//! and converts that to an integer by Appendix B.2.1 (SP 800-186 F.4). +//! SEC 1 §4.1.4 goes through an octet string (§2.3.1, which pads on the +//! left with zeros, then §2.3.8); the integer is the same. A digest of 0 +//! octets gives e = 0. The result may exceed n; step 5 reduces it. +//! 11. **Steps 7 and 8 are folded.** Step 7 takes the x-coordinate of the +//! affine representation, which [`Point::Affine`] already is. Step 8 +//! converts it to an integer by SP 800-186 F.1; for an odd prime q, F.1 +//! step 1 is the identity (a is already an integer in [0, q-1]), and so +//! is SEC 1 §2.3.9 step 1. +//! 12. **The result says which step rejected.** [`ecdsa_verify_steps`] +//! returns `Err(step)` so that a deliberate bug in one check can be told +//! apart from a bug elsewhere. The standard's output is only "accept" or +//! "reject"; that is [`ecdsa_verify`]. A failure of [`inv`] or of [`ec_add`] +//! while computing step 4 or step 6 is reported at that step. Step 3 and +//! step 5 cannot reject. FIPS 186-5 prints step 3's second sub-step as +//! "a." again; it is written 3b here (see `docs/ERRATA.md`). +//! 13. **No constant time.** Every input is public. + +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +// --------------------------------------------------------------------- +// Domain parameters (FIPS 186-5 §6.1, SP 800-186 §3.2.1). +// --------------------------------------------------------------------- + +/// The domain parameters D = (q = p, h = 1, n, a, b, G) of FIPS 186-5 §6.1 +/// for a curve `y^2 = x^3 + a x + b` over GF(p) (SP 800-186 §3.2.1), plus +/// `octets`, the length `⌈(log2 p)/8⌉` of a field element as an octet string +/// (SEC 1 §2.3.4's `⌈(log2 q)/8⌉`). The cofactor is 1 (choice 8) and is not a +/// field. `a` is the residue in [0, p-1] (for a = -3, `p - 3`). +pub struct Curve { + /// The prime modulus of the field GF(p). + pub p: nat, + /// The coefficient a, as a residue in [0, p-1]. + pub a: nat, + /// The coefficient b. + pub b: nat, + /// The x-coordinate of the base point G. + pub gx: nat, + /// The y-coordinate of the base point G. + pub gy: nat, + /// The (prime) order of G, which is the order of the group (h = 1). + pub n: nat, + /// The length in octets of a field element: `⌈(log2 p)/8⌉`. + pub octets: nat, +} + +/// NIST P-384, SP 800-186 §3.2.1.4 (printed pages 11-12). Every constant +/// below is the hexadecimal value printed there, and was also checked against +/// the printed decimal value and, for p, against `2^384 - 2^128 - 2^96 + +/// 2^32 - 1`, with a script. +/// +/// - p = `2^384 - 2^128 - 2^96 + 2^32 - 1` +/// - n = `0xffffffff ffffffff ffffffff ffffffff ffffffff ffffffff c7634d81 +/// f4372ddf 581a0db2 48b0a77a ecec196a ccc52973` +/// - a = -3, that is `p - 3` +/// - b, Gx and Gy as printed there +/// - h = 1 (not a field, choice 8) +pub open spec fn p384() -> Curve { + Curve { + p: 0xffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_fffffffe_ffffffff_00000000_00000000_ffffffffnat, + a: 0xffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_fffffffe_ffffffff_00000000_00000000_fffffffcnat, + b: 0xb3312fa7_e23ee7e4_988e056b_e3f82d19_181d9c6e_fe814112_0314088f_5013875a_c656398d_8a2ed19d_2a85c8ed_d3ec2aefnat, + gx: 0xaa87ca22_be8b0537_8eb1c71e_f320ad74_6e1d3b62_8ba79b98_59f741e0_82542a38_5502f25d_bf55296c_3a545e38_72760ab7nat, + gy: 0x3617de4a_96262c6f_5d9e98bf_9292dc29_f8f41dbd_289a147c_e9da3113_b5f0b8c0_0a60b1ce_1d7e819d_7a431d7c_90ea0e5fnat, + n: 0xffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_c7634d81_f4372ddf_581a0db2_48b0a77a_ecec196a_ccc52973nat, + octets: 48, + } +} + +/// A toy curve for evaluated examples. **No standard defines it**, and it is +/// never used by any executable code: it is small enough for `by +/// (compute_only)` to evaluate a whole verification. +/// +/// `y^2 = x^3 - 3x + 50` over GF(83): p = 83 and a = 80 = -3 (mod 83). +/// The group has 67 elements, a prime, so n = 67 and h = 1, and every point +/// other than O generates it. G = (1, 31). Field elements are one octet. n +/// has 7 bits, so a digest is truncated at a bit that is not an octet +/// boundary, and n < p, so an x-coordinate can be at least n and `x mod n` +/// matters (step 9). How it was found and checked is in the comment below; +/// `examples.rs` evaluates the checks that can be. +/// +/// ```text +/// # Search (Python 3): every prime p < 128 and b in [0, p), with +/// # 4a^3 + 27b^2 != 0 mod p for a = -3, counting points by brute force: +/// # count = 1 + sum over x of #{y : y^2 = x^3 - 3x + b} +/// # keeping those whose count n is prime with 64 <= n < p. The one chosen +/// # is (p, b, n) = (83, 50, 67); G is the first point found, (1, 31). +/// # Checks, same script: the curve has 66 affine points (so n = 67 with O); +/// # n * P = O for every one of them with an independent double-and-add +/// # (so each has order n, h = 1); 67 is prime; 83 is prime. +/// ``` +/// +/// `examples.rs` shows `[67]G = O` and `[66]G = -G` by evaluation. +pub open spec fn toy() -> Curve { + Curve { p: 83, a: 80, b: 50, gx: 1, gy: 31, n: 67, octets: 1 } +} + +// --------------------------------------------------------------------- +// Points and the group law (SEC 1 §2.2.1). +// --------------------------------------------------------------------- + +/// A point of E(Fp): the point at infinity O, or an affine point (x, y) with +/// both coordinates in [0, p-1] (SEC 1 §2.2.1). +pub enum Point { + /// The point at infinity O. + Infinity, + /// An affine point `(x, y)`. + Affine { + /// The x-coordinate, in [0, p-1]. + x: nat, + /// The y-coordinate, in [0, p-1]. + y: nat, + }, +} + +/// The base point G of D (FIPS 186-5 §6.1). +pub open spec fn base_point(c: Curve) -> Point { + Point::Affine { x: c.gx, y: c.gy } +} + +/// `x^3 + a x + b` in GF(p), reduced. +pub open spec fn curve_rhs(c: Curve, x: nat) -> nat { + (x * x * x + c.a * x + c.b) % c.p +} + +/// The defining equation `y^2 ≡ x^3 + a x + b (mod p)` (SEC 1 §2.2.1; +/// SP 800-186 §3.2.1). It says nothing about the range of x and y. +pub open spec fn satisfies_equation(c: Curve, x: nat, y: nat) -> bool { + y * y % c.p == curve_rhs(c, x) +} + +/// `x - y` in GF(p), for any naturals x and y, as a residue in [0, p-1]. +pub open spec fn fe_sub(m: nat, x: nat, y: nat) -> nat { + ((x % m) + m - (y % m)) as nat % m +} + +/// `a^e mod m` by square-and-multiply, from the most significant bit of e +/// (a helper of [`inv`], not a step of any standard). +pub open spec fn pow_mod(a: nat, e: nat, m: nat) -> nat + decreases e, +{ + if e == 0 { + 1nat % m + } else { + let half = pow_mod(a, e / 2, m); + let sq = half * half % m; + if e % 2 == 0 { + sq + } else { + sq * (a % m) % m + } + } +} + +/// `a^(-1) mod m` (choice 3): `w = a^(m-2) mod m`, and `Some(w)` only if +/// `a w ≡ 1 (mod m)`; `None` otherwise. `m` is p or n, both prime +/// (SP 800-186 §3.2.1.4), so by Fermat's little theorem the check passes +/// exactly when `a ≢ 0`. FIPS 186-5 step 4 and SEC 1 §2.2.1's divisions +/// both mean this. +pub open spec fn inv(m: nat, a: nat) -> Option { + let w = pow_mod(a, (m - 2) as nat, m); + if (a % m) * w % m == 1 { + Some(w) + } else { + None + } +} + +/// FIPS 186-5 Appendix B.1 steps 3 to 7: the loop of the extended Euclidean +/// algorithm, with the state `(i, j, y2, y1)` of step 2, run until `j` is 0 +/// (step 7 "If (j > 0), then go to step 3"). Returns `(i, y2)`. The caller +/// has already ensured j > 0 (step 1), so the loop body runs at least once, +/// as the standard's does. +pub open spec fn b1_loop(i: nat, j: nat, y2: int, y1: int) -> (nat, int) + decreases j, +{ + if j == 0 { + (i, y2) + } else { + // 3. quotient = ⌊i/j⌋. + let quotient = i / j; + // 4. remainder = i - (j × quotient). That is i mod j, which is also + // what makes the recursion terminate. + let remainder = i % j; + // 5. y = y2 - (y1 × quotient). + let y = y2 - y1 * quotient; + // 6. Set i = j, j = remainder, y2 = y1, and y1 = y. + // 7. If (j > 0), then go to step 3. + b1_loop(j, remainder, y1, y) + } +} + +/// FIPS 186-5 Appendix B.1, "Computation of the Inverse Value" (printed +/// page 53). Input `z` and `a`; `None` is the ERROR indication, and +/// `Some(z^-1 mod a)` is SUCCESS. It is the reference routine of step 4; +/// [`inv`] is the one used (choice 3). +pub open spec fn b1_inverse(z: nat, a: nat) -> Option { + // 1. "Verify that a and z are positive integers such that z < a; if not, + // return an ERROR indication." (Inputs: a is "a positive integer + // greater than 1".) + if !(a > 1 && z > 0 && z < a) { + None + } else { + // 2. Set i = a, j = z, y2 = 0, and y1 = 1. + // 3. to 7. The loop. + let (i, y2) = b1_loop(a, z, 0, 1); + // 8. If (i ≠ 1), then return an ERROR indication. + if i != 1 { + None + } else { + // 9. Return SUCCESS and z^-1 = y2 mod a. + Some((y2 % (a as int)) as nat) + } + } +} + +/// SEC 1 §2.2.1, the addition rule on E(Fp) (printed page 7, rules 1 to 5), +/// in the order printed. `None` is a failed division ([`inv`] returned +/// `None`), which makes the whole verification reject (choice 3). +pub open spec fn ec_add(c: Curve, pp: Point, qq: Point) -> Option { + match (pp, qq) { + // 1. "Rule to add the point at infinity to itself: O + O = O." + (Point::Infinity, Point::Infinity) => Some(Point::Infinity), + // 2. "Rule to add the point at infinity to any other point: + // (x, y) + O = O + (x, y) = (x, y)." + (Point::Infinity, Point::Affine { x, y }) => Some(qq), + (Point::Affine { x, y }, Point::Infinity) => Some(pp), + (Point::Affine { x: x1, y: y1 }, Point::Affine { x: x2, y: y2 }) => { + if x1 == x2 && (y1 + y2) % c.p == 0 { + // 3. "Rule to add two points with the same x-coordinates when + // the points are either distinct or have y-coordinate 0: + // (x, y) + (x, -y) = O." + Some(Point::Infinity) + } else if x1 != x2 { + // 4. "Rule to add two points with different x-coordinates: + // ... λ ≡ (y2 - y1)/(x2 - x1) (mod p), + // x3 ≡ λ^2 - x1 - x2 (mod p), + // y3 ≡ λ(x1 - x3) - y1 (mod p)." + match inv(c.p, fe_sub(c.p, x2, x1)) { + None => None, + Some(w) => { + let lambda = fe_sub(c.p, y2, y1) * w % c.p; + let x3 = fe_sub(c.p, fe_sub(c.p, lambda * lambda % c.p, x1), x2); + let y3 = fe_sub(c.p, lambda * fe_sub(c.p, x1, x3) % c.p, y1); + Some(Point::Affine { x: x3, y: y3 }) + }, + } + } else { + // 5. "Rule to add a point to itself (double a point): Let + // (x1, y1) be a point with y1 ≠ 0. ... + // λ ≡ (3 x1^2 + a)/(2 y1) (mod p), + // x3 ≡ λ^2 - 2 x1 (mod p), + // y3 ≡ λ(x1 - x3) - y1 (mod p)." + // Here x1 = x2 and not rule 3. On the curve that means + // y2 = y1 ≠ 0 (modelling choice 4). + match inv(c.p, 2 * y1 % c.p) { + None => None, + Some(w) => { + let lambda = (3 * x1 * x1 + c.a) % c.p * w % c.p; + let x3 = fe_sub(c.p, lambda * lambda % c.p, 2 * x1 % c.p); + let y3 = fe_sub(c.p, lambda * fe_sub(c.p, x1, x3) % c.p, y1); + Some(Point::Affine { x: x3, y: y3 }) + }, + } + } + }, + } +} + +/// `[k]P` (SEC 1 §2.2.1 "scalar multiplication"; choice 5): MSB-first +/// double-and-add. It handles the bits of `k` from the most significant: the +/// result for `k` is the result for `k / 2`, doubled, plus P when `k` is odd. +/// `[0]P = O`. `None` if any addition fails. +pub open spec fn scalar_mul(c: Curve, k: nat, pt: Point) -> Option + decreases k, +{ + if k == 0 { + Some(Point::Infinity) + } else { + match scalar_mul(c, k / 2, pt) { + None => None, + Some(half) => match ec_add(c, half, half) { + None => None, + Some(twice) => if k % 2 == 1 { + ec_add(c, twice, pt) + } else { + Some(twice) + }, + }, + } + } +} + +// --------------------------------------------------------------------- +// Conversions (SEC 1 §2.3, SP 800-186 Appendix F, FIPS 186-5 B.2.1). +// --------------------------------------------------------------------- + +/// `2^m`, by repeated squaring. +pub open spec fn two_to(m: nat) -> nat + decreases m, +{ + if m == 0 { + 1 + } else if m % 2 == 0 { + let half = two_to(m / 2); + half * half + } else { + 2 * two_to((m - 1) as nat) + } +} + +/// SEC 1 §2.3.8 Octet-String-to-Integer Conversion, step 1: +/// `x = Σ 2^(8(mlen-1-i)) M_i`, the first octet the most significant. +pub open spec fn os2ip(m: Seq) -> nat + decreases m.len(), +{ + if m.len() == 0 { + 0 + } else { + os2ip(m.drop_last()) * 256 + m.last() as nat + } +} + +/// SEC 1 §2.3.2 Octet-String-to-Bit-String Conversion, step 1: "B_8i ... +/// B_8i+7 = M_i". Bit `i` of the result is bit `7 - (i mod 8)` of octet +/// `i / 8` (each octet written most significant bit first). +pub open spec fn octets_to_bits(m: Seq) -> Seq { + Seq::new(8 * m.len(), |i: int| (m[i / 8] as nat / two_to((7 - i % 8) as nat)) % 2 == 1) +} + +/// FIPS 186-5 Appendix B.2.1 (printed page 54), step 2: "{x1, ..., xn} → +/// (x1 × 2^(n-1)) + ... + xn": the first bit is the most significant. The +/// empty bit string is 0. Same as SP 800-186 F.4. +pub open spec fn bits_to_int(b: Seq) -> nat + decreases b.len(), +{ + if b.len() == 0 { + 0 + } else { + bits_to_int(b.drop_last()) * 2 + if b.last() { + 1nat + } else { + 0nat + } + } +} + +/// `⌈log2 n⌉`: the least `L` with `n ≤ 2^L` (0 for n ≤ 1). For a prime n > 2 +/// this is the bit length `len(n)` (see the header, "How the extracted text +/// was read"). +pub open spec fn ceil_log2(n: nat) -> nat + decreases n, +{ + if n <= 1 { + 0 + } else { + 1 + ceil_log2((n + 1) / 2) + } +} + +/// SEC 1 §2.3.6 Octet-String-to-Field-Element Conversion, for q = p an odd +/// prime. Input: an octet string of `mlen` octets (the caller passes +/// exactly `octets`). +pub open spec fn os2fe(c: Curve, m: Seq) -> Option { + // 1. "Convert M to an integer a using the conversion routine specified in + // Section 2.3.8. Output 'invalid' and stop if a does not lie in the + // interval [0, p - 1], otherwise output a." + let a = os2ip(m); + if a < c.p { + Some(a) + } else { + None + } +} + +/// SEC 1 §2.3.4 Octet-String-to-Elliptic-Curve-Point Conversion, with the +/// compressed form refused (choice 7). `None` is "invalid". +pub open spec fn os2p(c: Curve, m: Seq) -> Option { + if m.len() == 1 && m[0] == 0x00 { + // 1. "If M = 00, output P = O." + Some(Point::Infinity) + } else if m.len() == c.octets + 1 { + // 2. The compressed form (`02`, `03`): refused (choice 7). + None + } else if m.len() == 2 * c.octets + 1 { + // 3.1. "Parse M = W || X || Y as a single octet W followed by + // ⌈(log2 q)/8⌉ octets X followed by ⌈(log2 q)/8⌉ octets Y." + let w = m[0]; + let xs = m.subrange(1, 1 + c.octets as int); + let ys = m.subrange(1 + c.octets as int, 1 + 2 * c.octets as int); + if w != 0x04 { + // 3.2. "Check that W = 04. If W ≠ 04, output 'invalid' and stop." + None + } else { + // 3.3. Convert X to a field element x_P (§2.3.6), else invalid. + // 3.4. Convert Y to a field element y_P (§2.3.6), else invalid. + match (os2fe(c, xs), os2fe(c, ys)) { + (Some(x), Some(y)) => + // 3.5. "Check that P = (x_P, y_P) satisfies the defining + // equation of the elliptic curve." + if satisfies_equation(c, x, y) { + // 3.6. "Output P = (x_P, y_P)." + Some(Point::Affine { x, y }) + } else { + None + }, + _ => None, + } + } + } else { + // The input condition of §2.3.4 (one of three lengths) is not met. + None + } +} + +// --------------------------------------------------------------------- +// Public key validation (SP 800-186 D.1.1.1, SEC 1 §3.2.2.1). +// --------------------------------------------------------------------- + +/// SP 800-186 Appendix D.1.1.1 Partial Public Key Validation (identical to +/// SEC 1 §3.2.2.1 steps 1 and 2 for a prime field). The check `nQ = O` +/// (SEC 1 §3.2.2.1 step 4) is omitted because h = 1 (choice 8). +pub open spec fn public_key_valid(c: Curve, q: Point) -> bool { + match q { + // 1. "If Q is the point at infinity, output REJECT." + Point::Infinity => false, + Point::Affine { x, y } => + // 2. "Verify that x and y are integers in the interval [0, p-1]." + // 3. "Verify that (x, y) is a point on W_a,b by checking that (x, y) + // satisfies the defining equation y^2 = x^3 + ax + b, where + // computations are carried out in GF(p)." + // 4. "Otherwise, output ACCEPT." + x < c.p && y < c.p && satisfies_equation(c, x, y), + } +} + +/// The public key Q as the octet string `q` (an ECPoint): converted by SEC 1 +/// §2.3.4 ([`os2p`]), then validated ([`public_key_valid`]). `None` rejects. +pub open spec fn decode_public_key(c: Curve, q: Seq) -> Option { + match os2p(c, q) { + Some(pt) => if public_key_valid(c, pt) { + Some(pt) + } else { + None + }, + None => None, + } +} + +// --------------------------------------------------------------------- +// FIPS 186-5 §6.4.2. +// --------------------------------------------------------------------- + +/// The step that rejected a signature (modelling choice 12). `Key` is the +/// validity check of Q that FIPS 186-5 §6.4.2's preamble puts before step 1. +/// Steps 2, 3, 5, 7 and 8 cannot reject. `S6` also covers a failed division +/// inside the group law, `S4` a failed inverse of s. +pub enum Step { + /// The public key Q is not a valid point (preamble of §6.4.2). + Key, + /// Step 1: r or s is not an integer in [1, n - 1]. + S1, + /// Step 4: s has no inverse mod n. + S4, + /// Step 6: R1 is the point at infinity (or a group operation failed). + S6, + /// Step 9: r ≠ r1 mod n. + S9, +} + +/// The integer `e` of step 3: "Derive the integer e from H as follows". +/// `h` is the digest H as octets; the bit string H has `hashlen = 8 |h|` +/// bits (choice 1). +pub open spec fn derive_e(c: Curve, h: Seq) -> nat { + let hbits = octets_to_bits(h); + let hashlen = hbits.len(); + // 3a. "If ⌈log2(n)⌉ ≥ hashlen, set E = H. Otherwise, set E equal to the + // leftmost ⌈log2(n)⌉ bits of H." + let e_bits = if ceil_log2(c.n) >= hashlen { + hbits + } else { + hbits.take(ceil_log2(c.n) as int) + }; + // 3b. (printed "a.") "Convert the bit string E to the integer e as + // specified in Appendix B.2.1." + bits_to_int(e_bits) +} + +/// `R1 = [u]G + [v]Q` (step 6), by choices 5 and 6. +pub open spec fn compute_r1(c: Curve, u: nat, v: nat, q: Point) -> Option { + match (scalar_mul(c, u, base_point(c)), scalar_mul(c, v, q)) { + (Some(ug), Some(vq)) => ec_add(c, ug, vq), + _ => None, + } +} + +/// FIPS 186-5 §6.4.2 ECDSA Signature Verification Algorithm (printed page +/// 25), . +/// +/// Inputs: the domain parameters D (`c`), the digest H of the message +/// (choice 1), the pair of integers (r, s) and the purported verification key +/// Q as an octet string `q`. `Ok(())` is "accept"; `Err(step)` is "reject" +/// at that step. +pub open spec fn ecdsa_verify_steps(c: Curve, h: Seq, r: nat, s: nat, q: Seq) -> Result< + (), + Step, +> { + // Preamble: "The validity of the public key Q should also be checked (see + // Appendix D.1 of SP 800-186)." (choice 8) + match decode_public_key(c, q) { + None => Err(Step::Key), + Some(qp) => + // 1. "Verify that both r and s are integers in the interval + // [1, n - 1]. Output 'reject' if verification fails." + if !(1 <= r && r <= c.n - 1 && 1 <= s && s <= c.n - 1) { + Err(Step::S1) + } else { + // 2. "Compute H = Hash(M) ..." Folded: H is the input (choice 1). + // 3. "Derive the integer e from H as follows: ..." + let e = derive_e(c, h); + // 4. "Compute s^-1 mod n using the routine in Appendix B.1." + // (choice 3) + match inv(c.n, s) { + None => Err(Step::S4), + Some(w) => { + // 5. "Compute u = e · s^-1 mod n and v = r · s^-1 mod n." + let u = e * w % c.n; + let v = r * w % c.n; + // 6. "Compute R1 = [u]G + [v]Q. Output 'reject' if R1 is + // the identity element (the point at infinity)." + match compute_r1(c, u, v, qp) { + None => Err(Step::S6), + Some(Point::Infinity) => Err(Step::S6), + // 7. "Set xR to the x-coordinate of the affine + // representation of R1 = (xR, yR)." + Some(Point::Affine { x: x_r, y: y_r }) => { + // 8. "Convert the field element xR to the integer + // r1, using the conversion routine in SP + // 800-186, Appendix F.1." F.1 step 1: for an + // odd prime q, x = a (choice 11). + let r1 = x_r; + // 9. "Verify that r = r1 mod n. Output 'reject' + // if verification fails; output 'accept' + // otherwise." + if r == r1 % c.n { + Ok(()) + } else { + Err(Step::S9) + } + }, + } + }, + } + }, + } +} + +/// Whether FIPS 186-5 §6.4.2 outputs "accept" ([`ecdsa_verify_steps`] is +/// `Ok`). +pub open spec fn ecdsa_verify(c: Curve, h: Seq, r: nat, s: nat, q: Seq) -> bool { + ecdsa_verify_steps(c, h, r, s, q) is Ok +} + +} // verus! diff --git a/docs/ERRATA.md b/docs/ERRATA.md index d0dd745..df33ac6 100644 --- a/docs/ERRATA.md +++ b/docs/ERRATA.md @@ -221,3 +221,39 @@ it evidently means. Each entry records what we specified instead. `crates/clazel-tls/src/connection/dispatcher_spec.rs` (protected handshake). - **Reported upstream:** not yet. + +## FIPS 186-5 §6.4.2 step 3 numbers its two sub-steps "a." and "a." + +- **Spec:** FIPS 186-5, *Digital Signature Standard (DSS)*, published + 3 February 2023 (PDF SHA-256 + `fbb9c7c2ba442f03c57b63b43c888311903c9d0f29f89b06efdebd9b619140c5`), + §6.4.2 "ECDSA Signature Verification Algorithm", printed page 25, + +- **Text:** step 3 "Derive the integer e from H as follows:", then "a. If + ⌈log2(n)⌉ ≥ hashlen, set E = H. Otherwise, set E equal to the leftmost + ⌈log2(n)⌉ bits of H." and then again "a. Convert the bit string E to the + integer e as specified in Appendix B.2.1." +- **Problem:** two sub-steps carry the label "a." (the signing algorithm, + §6.4.1 step 2, labels them "a." and "b."). A citation "step 3a" is + ambiguous. +- **We specify:** the second sub-step is 3b, and the first is 3a. See + `derive_e` in `crates/clazel-p384/src/spec.rs`. +- **Reported upstream:** not yet. + +## FIPS 186-5 §6.4 says "the leftmost n bits" of a long hash, where n is the order + +- **Spec:** as above, §6.4 "ECDSA Digital Signature Generation and + Verification", printed page 23. +- **Text:** "When the length of the output of the hash function (or XOF) is + greater than the bit length of n, then the leftmost n bits of the hash + function (or XOF) output block shall be used in any calculation using the + hash function (or XOF) output". +- **Problem:** the symbol n is the order of the base point, a number of 384 + bits for P-384 (SP 800-186 §3.2.1.4), so "the leftmost n bits" read + literally asks for about 2^384 bits. The same paragraph's first clause + says "the bit length of n", §6.1.1 says "the leftmost len(n) bits", and + §6.4.2 step 3a says "the leftmost ⌈log2(n)⌉ bits". +- **We specify:** the leftmost `⌈log2 n⌉` bits, which for a prime n > 2 is + `len(n)`, as in §6.4.2 step 3a and SEC 1 §4.1.4 step 3.2. See `derive_e` + in `crates/clazel-p384/src/spec.rs`. +- **Reported upstream:** not yet.