saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-04 20:24:12 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs: state the signing exclusion (round-7 review, ed-scope-exclusions-missing)

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-08-06 20:54:44 +02:00
parent a6e5e89120
commit fa22ececa7
1 changed files with 32 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
TRUSTED-BASE.md
View file

@ -272,3 +272,35 @@ running Rust code. Everything else is machine-checked.
The general lesson, which is why the purge is worth its minutes: a The general lesson, which is why the purge is worth its minutes: a
verification that never cleans up cannot distinguish "these proofs check" verification that never cleans up cannot distinguish "these proofs check"
from "these proofs check given whatever happens to be lying around". 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.
This is not hypothetical for THIS fork. The pacta transparency log signs
its published tree heads with this library's signing path, and records
`signing_backend: verified-dalek-serial` in every head. The word
"verified" in that name refers to the verification certificates in this
repository — the attested artifact was used, rather than an unattested
third implementation — and must NOT be read as a claim that the signing
operation which produced the signature is itself proven. It is not.
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.