From 023961094e49e7299a6e2d701875015fe9837e1a Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 6 Aug 2026 20:54:44 +0200 Subject: [PATCH] docs: state the signing exclusion (round-7 review, ed-scope-exclusions-missing) Every certificate here covers the VERIFICATION path; nonce derivation, the secret scalar multiplication, s-assembly and key generation were never extracted, never modeled, and no theorem mentions them. That was always true. No document in this repository said it, which round-7 external review correctly flagged as a missing required exclusion. The new final item states it, names the concrete consequence (a nonce-reusing signer emits key-leaking signatures the proven verifier rightly accepts, every certificate green), and states the deployment fact for this fork. Appended rather than renumbered: existing items are cited by number elsewhere. The cost of the silence is recorded in the item itself: the estate's own author twice mangled the sign/verify boundary in one session before writing this. A trust document that states only what IS covered invites over-reading. Doc-only: TRUSTED-BASE.md is pinned by no harness map and gated by no button. Co-Authored-By: Claude Opus 4.8 --- TRUSTED-BASE.md | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 0261497..6bcd6b4 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -273,3 +273,32 @@ running Rust code. Everything else is machine-checked. The general lesson, which is why the purge is worth its minutes: a verification that never cleans up cannot distinguish "these proofs check" from "these proofs check given whatever happens to be lying around". + +14. **The signing side of this library — not covered, by anything, at all.** + Every certificate in this repository is about the VERIFICATION path: the + apex is `verify_accepts_iff`, an acceptance decision over a message, + public key and candidate signature. Producing a signature is different + code — nonce derivation from the hashed secret key, the scalar + multiplication by the secret, the assembly of `s = r + H(R,A,M)·a mod ℓ` — + and none of it was extracted, none of it is modeled, and no theorem here + mentions it. Key generation likewise. This was always true; until + 2026-08-06 no document in this repository said it, which round-7 external + review (GPT-5.6) correctly flagged as a missing required exclusion. + + Concretely, so the consequence is not left to the reader: a defective + signer — say one that reuses or biases its nonce, the classic key-leaking + failure — would emit signatures this repository's proven verifier happily + accepts, because they are valid signatures. Every certificate would hold. + The green button says nothing about whether the private key survived the + signing operation. + + Deployment note: this fork's proven verify path serves as an independent + quorum member for checking the pacta transparency log's head signatures. + That use needs only the verification half — which is the proven half. No + signing code from this repository is deployed anywhere. + + The silence of this document on that point had a measured cost: the + estate's own author, in 2026-08-06 session notes, twice mangled which half + of which library the proofs cover. A trust document that states only what + IS covered invites every reader to over-read it; this item is the + counterweight.