Repository navigation
clazel-p384: ECDSA P-384 verification spec (3.5h, PR1), tier 0 - #22
Merged
Merged
Conversation
Specification and contract only: no field arithmetic, no point code and no exec implementation. Tier 0, target tier 2. spec.rs transcribes the nine steps of FIPS 186-5 6.4.2 (step numbers read from the extracted text and, for 6.4.2 and Appendix B.1, the rendered pages), with the routines it defers to taken from SP 800-186 (D.1.1.1, F.1, 3.2.1.4) and SEC 1 v2 (2.2.1 group law, 2.3 conversions, 3.2.2.1, 4.1.4). Sources are pinned by SHA-256; 13 modelling choices are listed in the header. The P-384 constants were checked with a script against both printed forms (hex and decimal), p = 2^384 - 2^128 - 2^96 + 2^32 - 1, the curve equation at G, [n]G = O and the primality of p and n. toy() is a 7-bit curve for evaluated examples (search and checks recorded in its doc comment). The digest-truncation length is read as ceil(log2 n): the PDF prints the ceiling brackets that the text extraction loses, and SEC 1 4.1.4 step 3.2 prints them too. docs/ERRATA.md records the duplicated "a." sub-step label of step 3 and a "leftmost n bits" slip in FIPS 186-5 section 6.4; neither reported upstream. contract.rs states verify's requires/ensures as predicates, the way clazel-pkcs1 does before its exec exists. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
examples.rs proves, by (compute_only), known answers for the spec's functions. On toy() (p = 83, n = 67, h = 1): conversions, step 3 with a digest cut at a non-octet bit, inverses (Fermat and FIPS B.1 agree), the group law and [k]G including [67]G = O, public key decoding (infinity, compressed, hybrid, coordinate >= p, off-curve, wrong lengths), and whole verifications: valid (with x_R >= n), step 1, 6 and 9 rejections and an invalid key. On p384(): G on the curve, 2G and 3G, key decoding, and verifications with small scalars built backwards from (u, v). A verification with full-size scalars times out in the compute_only interpreter and is not included. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
CI's mutation step fails a Verus crate with no mutations.json. 26 mutations of spec.rs, covering the step 1, 5, 6 and 9 checks, step 3's truncation, the conversions, point decoding and validation, the group law, double-and-add, the checked inverse, B.1 and the P-384 constants. Each is killed with a certificate against an evaluated example. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
PR1 of P-384 ECDSA verification (proposed item 3.5h): the new crate
clazel-p384, specification only. There is no field arithmetic, no point code and no exec yet. The crate is tier 0, with target tier 2.Commits
c906b96spec:src/spec.rsandsrc/contract.rs, twodocs/ERRATA.mdentries, the crate skeleton and README.2a45487:src/examples.rs, known answers provenby (compute_only).What the spec says
ecdsa_verify_steps(curve, digest, r, s, q)transcribes FIPS 186-5 §6.4.2's nine steps, each quoted. It returns the step that rejected. The parts it relies on:nQ = Ocheck is left out, which SEC 1 §3.2.2.1 says h = 1 allows.a^(m−2), accepted only after checking that it really is an inverse. FIPS B.1 is also transcribed, as a reference.⌈log2 n⌉. The ceiling was confirmed on the rendered page.The file header lists 13 modelling choices.
contract.rsgives the future execverify(digest, r: &[u8; 48], s: &[u8; 48], point), which requires a digest of at most 64 octets. Followingclazel-pkcs1's pattern, it is predicates only.Sources
Pinned by PDF SHA-256 in the header: FIPS 186-5, SP 800-186 and SEC 1 v2. Step numbers were read from those texts. Several numbers in the design note were wrong and have been corrected here: §6.4.2 has nine steps, not eight, and the P-384 parameters are in §3.2.1.4.
Checks done
16 verified, 0 errors(clean cache).cargo xtask check: passes. It listsspec.rsandcontract.rsas unreviewed.Limits, stated plainly
compute_onlytimes out on a full P-384 verification. The P-384 examples therefore use signatures built backwards from small u and v: genuine signatures for that key, but over a digest that no hash produced. The toy curve y² = x³ − 3x + 50 over GF(83), with n = 67 and h = 1, covers whole verifications.ring, and an independent transcription.CI has not run yet.
🤖 Generated with Claude Code