diff --git a/docs/spec/PRIMER.md b/docs/spec/PRIMER.md new file mode 100644 index 0000000..bf633d0 --- /dev/null +++ b/docs/spec/PRIMER.md @@ -0,0 +1,269 @@ +# Ceremony Suite — Agent Onboarding Primer + +**Read this first.** You have been brought online to work on the **Ceremony +Suite**: the specification (and eventually the proven implementation) of how +an agent system decides *who may do what*, binds those decisions to a +tamper-evident history, and proves it. This primer gets you from cold to +productive. It is opinionated on purpose — the design has survived multiple +adversarial reviews, and the conventions below are how it stays sound. + +If you read nothing else, read: this file, then +[`README.md`](README.md) (the suite index), then the one profile you were +assigned. The five laws in [`ceremony-contract.md`](ceremony-contract.md) §4 +are the spine of everything. + +--- + +## 1. What this is, in one breath + +Agent harnesses need to enforce authority: run this command? trust this +peer? pin this key? The **Ceremony Contract** is the library-side contract +for those decisions; the **Ceremony Suite** is that contract split into +seven documents, each provable in isolation, with the five laws as a *narrow +waist*. + +The deliverable for end-users is a harness (newt, hermes, gila, a Claude +Code / Codex plugin) that prompts a human at the right moment and enforces +the answer. Everything here is the plumbing that makes those prompts +**honest** — cryptographically bound to what actually executes, and provably +unable to widen authority behind the user's back. + +## 2. Why it matters — the contribution + +A verified research pass established that the *ideas* here are ~30 years of +mainstream consensus (Saltzer's identifier/locator split, Host Identity +Protocol, NIST 800-207 Zero Trust, SPIFFE, iroh's "dial the key, not the +IP"). We are not inventing the loc/ID split. + +**The unique contribution is the enforcement gate.** Nobody ships +*first-contact ceremony enforcement* — fail-closed, consumer-rendered, +presence-attested, caveat-attenuated — as a reusable, harness-agnostic, +formally-verified library. HIP admits the trust-on-first-use "leap of faith" +and ships nothing; SSH/Signal bake a prompt into one client; WebPKI/Tailscale +centralize; SPIRE automates the human away. WebAuthn is the closest precedent +(relying-party library enforces, platform renders) but is user→service, not +peer↔peer agent introduction. + +So the moat is **the contract, not the crate**: publish the spec so any +harness can comply without taking a dependency; `agent-bridle` is the +reference implementation. Client libraries follow in Rust, Python, Dart, and +TypeScript (one Rust enforcement core; the other languages implement the +*consumer* side only — never fork the gate). + +## 3. The doctrine (load-bearing beliefs — internalize these) + +These are not style preferences; violating them has repeatedly produced real +bugs that adversarial reviewers found. + +1. **The authenticated thing is always the key, never the channel.** + Locations, relays, registries, and rendered pixels are candidates and + hints; signatures and content-IDs are what a gate trusts. (This is the + floating-identity doctrine — see agent-mesh `docs/decisions/ + floating_identity.md`. Identity floats; harnesses are fungible substrate.) +2. **No authorization or claim floats free of the exact history and + artifacts that gave it meaning.** A decision binds the request; the + request binds the executable effect; an attestation binds a non-regressing + history checkpoint. +3. **Law minimalism.** A good system has only the laws it absolutely needs. + *Nothing enters the law section without a proof obligation demanding it;* + everything else is mechanism (a profile) or well-formedness. We have gone + 6 → 5 laws and absorbed four review rounds of additions at **zero** net + law cost. The algebra decides the count; ambition does not. +4. **Libraries expose decision STRUCTS and seams; they contain NO TUI.** + `agent-bridle` / `agent-mesh` / `agent-*` are libraries. They expose a + `DecisionSurface` seam that *demands* a consumer-built UI; they never + render. newt draws a matrix chooser, hermes a flat list, a daemon reads a + policy file — one struct, many layouts. (Backlog: agent-bridle#225.) +5. **Algorithms are pins, not laws.** Laws name *properties* (collision + resistance, determinism); a profile pins the algorithm; identifiers are + self-describing (multihash/multicodec). *"BLAKE3 is an implementation + detail."* Agility needs an allowlist checked before dispatch, or it is a + downgrade attack. +6. **Honesty over completeness.** When a mechanism does not fully close a + gap, name the residual (rendering faithfulness is not cryptographic; the + chain alone does not stop rollback). A claim stronger than the machinery + is the exact failure adversarial review punishes: *"prose becomes + authority-bearing protocol."* +7. **Publish over patent.** Default to publishing defensively. + +## 4. The architecture: the suite + +Seven documents. Each is a **decision** with a lifecycle: *Proposed → +Accepted → Proven*. A downstream decision **cannot be Accepted until its +dependencies are Proven** — that is the "chain of decisions." + +| # | Profile | Owns | +|---|---|---| +| **P0** | [`ceremony-contract.md`](ceremony-contract.md) | the five laws, the authority lattice, the `DecisionSurface` seam, gate acceptance — **the narrow waist** | +| **P1** | [`signed-object-profile.md`](signed-object-profile.md) | naming, canonicalization, signatures, the signed-bytes envelope, the algorithm allowlist | +| **P2** | [`chain-store-profile.md`](chain-store-profile.md) | the causal-transcript store, the linear authority spine, the external anti-rollback anchor | +| **P3** | [`enrollment-protocol.md`](enrollment-protocol.md) | introductions, SAS pairing, external anchors | +| **P4** | [`identity-lifecycle.md`](identity-lifecycle.md) | roles & delegation, records, quorum revocation, break-glass/succession | +| **P5** | [`rendering-security-profile.md`](rendering-security-profile.md) | effect binding, gate-signed requests, surface attestation | + +**Dependency order:** `P1 → P2 → P0 → P4 → P3`, with P5 on {P0, P1, P4}. +(P0 depends on P4 only via *abstract contracts P0 itself defines* — +`AttestEvidence`, `ValidAssociationProof` — which P4 implements. That +dependency inversion is what keeps the graph acyclic; do not reintroduce a +concrete P4 type into P0.) + +The provable MVP is **P1 + P2 + P0** — the waist. Ceremonies (P3–P5) graft +on once the waist is Proven. `suite.toml` pins which profile versions form +one compatible suite. + +## 5. The three tiers of "teeth" (do not confuse them) + +Correctness is enforced in layers, each verified by a *different* tool. A +proof that silently assumes the wrong tier is the classic failure mode. + +- **Tier 3 — Lean + Aeneas (kernel refinement).** The authority *algebra* + and the trusted *state machine* (P0/P1/P2/P4). A pure Rust kernel is + extracted by Charon and proven in Lean via Aeneas to refine the model. CI + gate: no Rust kernel merges unless the refinement proof passes. +- **Tier 2 — Tamarin / ProVerif (protocol safety).** The *ceremonies* (P3, + parts of P5). A flawless lattice can sit behind a leaky handshake, so + MITM / replay / unknown-key-share get *symbolic* proof, not algebraic. +- **Tier 1 — cryptographic primitives (assumed).** Ed25519 unforgeability, + BLAKE3 collision resistance, deterministic nonces. Cited, not proven; the + trust base; rotatable via P1's allowlist. +- **Cross-cutting — conformance vectors.** Shared JSON vectors bind the four + client languages to one observable behaviour where proofs stop. + +The pure kernel is `resolve` + precedence + the gate acceptance checklist + +the P2 trusted-state transition — **no serde, no IO, no crypto impl, no UI**. +Crypto enters the kernel as *abstract injective/one-way contracts* (P1's job +to satisfy). Keeping that boundary is what lets Aeneas run. + +Toolchain setup (Lean/elan, Charon nightly, opam/OCaml for Aeneas, per OS): +[`../TOOLCHAIN.md`](../TOOLCHAIN.md). + +## 6. The five laws (memorize these) + +From P0 §4. Each has a proof obligation. + +- **L1 — Resolution is a meet.** Verdicts are ordered `deny ⊏ attest ⊏ ask + ⊏ approve`; `resolve` is the meet of matching verdicts, **with the no-match + case defined explicitly as `ask`** (empty meet = ⊤ = approve would fail + *open* — this is a subtle bug we fixed). Order-independent. (PO-1) +- **L2 — Tamper-boundedness.** A sub-quorum actor can neither *widen* + authority nor *shrink* the load-bearing identity structure. Revoking an + identity requires quorum ("reset mesh" must not be a DoS). Rollback + resistance needs an *external* anchor, not the chain alone. (PO-2/2a/2b/2c) +- **L3 — Fail-closed totality.** `resolve` is total; headless degrades + `ask/attest ↦ deny`. Nothing reaches "undefined permission." (PO-3) +- **L4 — Attenuation.** `effective = granted ⊓ required`; authority composes + by meet, never amplifies; `escalate` carries ⊥ authority. (PO-4) +- **L5 — The ceremony gate.** `association ⇒ pinned`; `fingerprint = + H(pubkey)` is self-certifying, so re-key ⇒ re-ceremony; pinned is + transitive through certification (delegation). (PO-5) + +## 7. Glossary (speak the same language) + +- **Fingerprint** — `H(pubkey)` as a multihash; a self-describing *name* for + a key. The key is the identity; the fingerprint is its name. +- **Verdict** vs **matrix verb** — `deny/attest/ask/approve` are *verdicts* + (resolution's codomain); `allow/attest/deny` are *matrix verbs* (what a + surface offers). `allow` = `approve` seen from the offer side. `ask` is a + verdict, never an offer. `escalate` is a navigation action (⊥ authority), + never a verdict. +- **attest** — the presence-required disposition (a fresh WebAuthn/passkey + ceremony). Renamed from `passkey` (that word now names only the hardware + mechanism; rename tracked in #231). Term follows the attestation + literature (Parno et al.). +- **chain-store** — the append-only-verifiable record log; a Merkle DAG. The + *authority projection* of the wider Conversation Graph (agent-mesh#67). +- **causal transcript / authority spine** — the store is a DAG for + conversation but a **linear spine per causal thread** `(store_id, + thread_id, sequence)` for authority. Conversation is a jungle; authority + is a railway. +- **checkpoint / anchor** — the highest `AuthorityCheckpoint` a participant + has accepted, kept *outside* the store it validates (device keystore / + TPM / witness quorum). Rollback resistance lives here. +- **Sealed** — a wire object constructed only through verification; + immutable after. The Rust heir of the `Memo` discipline. +- **Gate** — the enforcement choke-point; mints authority only after its + acceptance checklist passes. Never trusts the surface. +- **Caveats** — attenuable authority; a meet-semilattice (`meet_never_ + amplifies` is property-tested upstream in agent-mesh-protocol). + +## 8. How we got here — the review discipline + +This spec is the product of **heterogeneous adversarial review**: successive +passes by different model families (Claude, GPT-5/Codex, others), each trying +to break it. That is not incidental — it is the method. A cross-model +adversary finds what four same-model rounds miss. + +- Findings are triaged into an **obligations ledger** (`README.md` → "Spec + obligations"), tagged blocker/high/medium, each mapped to the owning + profile. +- We fix by **naming and binding a mechanism**, not by adding a law. +- We record the *residual* honestly when a fix is partial. +- Every review round to date has *strengthened* the design and held the law + count at five. The last full pass moved the criticism from "the + architecture is confused" to "four interfaces need exact state-machine + definitions" — which is victory, not defeat. + +When you find a gap: add it to the obligations ledger with a resolution +direction before (or instead of) arguing it in prose. + +## 9. Current state & what is HELD + +- **PR #229** carries the whole suite on branch `docs/spec-ceremony-contract`. +- **PR #232** (GPT-5/Codex) is the stacked *formal kernel* design — adopted + as the P0+P1+P2 provable MVP. +- **Status: design draft, actively reviewed.** Spec **revisions are open**; + **merge and implementation are HELD** pending the author's sign-off. Do + not merge to `main`; do not start the Lean/Rust/Aeneas implementation + until told. (When in doubt, the hold is: *revise freely, land nothing.*) +- **Open author's-calls** (do not decide these yourself): (a) the OB-2 + *linear authority spine vs. frontier checkpoint* model — currently adopted + as linear, pending veto; (b) the **`attest` factorization** — one verb + axis vs. `effect × assurance × scope` (GPT-5 #232 leans product-lattice; + L1 survives either). + +## 10. How to contribute (the workflow) + +Follow `AGENTS.md` and `../DESIGN.md` at the repo root; the essentials: + +- **Branch → change → `just check` green → push → PR.** Never push to + `main`. `just check` = fmt + clippy `-D warnings` (both feature configs) + + tests. `just install-hooks` after clone; **never `--no-verify`** in this + repo. +- **Concurrency hazard:** more than one agent writes the spec branch. Always + `git fetch` first; work in a throwaway **worktree**; if a push is rejected, + `git rebase` onto the moved branch (verify tree parity if the history was + rewritten). Remove your worktree when done (disk discipline). +- **Commit hygiene:** author `hartsock@users.noreply.github.com`; trailer + `Co-Authored-By: Claude Opus 4.8 (1M context) `. + **Never** put a Claude session URL / `Claude-Session:` trailer in a commit + or PR body — banned, enforced by hook where present. +- **Spec edits** cross-reference the owning profile and cite the obligation + (`OB-n`) or law they serve. Keep the five-law waist sacred: a new law needs + a proof obligation and an author decision. +- **When implementation opens** (not yet): build order `P1 → P2 → P0`; carve + the pure kernel first; wire Charon→Aeneas→Lean; keep crypto behind abstract + contracts. + +## 11. Map — where everything lives + +- **This suite:** `docs/spec/` (you are here). Index: `README.md`. Manifest: + `suite.toml`. Toolchain: `../TOOLCHAIN.md`. +- **Reference implementation:** `agent-bridle` crates (`agent-bridle-core` + owns the policy/verdict/gate; `step_up::DischargeVerifier` is the shipped + presence seam; #226/#227 shipped signed loosening entries). +- **Mesh side:** `agent-mesh` — `Introduction`/decision surfaces (#65), + enrollment + multihash `Fingerprint` (#66), the **Conversation Graph** + (#67); `CertChain::verify` + proof-of-possession (#39/#40); + `docs/decisions/floating_identity.md` (the doctrine). +- **First consumer:** newt-agent#1209 (the pinning ceremony, HIGH). +- **Umbrella / strategy:** agent-bridle#225 (the no-TUI directive, client-lib + matrix, the contribution framing). Rename: #231 (`passkey`→`attest`). +- **Prior art (cite, don't reargue):** Saltzer RFC 1498; HIP RFC 7401/9063; + NIST SP 800-207; SPIFFE; iroh; RFC 6962 (CT); TUF; Schneier-Kelsey; FssAgg + (eprint 2008/185); Landrock-Pedersen 1998 (WYSIWYS); RFC 8785 (JCS). + +--- + +*The rule underneath all of it: no authorization floats free of the history +and artifacts that gave it meaning. Everything else is how we make that +true and prove it.* diff --git a/docs/spec/README.md b/docs/spec/README.md new file mode 100644 index 0000000..21fc460 --- /dev/null +++ b/docs/spec/README.md @@ -0,0 +1,240 @@ +# The Ceremony Suite — a dependency-ordered set of provable profiles + +> **New to this job? Start with [`PRIMER.md`](PRIMER.md)** — the agent +> onboarding doc (doctrine, architecture, conventions, current hold, how to +> contribute). Then this index, then your assigned profile. + +**Status:** DRAFT (2026-07-16). This directory replaces the single +`ceremony-contract.md` monolith with a suite of **loosely-coupled, +functionally-cohesive** profiles: each names one job, owns its own algebra +and proof obligations, and exposes a narrow seam the others depend on. The +five laws are the **narrow waist**; everything else is a profile that either +supplies a mechanism the laws assume or consumes the laws to build a +ceremony. + +This is the project's architecture doctrine applied to its own +specification: *group what works together to do one job into a unit named +for it; expose only the narrow seam.* + +## Why a suite, not a constitution + +The monolith grew to ~1000 lines spanning identity, enrollment, revocation, +audit, storage, hash agility, rendering, and MITM analysis. That made three +things impossible: + +1. **Independent proof.** A rollback theorem should not have to re-import + the render-swap threat model to compile. +2. **Independent evolution.** Rotating the hash profile should not reopen + the enrollment protocol. +3. **Independent reuse.** hermes-agent or an outside harness may want the + Signed-Object and Chain-Store profiles without the ceremony UI. + +Each profile below is a **decision** (an ADR): it is `Proposed`, then +`Accepted`, then `Proven`. A downstream decision **cannot be Accepted until +its dependencies are Proven** — that is the "chain of decisions" made real. + +## The dependency DAG + +Corrected 2026-07-16 per an adversarial review (OB-1): the prose had +back-edges the first diagram hid — P0's attestation and L5 lean on P4, and +P3/P5 consume P4 records. The fix is **dependency inversion**: P0 depends +only on *abstract contracts* (`AttestEvidence`, `ValidAssociationProof`) +that **P4 implements** — so the linear order below is real, not aspirational. + +``` + P1 Signed-Object (foundation: CID · canon · Sealed · allowlist) + │ + ▼ + P2 Chain-Store (causal transcript DAG · external anti-rollback anchor) + │ + ▼ + P0 Ceremony Contract ◄── THE NARROW WAIST + │ five laws · lattice · seam · gate; + │ depends on P4 only via abstract contracts + ▼ + P4 Identity Lifecycle (roles · records · quorum revocation · recovery; + │ implements P0's AttestEvidence / association proof) + ▼ + P3 Enrollment (SAS · PoP; produces P4 PinRecords) + + P5 Rendering depends on {P0, P1, P4} (effect binding · gate-signed requests) + + External fabric: agent-mesh#67 Conversation Graph — the wider causal + transcript of which P2's chain-store is the *authority projection*. +``` + +Build/prove order: **P1 → P2 → P0 → P4 → P3**, with P5 after P0/P1/P4. + +## The profiles + +| # | Profile | Owns | Depends on | Primary teeth | +|---|---|---|---|---| +| **P0** | [Ceremony Contract](ceremony-contract.md) | the five laws; the authority **product lattice**; the `DecisionSurface` seam; gate acceptance | P1, P2 | Lean (lattice + resolution) → Aeneas (kernel refines model) | +| **P1** | [Signed-Object Profile](signed-object-profile.md) | ContentId (multihash), canonical DAG-CBOR, `Sealed`, deterministic signatures, algorithm allowlist, Profile v1 pins | — | proptest round-trip + Lean canonicalization-injectivity contract | +| **P2** | [Chain-Store Profile](chain-store-profile.md) | the causal-transcript DAG, content-CID/line-CID, `Extends` partial order, external anti-rollback anchor | P1 | Lean trusted-state-machine (`untrusted_step_safe`, checkpoint monotonicity) → Aeneas | +| **P3** | [Enrollment Protocol](enrollment-protocol.md) | SAS pairing, PoP introductions, recipient-issued challenge, external anchors | P0, P1, P2 | **symbolic protocol analysis (Tamarin/ProVerif)** — freshness, MITM, unknown-key-share | +| **P4** | [Identity Lifecycle](identity-lifecycle.md) | roles & delegation, quorum revocation, break-glass & succession | P0, P2 | Lean (quorum k-of-n; non-regression of the load-bearing set) + a liveness/recovery obligation | +| **P5** | [Rendering Security](rendering-security-profile.md) | gate-signed requests, effect binding, display-from-effect, render transcript | P0 | Lean (effect-CID soundness) + a stated human-factors residual (not cryptographic) | + +## The teeth — three tiers, do not confuse them + +Correctness enforcement is layered; each tier assumes the one below and is +verified by a *different* kind of tool. Naming the boundary is the point — +a proof that silently assumes the wrong tier is exactly the "prose becomes +authority-bearing protocol" failure the two security reviews caught. + +``` +Tier 3 Kernel refinement Lean model ⟵Aeneas⟶ pure Rust kernel + (functional correctness) proves the algebra + state machine; Charon + extracts the Rust; a bridge theorem proves + the extraction refines the model. CI gate: + no Rust kernel merges unless the refinement + proof passes. (P0, P2, P4.) + +Tier 2 Protocol safety Tamarin / ProVerif symbolic models prove the + (ceremony soundness) CEREMONIES have no MITM / replay / unknown- + key-share under Dolev-Yao. Algebra proofs do + NOT cover this — a lattice can be flawless + while its handshake leaks. (P3, parts of P5.) + +Tier 1 Cryptographic primitives Ed25519 unforgeability, BLAKE3 collision + (assumed, not proven) resistance, deterministic-nonce property. + Cited to the literature; the trust base. + Rotatable via P1's profile + allowlist. + +Cross-cutting: conformance VECTORS (shared JSON, kyln round-trip pattern) + bind the four client languages (Rust/Python/Dart/TS) to ONE + observable behaviour — the teeth that keep implementations + honest where proofs stop. +``` + +**The refinement boundary (Tier 3), stated once:** the pure kernel is +`resolve`, precedence, the gate acceptance checklist, and the trusted-state +transition — no serde, no IO, no crypto impl, no UI. Crypto and hashing +enter as *abstract injective/one-way contracts* at the kernel edge (P1's +job to satisfy, the kernel's job to assume). This is what lets Aeneas run. + +## Build order (what to prove first) + +The DAG dictates it: **P1 → P2 → P0 → P4 → P3**, P5 after P0/P1/P4 (OB-1). +The provable MVP is +**P1 + P2 + P0** — the Signed-Object foundation, the anti-rollback store, +and the authority kernel with its five laws. That triple is GPT-5's #232 +"formal ceremony kernel" almost exactly; adopt it as the P0/P1/P2 slice and +graft the ceremonies (P3–P5) on once the waist is Proven. Nothing in P3–P5 +may be Accepted against an unproven waist. + +## Proof-obligation ledger (moves with the profiles) + +| PO | Profile | Statement | Tier | +|---|---|---|---| +| PO-1 | P0 | ⨅-resolution is order-independent (assoc ∘ comm ∘ idem) | 3 | +| PO-4 | P0 | authority composes by meet, never amplifies | 3 | +| PO-3 | P0 | resolve is total; headless degradation is ⊑-monotone | 3 | +| PO-1c | P1 | canonicalization is injective; verify-over-received-bytes | 3 | +| PO-8 | P1 | algorithm dispatch is allowlist-gated (no downgrade) | 3 | +| PO-2 | P2 | sub-quorum mutation is ⊑-monotone under H1 | 3 | +| PO-2a | P2 | interior deletion/replay rejected vs. a trusted head | 3 | +| PO-2c | P2 | tail truncation + fork rejected vs. the external anchor | 3 | +| PO-5 | P0/P4 | no association without pin; re-key forces re-ceremony | 3 | +| PO-2b | P4 | sub-quorum cannot shrink the load-bearing set | 3 | +| PO-R | P4 | recovery is live: a legitimate owner is never permanently locked out | 3 (liveness) | +| PO-E | P3 | enrollment has no MITM / unknown-key-share under Dolev-Yao | 2 | +| PO-F | P3 | challenge freshness: no self-issued nonce is accepted | 2 | +| PO-W | P5 | effect-CID soundness: an accepted decision's effect = the executed call | 3 | +| WF-1 | P0 | matrix decidable sans escalations (schema predicate) | vector | +| WF-2 | P1 | Memo discipline (CID/sig/parents/Sealed) | vector | + +The waist stays **five laws**; the ledger just relocates each obligation to +the profile that owns it. + +## Specification obligations — status + +From adversarial review round 6 (a fresh GPT pass, 2026-07-16), which +confirmed the split closed the prior attacks and rated architecture / +threat-honesty / separation / formal-plan all *Strong*. **All eleven are +addressed in the v0.3.0 repair cut** below (spec text changed; the *proofs* +that discharge them are the implementation phase, still held). **B/H/M** = +original severity. + +| # | Sev | Status | Where fixed | +|---|---|---|---| +| OB-1 | B | ✅ resolved | dependency inversion — P0 §3/L5 define abstract `AttestEvidence` + `ValidAssociationProof`; P4 implements. DAG corrected above (P1→P2→P0→P4→P3). | +| OB-2 | B (choice) | ✅ adopted¹ | **linear authority spine per causal thread** `(store_id, thread_id, sequence)` — P2 §1. Conversation branches; authority is a railway. (Frontier alt rejected as harder to prove.) | +| OB-3 | B | ✅ resolved | P0 §3 — one canonical challenge preimage; CAS-committed transaction (verify→presence→construct→append→advance-anchor→mint); four separate roles (authenticator ≠ DAG verifier). | +| OB-4 | B | ✅ resolved | P1 §2 — signed-bytes-in-envelope `{profile, codec, body, cid, by, sig}`; JSON/TOML are views. | +| OB-9 | B | ✅ resolved | P0 L1 — `resolve(∅,q) = ask` (piecewise, not a seed — a seed would downgrade legitimate `approve`); vocabulary glossary P0 §2.4. | +| OB-5 | H | ✅ resolved | P3 §1 — reserve→validate→**consume-last**; bind challenge object CID + recipient + role + context. | +| OB-6 | H | ✅ resolved | P1 §4·5 — universal domain-separation tuple on every signed `body`; normative `store_id` (P2 §1). | +| OB-7 | H | ✅ resolved | P4 §2 — `policy_cid == ActiveRevocationPolicy(target, observed_checkpoint, generation)`; enrollment records the exact required revocation predicate (tuple isn't totally ordered). | +| OB-8 | H | ✅ resolved | P4 §3 — PO-R stated **conditionally**; timelock-recovery veto-suppression threat answered (multi-channel ack, fail-closed on silence). | +| OB-10 | M | ✅ resolved | P5 §1 — per-class sealed resource identities (container **digest** not tag, repo commit/tree CID, …); ambient = named residual. | +| OB-11 | M | ✅ resolved | `suite.toml` compatibility manifest (below). | + +¹ OB-2's linear spine and the `attest` factorization were the two +author's-calls — **both now decided** (see OB-12/OB-15 below). + +### Review 7 — the v0.3.1 PROTOCOL FREEZE (2026-07-16) + +A protocol-freeze review named seven places implementers would otherwise +diverge. All closed in text; the *proofs / conformance vectors* that discharge +them are the (still-held) implementation phase. + +| # | Sev | Status | Where fixed | +|---|---|---|---| +| OB-12 | B | ✅ **type frozen** | P0 §2.0 — `Authority = Effect × Assurance × Scope` (componentwise meet); `ask`→`NeedsDecision` (control-flow, not authority); `deny`=⊥; **explicit signed `ceiling`**; scope is a profile-declared closed order. Resolves the `attest` factorization (4-way converged). | +| OB-13 | B | ✅ resolved | P1 §2 — ONE signed-object constructor; `sig` covers a canonical **protected tuple** (profile, codec, cid, signer, domain-sep), not bare cid; body domain tuple must equal the envelope. | +| OB-14 | B | ✅ resolved | P1 §2 / P2 §1 — genesis `STORE_ID_SELF` sentinel breaks the `store_id = CID(genesis)` fixed point. | +| OB-15 | B | ✅ **CAS frozen** | P2 §1.1 — compare-and-swap on expected head; **concurrent candidates + CAS-losers are NOT equivocation**. Roadmap: CAS → **Byzantine Vertical Paxos** (below). | +| OB-16 | B | ✅ **law corrected** | P0 L2 — upward direction is now `TrustedStructure(m(R)) = TrustedStructure(R)` (equality), not `⊆`: sub-quorum actors can't *add* a trusted issuer either (closes time-delayed privilege escalation). | +| OB-17 | H | ✅ resolved | P3/P4 — dropped "punting ≥ pinning" scalar (tuple isn't totally ordered); revocation is P4's exact policy-CID predicate; P3 now depends on P4. | +| OB-18 | H | ✅ resolved | P5 — token downgraded to attention-aid; faithfulness = **byte-compare vs a gate-produced canonical render**; **raw secrets forbidden** in any signed record (use secret-version refs / one-shot caps / keyed commitments). | + +**Exit gate (v0.3.1) status:** factorization + `ask` ✅ · ceiling + scope +order ✅ · signed-envelope grammar ✅ · genesis non-circular ✅ · append/CAS +normative ✅ · L2 forbids latent additions ✅ · P3/P4 agree ✅ · P5 token + +secrets ✅ · **conformance vectors (positive + negative) — the one +implementation-phase item, tracked with the kernel (`suite.toml` +`conformance_vectors`).** + +### Store roadmap (adopted): CAS → Byzantine Vertical Paxos + +The frozen CAS append is the **threshold-1 steady-state case** of a +vertically-reconfigurable store. **Sequencing (author-adopted):** prove the +`P1 → P2 → P0` waist on CAS first; then evolve P2 to separate a lean +steady-state protocol from a stronger **reconfiguration** mechanism (the +*wedge*: fence config → capture safe closing state → certify next config), +giving 2-full-node deployments safe failover (`f+1` steady / `2f+1` +reconfiguration) and an operation-sensitive partition-authority ceiling on the +§2.0 lattice. **Reference implementation: (Byzantine) Vertical Paxos — +Abraham & Malkhi (IBM Zurich DCCL); VP orig. Lamport-Malkhi-Zhou, PODC 2009.** +The wedge/closing-state correctness gets its own ADR + TLA+/Lean model before +it is normative; it is **not** part of the v0.3.1 freeze. + +## Suite compatibility manifest (OB-11) + +`suite.toml` names which profile versions form one compatible suite — one +atomic target for implementers, independent profile evolution preserved: + +```toml +suite = "ceremony-suite" +suite_version = "0.3.0" +[requires] +p0 = "0.2" # ceremony-contract (waist) +p1 = "1" # signed-object +p2 = "0.2" # chain-store +p3 = "0.2" # enrollment +p4 = "0.2" # identity-lifecycle +p5 = "0.2" # rendering-security +conformance_vectors = "cid:…" # populated with the kernel +``` + +## The rule underneath the whole suite + +> No authorization or claim floats free of the exact history and artifacts +> that gave it meaning. + +P1 gives things names; P2 gives history that cannot silently move; P0 makes +authority an algebra that cannot amplify; P3/P4 bind identity to ceremony; +P5 binds what-was-approved to what-executes. Each is a telescope, not the +sky — the thing being observed is a human's authority, faithfully carried. diff --git a/docs/spec/ceremony-contract.md b/docs/spec/ceremony-contract.md new file mode 100644 index 0000000..32a9d05 --- /dev/null +++ b/docs/spec/ceremony-contract.md @@ -0,0 +1,366 @@ +# P0 — The Ceremony Contract (the narrow waist) + +**Status:** DRAFT 0.3.1 — PROTOCOL FREEZE (2026-07-16). Authority type frozen +(`Effect × Assurance × Scope`; `ask`→`NeedsDecision`; explicit ceiling — the +`attest` factorization, decided). Partitioned from the v0.1.x +monolith into the [Ceremony Suite](README.md), then repaired against review +round 6 (all eleven obligations closed in text — see README). This document +is the **waist**: the five laws, the authority algebra, and the decision +seam. Everything mechanical moved to a profile (P1–P5); this doc *references* +them and states the invariants they must satisfy. +**Depends on:** P1 (Signed-Object), P2 (Chain-Store); P4 only via the +abstract contracts it defines (`AttestEvidence`, `ValidAssociationProof`) — +no back-edge (OB-1). +**Depended on by:** P4, P3, P5. +**Teeth:** Lean proof of the lattice laws + resolution, refined to the pure +Rust kernel by Aeneas (Tier 3). See the review history and adjudications on +[#229](https://github.com/Gilamonster-Foundation/agent-bridle/pull/229); +positioning on [#225](https://github.com/Gilamonster-Foundation/agent-bridle/issues/225). + +**Scope:** the contract between agent-* libraries (decision *semantics*) and +harnesses (*rendering*). A harness can comply without depending on any +bridle crate; `agent-bridle` is the reference implementation. + +## 1. The seam + +Libraries define the decision **space**; consumers define the **layout**. A +library crate MUST NOT contain rendering or interactive prompting. A +consumer binds a `DecisionSurface`; with none bound, the laws fail closed +(L3). + +``` + agent-* libraries consumer (harness) +┌─────────────────────┐ ┌──────────────────────────┐ +│ decision kernel │ struct │ DecisionSurface impl: │ +│ (pure; provable) │──────► │ newt: matrix + audit │ +│ resolve · meet · │ │ hermes: flat list │ +│ gate · pin store │ ◄──────│ daemon: policy files │ +└─────────────────────┘Decision│ phone: GUI sheet │ + └──────────────────────────┘ +``` + +```rust +#[async_trait] +pub trait DecisionSurface { + async fn decide(&self, req: PermissionRequest) -> Decision; +} +``` + +Policy files (#220) are the headless implementation of this trait. + +## 2. Wire objects (the seam's vocabulary) + +All are Memo-descendants (P1 §3). Full field-level definitions of the +identity/enrollment/store records live in their owning profiles; the three +objects the *seam* itself trades are here. + +### 2.0 The Authority type (FROZEN — OB-12) + +Authority is a **product meet-lattice of three independent axes**, with +componentwise attenuation: + +``` +Authority = Effect × Assurance × Scope + Effect : deny ⊏ allow (deny = ⊥) + Assurance : none ⊏ presence ⊏ hardware (the old `attest` lives here) + Scope : once ⊏ session ⊏ durable (open-EXTENSIBLE, but see below) + (e₁,a₁,s₁) ⊓ (e₂,a₂,s₂) = (e₁⊓e₂, a₁⊓a₂, s₁⊓s₂) + ⊥ = (deny, none, once) ⊤ = (allow, hardware, durable) +``` + +`deny` is the bottom of `Effect`; there is exactly one denied authority +(`⊥`), never several semantically-equal "denied authorities". The former +`attest` disposition is **`Assurance = presence`** (or `hardware`); it is no +longer a verb, so it composes with any Effect/Scope. + +**`ask` is NOT an authority level — it is a control-flow result (OB-1/#1):** + +``` +Resolution = NeedsDecision (was `ask`: must interact) + | Decided(Authority) +``` + +`NeedsDecision` means "no rule settled this; a surface must decide." It has +no place in the lattice; the gate never *grants* `NeedsDecision`. Headless, +it degrades to `deny` (L3). + +**Scope is a *declared, closed-per-profile* order, not arbitrary strings +(#1).** A profile MUST publish its scope set and their total order + meet +(v1: `once ⊏ session ⊏ durable`); an implementation rejects a scope outside +its profile. "Open vocabulary" means *a profile may extend the set*, never +*any string compares somehow*. + +### 2.1 PermissionRequest + +```json +{ "v": 1, "subject": "b3:…", + "action": { "class": "exec", "display": "run_command: cd ", + "effect": "cid:…" }, // canonical resolved call — P5 + "violation": "outside-granted-allowlist", + "ceiling": { "effect": "allow", "assurance": "presence", "scope": "session" }, + "matrix": { … }, "context": { "session": "…", "generation": 41 }, + "by": "b3:…", "sig": "…" } // gate signature — required remote (P5) +``` + +**`ceiling` is an explicit, signed field (#1)** — the maximum Authority this +request may resolve to. No grant may exceed it (L4). It is set by the gate +from policy at issue time; the gate re-derives and re-checks it before +minting (never trusts a surface-supplied ceiling). `action.effect` binds the +signature to *what executes* (P5). + +### 2.2 DecisionMatrix + +```json +{ "effects": ["allow", "deny"], + "assurances": ["none", "presence"], + "scopes": ["once", "session"], + "default": { "effect": "allow", "assurance": "none", "scope": "once" }, + "escalations": ["audit"] } +``` + +The decision *space* over the three axes; nothing encodes layout. A surface +offers points of `effects × assurances × scopes` bounded by `ceiling`. +Presence-required is `assurance ∈ {presence, hardware}` (§3). `default` is +the administrator/packager **opinion surface** (`rm -rf` ships +`{deny, none, once}`), never an auto-grant. Scopes are drawn from the +profile's declared set (§2.0). + +**WF-1 (well-formedness, not a law):** every matrix MUST be decidable with +all escalations unrendered — the axis products are non-empty and sufficient. + +### 2.3 Decision + gate acceptance + +```json +{ "v": 1, "request": "cid:…", + "grant": { "effect": "allow", "assurance": "presence", "scope": "once", + "discharge": { "challenge": "cid:…", "attempt": "…" } }, // if assurance>none + "by": "b3:…", "sig": "…" } +{ "v": 1, "request": "cid:…", "escalate": "audit", "by": "b3:…", "sig": "…" } +``` + +`escalate` carries **⊥ authority** (L4); exactly one of `grant`/`escalate`. +A `grant` is a point in the Authority lattice. **Gate acceptance is a +checklist of MUSTs — the client is never trusted:** + +1. `request` = the content-CID of the request the gate itself issued; +2. each axis of `grant` is a member of the matrix's declared axis sets; +3. `grant ⊑ ceiling` (L4, componentwise) — no axis exceeds the request ceiling; +4. the executable effect recomputes equal to `action.effect` (P5); +5. if `grant.assurance > none`, the discharge verifies **and** its history + witness passes the forward-only ratchet (§3). + +A surface violating any is refused — the wire *enforces* L4. + +### 2.4 Vocabulary (one word, one job — OB-9/OB-12) + +| Term | Register | Meaning | +|---|---|---| +| `Effect` (`deny`/`allow`) | authority axis | *what* is permitted; `deny = ⊥` | +| `Assurance` (`none`/`presence`/`hardware`) | authority axis | *how strongly proven present*; the old `attest` = `presence` | +| `Scope` (`once`/`session`/`durable`) | authority axis | *how long* the grant covers (profile-declared order) | +| `NeedsDecision` | **control-flow result**, not authority | "no rule settled it → interact"; headless ↦ `deny` (L3); never granted | +| `escalate` | **Decision action**, not authority | navigation to a richer surface; `authority(escalate) = ⊥` | + +There is no `ask` verdict and no `attest` verb any more: `ask` became the +control-flow `NeedsDecision`; `attest` became `Assurance = presence`. + +## 3. Presence discharge + the forward-only ratchet + +A grant with **`Assurance > none`** (formerly "attest") is **inert until a +presence proof is verified**, and the proof *also witnesses a non-regressing +history*: the same finger-press attests "I approved R" **and** "the world had +not regressed when I did." (`presence` = a WebAuthn/FIDO2 user-presence +discharge; `hardware` additionally requires a bound hardware/measurement +attestation, P5 §4.1.) + +**Four roles, deliberately separate (OB-3).** The WebAuthn authenticator +does not understand a Merkle DAG — it signs over a client-data hash. So do +not say "the hardware witnessed the chain." The roles are: + +| Role | Does | +|---|---| +| **Witness-verifier** | holds the P2 §4 protected checkpoint; verifies DAG extension; **constructs the challenge preimage** | +| **Authenticator** (WebAuthn/FIDO2) | proves user presence/verification over that challenge — nothing more | +| **Surface identity** | signs the resulting `AttestEvidence` record | +| **Gate** | appends, advances the anchor, then activates authority | + +**One canonical challenge preimage** — every field the attestation binds, +domain-separated (P1 §), so nothing is left to prose: +``` +challenge = H("agent-bridle/attest/v1", + store_id, thread_id, request_cid, decision_cid, + previous_checkpoint, observed_checkpoint, generation, nonce) +``` + +**The commit is transactional (compare-and-swap, OB-3).** A crash or +rollback must never leave "authority active but attestation not durable" or +"attestation appended but anchor not advanced": +``` +1. witness-verifier: observed_checkpoint Extends protected_checkpoint (else HALT) +2. authenticator: presence proof over the canonical challenge +3. surface: construct AttestEvidence +4. append it → post_attestation_head +5. CAS-advance the protected anchor: protected := post_attestation_head +6. only now mint/activate authority +``` +Steps 4–6 are one atomic transition (CAS on the anchor); a recoverable +two-phase form is permitted. Rollback *or* fork at step 1 → `CHAIN HISTORY +REGRESSION` → halt + escalate (a fork is P2 proof-of-misbehavior, never a +branch to silently adopt). Checked **per causal thread** (P2 `thread_id`), +so concurrent threads never false-trip; generation (total order) and DAG +ancestry (partial order) must *both* advance. + +**P0 depends only on an abstract evidence contract (OB-1)** — not on P4's +concrete record — so the waist has no back-edge into P4: +```rust +trait AttestEvidence { + fn request(&self) -> ContentId; + fn decision(&self) -> ContentId; + fn previous_checkpoint(&self) -> Checkpoint; + fn observed_checkpoint(&self) -> Checkpoint; + fn presence_proof(&self) -> PresenceProof; +} +``` +P4 supplies `AttestationRecord` as the concrete implementation. Payoff of +the whole ratchet: **every ordinary approval is a free freshness +checkpoint.** Not a new law — L2·H1's anchor applied at ceremony time. + +## 4. The Laws (normative — the whole waist) + +Five laws. Nothing enters this section without a proof obligation (§5); +everything else is mechanism (a profile) or well-formedness. + +### L1 — Resolution is a meet +Authority is the **product meet-lattice** `Effect × Assurance × Scope` (§2.0); +`⊓` is componentwise; `⊥ = (deny,none,once)`. Resolution meets the matching +rules, **with the no-match case an explicit control-flow result** so it is +total *and* fail-closed (OB-9): +``` +resolve(R, q) = Decided( ⨅ { authority(r) | r ∈ R, r matches q } ) if some rule matches + = NeedsDecision if none matches +``` +The explicit `NeedsDecision` default is load-bearing: the empty meet's +identity is `⊤ = (allow,hardware,durable)`, so *without this clause an +unmatched request would fail OPEN*. `NeedsDecision` is not an authority — it +routes to a surface (headless ↦ `deny`, L3). Componentwise `⊓` is +associative, commutative, idempotent ⇒ resolution is independent of +rule/file/load order; no ordering attack. **PO-1** (includes +`resolve(∅,q) = NeedsDecision`, i.e. no fail-open; product-of-lattices is a +lattice, so the meet laws lift componentwise). + +### L2 — Tamper-boundedness +For any mutation `m` by a party holding **fewer than quorum(target)** keys: +``` +resolve(m(R), q) ⊑ resolve(R, q) (no widening, any query) +TrustedStructure(m(R)) = TrustedStructure(R) (no authority-generating change) +``` +Two directions, one law. **Downward:** sub-quorum actors only narrow +authority; forged loosening entries drop at load (fail-closed). **Structural +(strengthened, OB-16/#5):** the *authority-generating structure* — pinned +principals, enrolled devices, trusted issuers, blessed anchors, delegation +edges — must be **unchanged**, not merely un-shrunk. The old `⊆` only forbade +*removal*; it permitted a sub-quorum actor to *add* a trusted issuer that +widens no query today but **issues authority later** — a time-delayed +privilege escalation that passes the per-query monotonicity test. Equality +closes it: any add *or* remove of authority-generating structure is a +quorum-gated operation (P4). Reversible authority *narrowing* (deny-spam) +stays a nuisance; **irreversible narrowing (revoking an identity) and any +structural change require quorum**, because a fail-closed system's failure +mode is an adversary who can *force* closure. Availability is a security +property. +**H1 (append-only-verifiability + monotone freshness)** is discharged *by +mechanism*, split across P2: interior integrity by the chain (**PO-2a**), +tail/fork by the external anchor (**PO-2c**), revocation-quorum by P4 +(**PO-2b**). **PO-2** proves ⊑-monotony under H1. (H1's chain-alone form was +over-claimed in v0.1.x and corrected — see README teeth Tier 3.) + +### L3 — Fail-closed totality +`resolve` is total; no input reaches "undefined permission." The +non-authority result is `NeedsDecision`; absent a bound surface it degrades +to `deny` (`⊥`-Effect), and any un-discharged `Assurance > none` grant also +degrades to `deny` (degradation is ⊑-monotone). **PO-3.** + +### L4 — Attenuation +`effective = granted ⊓ required`; `granted ⊑ ceiling` (componentwise, §2.0); +`authority(escalate) = ⊥`. Authority composes by componentwise meet, never +amplifies on any axis (property-tested upstream as `meet_never_amplifies`, +lifted to the product). **PO-4.** + +### L5 — The ceremony gate +`association(peer) ⇒ pinned(fingerprint(peer))`. `fingerprint = H(pubkey)` +is self-certifying (P1) — re-key ⇒ new fingerprint ⇒ unpinned ⇒ full +re-ceremony; no silent identity swap is expressible. Pinned is **transitive +through certification** — but the waist states this over an **abstract +predicate** (OB-1), not P4's concrete cert-chain, so L5 has no back-edge: +``` +pinned(fp) ⇔ fp ∈ PinSet ∨ ValidAssociationProof(fp, PinSet) +``` +`ValidAssociationProof` is an abstract contract (there exists a +PoP-at-every-link chain `fp →* root ∈ PinSet`); **P4 proves its cert-chains +implement it** (shipped as mesh `CertChain::verify` + PoP, #39/#40). **PO-5** +(incl. chain soundness) is proved by P4 against this predicate. + +## 5. Proof-obligation ledger (owned here; full suite in README) + +| PO | Law | Statement | Tier | +|---|---|---|---| +| PO-1 | L1 | ⨅-resolution order-independent | 3 | +| PO-2 | L2 | sub-quorum mutation ⊑-monotone under H1 | 3 | +| PO-3 | L3 | totality + monotone headless degradation | 3 | +| PO-4 | L4 | meet never amplifies | 3 | +| PO-5 | L5 | no association without pin; re-key forces re-ceremony | 3 | + +Pilot proofs: PO-1, PO-2. The kernel is pure `resolve` + precedence + the +gate checklist + the P2 trusted-state transition — no serde/IO/crypto/UI; +crypto enters as P1's abstract contracts. Conformance **vectors** bind the +four client languages to one observable behaviour. + +## 6. Cross-cutting: the MITM ledger + +"No MITM hole anywhere" is a claim to *enumerate*. Each row's closure lives +in the cited profile; the unifying rule is **the authenticated thing is +always the key, never the channel.** + +| Channel | Attack | Closure (profile) | +|---|---|---| +| First contact | TOFU key swap | L5 ceremony / chain-to-pinned-principal (P3) | +| First contact | intro replay / unknown-key-share | recipient-issued challenge + PoP (P3) | +| Enrollment | relay + key substitution | commit-reveal SAS over long-term keys (P3) | +| Post-pin transport | path impersonation | dial-by-pubkey; paths are hints (mesh) | +| Delegation | rogue delegated agent | chains verify to a pinned principal (P4) | +| Remote surface | render-swap | `Decision.request` CID binding (P5) | +| Remote surface | phishing canvas | gate-signed requests, verified before render (P5) | +| Store sync | rollback / truncation / fork | external anti-rollback anchor (P2 §4) | +| Anchor channel | fake-root vouch | blessed anchors, k-of-n, never alone (P4) | +| The human | prompt fatigue | `attest` for high ceilings; UI guidance (residual) | + +## 7. Governance — law minimalism + +A good system has only the laws it absolutely needs. **Nothing enters §4 +without a proof obligation; everything else is a profile or a +well-formedness predicate.** The count history: six → five (L6 → WF-1); +then held at five through the revocation-DoS absorption (L2 upward), the +Memo/multihash discipline (WF-2/P1), two adversarial security reviews +(rounds 4–5), the forward-only ratchet, and the **v0.3.1 protocol freeze** +(review 7): seven findings closed as *type freeze* (OB-12: `Effect × +Assurance × Scope`, `ask`→control-flow, explicit ceiling), *law correction* +(OB-16: L2 upward now **equality** over authority-generating structure, not +`⊆` — closing latent-injection escalation), and *mechanism/wire discipline* +(OB-13 signed grammar, OB-14 genesis, OB-15 CAS append, OB-17 P3/P4 +revocation, OB-18 P5 token+secrets). **Still five laws** — the frozen product +authority type is a *carrier* change, not a new law; L1/L4 lift componentwise. +**Next candidate:** L1+L4 unify as one "authority composes by meet" law on +the product carrier — five → four if the Lean formulation collapses them. + +The algebra decides the count; ambition doesn't. + +## Relations +- Suite index: [README.md](README.md) +- Profiles: P1 [signed-object](signed-object-profile.md) · P2 + [chain-store](chain-store-profile.md) · P3 + [enrollment](enrollment-protocol.md) · P4 + [identity-lifecycle](identity-lifecycle.md) · P5 + [rendering](rendering-security-profile.md) +- #220 verdict/policy TOML · #231 `passkey`→`attest` rename · GPT-5 PR #232 + formal kernel · agent-mesh#67 Conversation Graph · + `docs/decisions/floating_identity.md` (law 5 = L5; law 4 = the graph) diff --git a/docs/spec/chain-store-profile.md b/docs/spec/chain-store-profile.md new file mode 100644 index 0000000..33c94eb --- /dev/null +++ b/docs/spec/chain-store-profile.md @@ -0,0 +1,194 @@ +# P2 — Chain-Store Profile + +**Layer:** 1. **Depends on:** P1 (Signed-Object). +**Depended on by:** P0 (L2), P3, P4, P5. +**Status:** DRAFT. **Teeth:** a Lean trusted-state-machine +(`untrusted_step_safe`, checkpoint monotonicity) refined to Rust by Aeneas +(Tier 3) — this is the heart of GPT-5 #232's §8–9. +**Owns:** durable, tamper-evident, **rollback-resistant** history — and the +honest statement of what the hash chain does and does not buy. + +## 1. Conversation is a jungle; authority is a railway (OB-2) + +Records are `MerkleNode` (P1). The wider **Conversation Graph** +(agent-mesh#67) is a genuine Merkle DAG — branches (parallel agents) and +merges (accepted synthesis) are first-class. But a branching DAG **cannot** +be checkpointed by a scalar `(length, head)`: two heads at equal depth can +be *legitimate* concurrent descendants, so "different heads at the same +length ⇒ equivocation" is false for a DAG. + +The resolution: **the authority projection is a linear spine per causal +thread.** The conversation may branch and merge freely; branches must +**merge before producing the next authority record**, so the sequence of +authority records along one thread is totally ordered. + +```rust +struct AuthorityCheckpoint { // the protected anchor state (P2 §4) + store_id: StoreId, // normative, cryptographically bound (OB-6) + thread_id: ThreadId, // one causal authority thread + sequence: u64, // dense per (store_id, thread_id) + head: LineCid, +} +``` + +Normative definitions: +- **`store_id`** — a content-addressed identifier of the store's genesis + (its root record's CID); every signed record's domain tuple binds it + (P1 §4·5), so a record cannot be replayed into a different store. Genesis + is non-circular via the `STORE_ID_SELF` sentinel (P1 §2, OB-14): the + genesis body binds `0x00`, and its own cid *becomes* the `store_id` every + later record binds. +- **`thread_id`** — the identifier of one authority thread within a store; a + causal thread is the totally-ordered sequence of authority records a + single principal-scope advances. A thread MAY be forked (declared) and + merged (a record naming multiple thread parents), but **within a thread, + `sequence n` has exactly one accepted successor at `n+1`.** +- **`length`/`sequence`** — the dense per-thread record count, *not* + longest-path depth. + +This chain-store is the authority projection of the Conversation Graph — +same `MerkleNode` structure, payload `T` = authority records here, +conversation records there. Deliberately *not* a blockchain: no mining, +tokens, leader election, or global total order. + +## 1.1 Append arbitration (OB-15/#4) + +**FROZEN for v0.3.1 — compare-and-swap on the expected head** (author's +decision). `Append(expected_head, next)` commits `next` iff the thread's head +still equals `expected_head`; a loser **retries**. Single-writer/optimistic; +the simplest model that closes the honest-race hole the review flagged. + +**Refined equivocation (this part is load-bearing regardless of the append +model):** a concurrent **candidate** record is NORMAL, and a **CAS-loser** +(one that lost the race to commit a parent) is **benign** — never evidence of +misbehavior. Equivocation is *two records both **committed** at the same +`(store_id, thread_id, sequence)` with different CIDs* — a genuine +double-commit / fork, not a race a writer lost. An honest device that reads a +head, proposes a successor, and loses the CAS is retrying, not attacking. + +> **Roadmap: CAS now → Byzantine Vertical Paxos next (adopted sequencing).** +> CAS is the threshold-1 steady-state case of a **vertically-reconfigurable** +> store: after the P1/P2/P0 waist is proven on CAS, P2 evolves to separate a +> lean *steady-state* protocol from a stronger *reconfiguration* mechanism — +> the **wedge**: fence the active configuration, capture a safe *closing +> state* (preserving acknowledged-but-partial commands), certify the next +> configuration, resume. This makes concurrent candidates normal, gives a +> 2-full-node deployment safe failover via a reconfiguration participant +> (`f+1` steady / `2f+1` reconfiguration), and makes the partition-authority +> ceiling operation-sensitive on the §2.0 lattice. Key-custody stays a +> *separate* threshold. **Reference implementation: (Byzantine) Vertical +> Paxos — Abraham & Malkhi, IBM Zurich DCCL; VP orig. Lamport-Malkhi-Zhou, +> PODC 2009.** The wedge/closing-state correctness gets its own ADR + TLA+/Lean +> model before it is normative — it is *not* part of the v0.3.1 freeze. + +The forward-only ratchet's "extends" means: the presented committed head is a +forward extension of the protected one on the same `(store_id, thread_id)` +spine, `sequence` strictly greater — never a sibling. + +## 2. Two CIDs per record + +``` +c_i = H(canon(record_i ∖ sig)) content-CID (what is signed) +s_i = Sign(k, c_i) the signature +line_i = record_i ∪ { sig: s_i } the full at-rest line +ℓ_i = H(canon(line_i)) line-CID (what parents reference) +parents(record_{i+1}) ∋ ℓ_i descendants commit to content AND sig +``` + +Parents reference the **line-CID** — the full predecessor *including its +signature* — so stripping or swapping a historical signature breaks the +chain as surely as editing content. + +**At rest:** JSONL as a lossless line-oriented view of the canonical +DAG-CBOR records — one `line_i` per line, human-auditable, no comment +affordances to make canonicalization ambiguous. CIDs/sigs are always over +the canonical form, never the view. + +## 3. What the chain buys — and what it does not + +**Interior integrity (PO-2a).** Editing or removing an *interior* record +orphans every descendant's parent link — it verify-fails loudly **against a +head the verifier already trusts.** This extends detection to +{add, delete, reorder} of the interior and retires the flat-file +known-limit (policy.rs #226). + +**What the chain alone does NOT do (finding #1).** Verification is always +*relative to a head*. An attacker who also controls the head can truncate +the tail, or present a wholly older / forked-but-internally-valid log; the +surviving prefix verifies and nothing is orphaned. This is the established +limit of every hash-chained log — Schneier-Kelsey (1999), FssAgg (eprint +2008/185), and the reason Certificate Transparency needs gossiped Signed +Tree Heads (RFC 6962). **Tail and fork integrity require §4's external +anchor, not the chain.** An anti-rollback claim resting on an in-chain +record is circular — it rolls back with the log it certifies. + +## 4. The anti-rollback anchor (external, load-bearing for L2·H1) + +Closing tail-and-fork requires state the attacker does not control. Three +canonical layers, ascending assurance: + +1. **Independently-protected monotonic head (REQUIRED).** Each participant + remembers — in storage *separate from the log* — the highest + `AuthorityCheckpoint` `(store_id, thread_id, sequence, head)` it has + accepted per thread (§1), and MUST reject any presented head that is not + a forward extension of the *same spine* — never a lower `sequence`, a + different store, or a sibling (TUF: + *"clients MUST NOT replace metadata with a version less than the one + currently trusted"*; RFC 6962 monotonicity). Defeats truncation and + rollback for that participant. **Where it lives is normative** (§6): + device keystore / hardware monotonic counter (TPM) / witness quorum / + separately-protected checkpoint. *"On disk beside the log" does NOT + qualify.* +2. **Witness cosigning (RECOMMENDED for shared stores).** The head is + periodically countersigned by witnesses (the `AuditRecord`s of P4/P0, + **exported off-chain**). A participant accepts a head only with a witness + cosignature no older than its freshness policy (CT gossip / STH). Defeats + *secret* equivocation: to fool a victim the attacker must fork the + witnesses too. +3. **Fork = proof of misbehavior (REQUIRED) — at the CERTIFIED layer only + (OB-15).** Two conflicting *quorum-certified* heads for the same + `(store_id, thread_id, config_epoch)`, or one voter's conflicting + certification votes, are incontestable evidence (§1.1; branching-safe + restatement of RFC 6962). Implementations MUST halt authority minting and + escalate — never silently pick one. **Concurrent Candidates and + CAS-losers are NOT forks** — only the certified frontier can equivocate. + +For a solo user (P3's n=2 world) the monotonic head lives on each enrolled +device and each device is the other's witness — the same k-of-n substrate +as revocation, reused. A quorum/witness set is the enterprise instance of +the identical mechanism. **Nothing here trusts the storage medium**; the +anchor is trusted state a participant carries into each verification, +exactly as `pinned` is. + +## 5. The trusted state machine (the Lean model) + +The kernel over this store is a state machine with `trustedHead: +Checkpoint` outside the store. Transitions: + +- **untrusted step** (anything an attacker with disk/network but no keys + can do): MUST NOT widen authority, add/remove trusted identities, or + rewrite the checkpoint — `untrusted_step_safe`. +- **sync/reload**: MAY advance the checkpoint only when the candidate + `Extends` the current one; MUST reject a strict ancestor or unrelated + fork. + +Theorems (Tier 3): accepted checkpoints are monotonic under `Extends`; a +strict ancestor is rejected; rollback detection is conditional on the +checkpoint staying outside the attacker-controlled store. + +## 6. Proof obligations + +| PO | Statement | Tier | +|---|---|---| +| PO-2a | interior deletion/replay rejected vs. a trusted head | 3 | +| PO-2c | tail truncation + fork rejected vs. the external anchor (not merely detected later) | 3 | +| — | (`untrusted_step_safe`; checkpoint monotonicity under `Extends`) | 3 | + +PO-2 (⊑-monotony under H1) and PO-2b (load-bearing set) live in P0/P4 but +*depend on* this profile discharging H1's rollback half. + +## Relations +- P1 (Signed-Object) — CIDs, canonical form, deterministic sig +- agent-mesh#67 — the Conversation Graph this projects from +- GPT-5 PR #232 §8–9 — the Lean trusted-state-machine formulation +- RFC 6962, TUF, Schneier-Kelsey, FssAgg (eprint 2008/185) — the canon diff --git a/docs/spec/enrollment-protocol.md b/docs/spec/enrollment-protocol.md new file mode 100644 index 0000000..216d034 --- /dev/null +++ b/docs/spec/enrollment-protocol.md @@ -0,0 +1,121 @@ +# P3 — Enrollment Protocol + +**Layer:** 2. **Depends on:** P0 (L5), P1, P2, **P4** (it produces P4 +`PinRecord`s and its revocation predicate is P4's — OB-17). +**Status:** DRAFT. **Teeth:** this profile is a **protocol**, not an +algebra — its correctness is *symbolic protocol analysis* (Tamarin / +ProVerif under Dolev-Yao), **Tier 2**, not Lean/Aeneas. A flawless lattice +can sit behind a leaky handshake; this is where that leak is proven absent. +**Owns:** how a key first joins — introductions, SAS pairing, and the +blessing of external corroboration surfaces. + +## 1. Introduction — first contact is challenge-response + +Freshness comes from the **recipient**, never the introducer: a self-chosen +nonce in a self-signed object is byte-for-byte replayable. + +**Message 1 — the recipient issues a challenge it will remember:** +```json +{ "v": 1, "challenge": "…", "issued_by": "b3:…", + "for_generation": 41, "expires_at_generation": 42 } +``` +**Message 2 — the introducer answers, binding that challenge:** +```json +{ "v": 1, "fingerprint": "b3:…", "pubkey": "ed25519:…", + "channel": "mdns | dial-back | relay | manual | qr", + "proposed_caveats": [ … ], "observed": { "addr_candidates": [ … ] }, + "answers": "…", "transcript": "cid:…", "sig": "…" } +``` +On receipt of message 2, **before any surface renders it**, validate +*first* and **consume last** — an early consume lets an unauthenticated +attacker submit garbage referencing a live challenge and *burn it* before +the signature is checked (OB-5). The order is `reserve → validate → +commit-consume`: +1. `answers` MUST reference a challenge *this recipient issued, unconsumed, + unexpired*, and bind the **challenge object CID** (not merely a nonce), + its intended recipient, protocol role, and store/principal context — + **reserve** it (do not yet consume); +2. the fingerprint's hash algorithm MUST be in the P1 allowlist **before + hashing**, then the fingerprint MUST equal that algorithm's multihash + name of `pubkey` (self-certification, checked by the library not the + human); +3. `sig` MUST verify under `pubkey` over message 2 incl. `answers` and + `transcript` — **proof of possession**, transcript-bound; +4. **only now consume** the challenge (commit). A failed step 2/3 releases + the reservation, so a forged message cannot burn a live challenge. +Replay-state lives with the challenger (unknown-key-share closure; +station-to-station). + +## 2. SAS pairing (enrolling your own devices/surfaces) + +How a new device — possibly no compute beyond key storage and a screen — +gets its keypair pinned under a principal. A naive "new device shows a +phrase, trusted device sends it back" is MITM-relayable. The sound +construction (Bluetooth numeric comparison / ZRTP): + +1. both devices **commit** to nonces before revealing; +2. both **derive** the SAS from the *entire transcript* — commitments, + reveals, **and the long-term public keys being enrolled**. This last is + not optional: an SAS over only ephemeral material lets a MITM relay the + handshake while substituting the long-term keys (key-substitution). The + SAS must checksum *what is being pinned*, not the channel; +3. **a human compares the SAS on both screens** — a low-bandwidth + *authenticated* channel the network MITM is not on. It is **not + unspoofable**: it has a measurable error probability (the SAS entropy) + and human-factors assumptions (humans skim). The phrase is a checksum, + not a secret. + +Commit-before-reveal forces the MITM to *guess* the SAS in advance; +`xxx-000` ≈ 1-in-46k per round. Paranoia is a parameter: +``` +strength(enrollment) = (SAS entropy × rounds, distinct witnesses, presence) +``` +Minima are set **by caveat ceiling**: a broad ceiling demands more rounds, +≥ 2 previously-secured witnessing surfaces, and a hardware presence +discharge (`attest`). Witnesses buy more than rounds — rounds shrink the +guess probability; independent witnesses multiply the channels an attacker +must own *simultaneously*. The completed enrollment is a `PinRecord` (P4) +whose payload carries the ceremony parameters. + +**Revocation is an exact predicate, not a scale (OB-17/#6).** An earlier +draft said "punting ≥ pinning" — revocation graded on the enrollment-strength +scale. That contradicts P4, and rightly: the strength tuple `(SAS entropy × +rounds, witnesses, presence)` is **not totally ordered**, so "≥" is +undefined. The normative rule is P4's: **each `PinRecord` names, at enrollment +time, the exact `RevocationPolicy` CID required to later punt that identity**, +and revocation compares against *that* recorded predicate. Enrollment's job +here is only to *record* the required policy CID in the pin; P4 owns its +evaluation. + +## 3. External anchors (corroboration, never the root) + +A principal root is **self-sovereign**. Externally published keys — GitHub +(`github.com/.keys`), DNS, an org CA, a prior device — are **candidate +corroboration channels**: independent witnesses that the root you pin +belongs to the human you think it does. No anchor is load-bearing (floating- +identity law 1): GitHub corroborates the root, never *is* it. A user with no +GitHub enrolls by ceremony alone with zero degradation. + +**Anchors are blessed, then participate.** Any public-key display surface +qualifies *once the key owner blesses it* — an `AnchorRecord` (principal- +signed binding of channel + location + displayed key) appended to the +chain-store. Unblessed anchors are ignored; a blessed one may *participate* +as a signing/corroboration surface (a GitHub-key signature counting as one +enrollment witness). Blessings revoke like any load-bearing identity (P4 +quorum) — a captured anchor is cut loose and `n` just shrank by one. + +## 4. Proof obligations (Tier 2 — symbolic) + +| PO | Statement | Tool | +|---|---|---| +| PO-E | enrollment has no MITM / unknown-key-share under Dolev-Yao | Tamarin/ProVerif | +| PO-F | challenge freshness: no self-issued or replayed nonce is accepted | Tamarin/ProVerif | +| PO-S | SAS guess advantage ≤ (entropy, rounds, witnesses) bound | analysis + vectors | + +The introduction/pin *outcome* records are P1/P4 objects and inherit their +Tier-3 obligations; the *handshake* is what this profile proves. + +## Relations +- P0 L5 (the ceremony gate this satisfies) · P1 (allowlist, PoP sig) · P2 + (the store the PinRecord lands in) · P4 (PinRecord, RevocationRecord, + AnchorRecord definitions) · agent-mesh#65/#66 (mesh-side structs) diff --git a/docs/spec/identity-lifecycle.md b/docs/spec/identity-lifecycle.md new file mode 100644 index 0000000..1b72cb4 --- /dev/null +++ b/docs/spec/identity-lifecycle.md @@ -0,0 +1,154 @@ +# P4 — Identity Lifecycle + +**Layer:** 2. **Depends on:** P1 (Signed-Object), P2 (chain-store), P0 +(L2, L5). **Implements** P0's abstract contracts `AttestEvidence` and +`ValidAssociationProof` (OB-1) — the waist stays acyclic because *P4 +depends on P0*, never the reverse. +**Status:** DRAFT. **Teeth:** Lean (quorum k-of-n soundness; non-regression +of the load-bearing set, PO-2b) + a **conditional liveness** obligation +(PO-R, §3). Tier 3. +**Owns:** roles and delegation, the durable identity records, quorum +revocation, and — required, not optional — break-glass and succession. + +## 1. Roles (one identity model, four roles) + +Every participant is a fingerprint; roles differ only in *what they sign*: + +| Role | Holds | Signs | +|---|---|---| +| **Principal** | root keypair (vault/hardware) | issuance of agent/surface certs; durable loosening entries | +| **Agent** | keypair chained to a principal | envelopes, requests, delegations | +| **Surface** | keypair chained to a principal — possibly nothing else (a no-compute device is keypair + renderer) | its `Decision`s and `AttestationRecord`s | +| **Gate** | the enforcement identity (usually = its agent) | chain-store appends | + +A monolith (newt carrying bridle + mesh in-process) is the **degenerate +case**: one fingerprint, all roles. Delegation is the roles splitting into +separate keypairs. In-process surfaces MAY omit signing decisions; **remote +surfaces MUST sign** (attributable provenance). + +**Delegation** (agent → agent): both endpoints present chains to a **common +pinned principal** (L5). The root key is involved at **issuance, not +per-delegation** — headless fleets verify chains offline while the root +stays in hardware; revocation is a generation bump. Cross-principal +delegation is two principals pinning each other's roots (L5, one level up). +Shipped as mesh `CertChain::verify` + PoP-to-certify (#39/#40). + +## 2. Durable records + +### PinRecord / GrantRecord +```json +{ "parents": ["cid:…"], // line-CIDs (P2); ⌀ only for genesis + "payload": { "v": 1, "fingerprint": "b3:…", "pubkey": "ed25519:…", + "channel": "qr", "caveats": [ … ], // the granted meet + "decision": { "grant": { "verb": "pin", "scope": "always" } }, + "presence": { "kind": "passkey", "discharge": "…" }, // §5 + "granted_at": "…" }, // provenance, not validity + "sig": "ed25519:…" } +``` +A pin is created only by a bound-surface `grant` or a pre-pinned policy +entry (a signed loosening entry, L2). + +### AuditRecord / AttestationRecord +An **AuditRecord** witnesses the chain head (`witnessed_head`, `fingerprint`, +`presence`); exported off-chain it becomes a P2 §4 anchor — in-chain alone +it anchors nothing. An **AttestationRecord** is the concrete implementation +of P0's `AttestEvidence` contract (OB-1) — its authorization-bearing +sibling: one presence signature, two distinct statements. **Authorization:** +`request_cid`, `decision_cid`. **History witness:** `previous_checkpoint` +and `observed_checkpoint`, each a P2 `AuthorityCheckpoint` `(store_id, +thread_id, sequence, head)` — not a bare CID, so the witness names *which +spine* it advanced (OB-2). Acceptance requires `observed_checkpoint` to be a +forward extension of `previous_checkpoint` on the same `(store_id, +thread_id)` spine, `sequence` strictly greater (else CHAIN HISTORY +REGRESSION). It binds the canonical challenge preimage of P0 §3 and is +committed by that section's CAS transaction. Attest and audit stay distinct +but co-signed — *no authorization floats free of the history that gave it +meaning.* + +### RevocationRecord (quorum) +```json +{ "v": 1, + "payload": { "revoke": "b3:…", "reason": "compromise|rotation|retirement", + "succession": "b3:…", "policy": "cid:…" }, // CANONICAL UNSIGNED + "signers": [ { "by": "b3:aa…", "sig": "…" }, + { "by": "b3:cc…", "sig": "…" } ] } // sorted, deduped +``` +**One payload, many detached signatures** — every signer signs +`content-CID(payload)`, so all cover identical bytes (a signature nested in +the object it signs is circular). `signers` is sorted by `by` and +deduplicated (one identity can't count twice toward `k`); the signature set +is *not* signed; the chain-append `sig` (WF-2) is separate and last. +Acceptance is **epoch-bound (OB-7):** `|distinct valid signers ∩ eligible| +≥ k` under `policy`, **and** `policy` MUST be the policy active at the +record's own checkpoint — +``` +policy_cid == ActiveRevocationPolicy(revoke_target, observed_checkpoint, generation) +``` +— else an attacker replays an older, weaker, validly-signed quorum policy. +Policy *transitions* are themselves authorized under the previously-active +policy (or a separately-defined root-transition rule). The quorum policy is +a principal-signed loosening entry (defining *who may revoke* is authority +structure, L2). + +**Enrollment records the exact required revocation predicate, not a strength +tuple (OB-7).** The enrollment strength tuple `(SAS entropy × rounds, +witnesses, presence)` is **not totally ordered** — "2 rounds + 1 witness + +hardware" is incomparable to "1 round + 3 witnesses + no hardware" — so +"punting ≥ pinning" cannot be derived from it after the fact. Instead each +PinRecord names, at enrollment time, the *precise* `RevocationPolicy` CID +required to later punt this identity. Revocation compares against that +recorded predicate, never an informal ordering. + +## 3. Break-glass & succession (REQUIRED) + +A quorum strong enough to defeat a hostile revocation can also lock out a +legitimate owner who loses `k` keys — availability cuts both ways. So +enrollment MUST provision recovery: + +- a **pre-enrolled recovery factor** (offline hardware key / printed share) + counted in `n`; +- a **succession path** transferring a principal root to a new key under + quorum, *or* **time-delayed unilateral recovery** — a self-revocation any + single device can start that only takes effect after a published + generation delay, giving co-signers a veto window ("social recovery with + timelock"). + +Revoking the **last** root without a `succession` ends the mesh — +implementations MUST refuse unless the record carries `"tombstone": true`. + +**PO-R is CONDITIONAL liveness (OB-8).** "Never permanently locked out" +cannot be proven unconditionally — all recovery factors can be destroyed, +all witnesses can vanish, an adversary can block progress forever. State the +theorem with its assumptions: +> **Given** at least one configured recovery threshold remains uncompromised, +> eventual communication among an authorized recovery quorum, fair +> advancement of recovery generations, and no permanent destruction of all +> recovery material — **then** a legitimate owner can eventually install a +> successor root. + +The time-delayed unilateral path has a specific threat to answer: an attacker +who owns *one* device and **suppresses the veto messages** during the delay +window. Mitigations (each recorded, not assumed): require the veto window to +be acknowledged over ≥ 2 independent channels; make a *missing* expected +acknowledgement itself veto-the-recovery (fail-closed on silence); and cap +unilateral recovery to below the quorum needed for high-ceiling authority. +This subsystem is **required and specified conditionally**; the full +state-machine is P4's open work — the suite does not claim it closed. + +## 4. Presence-attested pins +A pin MAY carry a `presence` discharge — a WebAuthn/passkey step-up bound to +the pin's `ContentId` (`DischargeVerifier`; PR #214). Upgrades first contact +from "someone clicked" to a hardware-attested human decision. Optional by +law, recommended for broad-ceiling pins. + +## 5. Proof obligations + +| PO | Statement | Tier | +|---|---|---| +| PO-2b | a sub-quorum coalition cannot shrink the load-bearing set | 3 | +| PO-5 | (shared with P0) delegation chain soundness; re-key ⇒ re-ceremony | 3 | +| PO-R | recovery is live — no permanent legitimate lock-out | 3 (liveness) | + +## Relations +- P0 (L2/L5) · P2 (the store) · P3 (enrollment produces PinRecords) · + mesh #39/#40 (CertChain + PoP) · PR #214 (presence) · newt-agent#1209 diff --git a/docs/spec/rendering-security-profile.md b/docs/spec/rendering-security-profile.md new file mode 100644 index 0000000..2ae982c --- /dev/null +++ b/docs/spec/rendering-security-profile.md @@ -0,0 +1,154 @@ +# P5 — Rendering Security Profile + +**Layer:** 2. **Depends on:** P0 (the decision seam), P1, P4 (surface +identity). **Status:** DRAFT. **Teeth:** Lean effect-CID soundness (Tier 3) +for the cryptographic half; **surface-attestation protocol** obligations +(Tier 2) for binary + rendering attestation; a **stated, shrunk +human-factors residual** for the analog gap that is not cryptographic. +Naming the boundary honestly is the whole job. +**Owns:** binding *what the human saw* to *what executes*, surface +attestation (proving the renderer is faithful), and the obligations a +rendering surface carries. + +## 1. Effect binding — what you see is what you sign + +`action` carries both a human `display` and an `effect` — the content-CID of +the **canonical, fully-resolved call** (arguments *and* resolved resources — +the `CallRequest` the tool layer produces): + +```json +"action": { "class": "exec", "display": "run_command: cd ", + "effect": "cid:…" } +``` + +The gate MUST, **before minting authority, recompute the canonical effect +from the call it is about to run and check it equals `action.effect`** — +otherwise a stale or lossy `display`→effect mapping approves X and executes +Y while the CID still matches (confused-deputy / TOCTOU; WYSIWYS, +Landrock-Pedersen 1998). Display and effect are bound under the one +signature. **PO-W (soundness):** the gate executes the exact +`Sealed` whose CID was approved. + +**Effect binds a value; the value must freeze the mutable world (OB-10).** +`action.effect` is only as strong as what enters the sealed `CallRequest`. +"Resolved resources" is therefore given a **normative per-class boundary** — +each action class names which resource *identities* (not mutable handles) +are sealed: + +| Class | Sealed identity — never a mutable handle | +|---|---| +| `file` | canonical path **+** inode/file-identity or content-CID | +| `container` | image **digest**, never a mutable tag | +| `repo` | repository identity **+** commit/tree CID | +| `network` | destination policy **+** an explicit DNS-resolution policy | +| `env`/`creds` | an immutable **secret-*version* reference** / one-shot capability / keyed commitment — **NEVER raw secret material** (OB-18) | + +Anything left ambient at approval time — symlink targets, DNS answers, +mutable files, env vars, container tags, credentials resolved *after* +approval — is a **named residual**, never silently folded into PO-W. If a +class cannot freeze a resource, it says so; it does not pretend the +signature covered it. + +**Never put raw secret material in a signed record (OB-18/#7).** The record +is content-addressed, permanently retained, replicated, and offline-guessable +against its CID — so a raw credential in the `body` is a permanent disclosure +(and lands in logs). An authority record MAY reference a secret only as an +immutable **secret-version id**, a **one-shot capability**, or a **keyed +commitment** the gate later redeems; the material itself resolves at +execution time, outside the record. A verifier rejects a body carrying an +apparent raw secret in a credential field. + +## 2. Gate-signed requests (the phishing-canvas closure) + +A **remote** surface MUST verify the request's signature and that `by` +chains to a pinned principal **before rendering** — an unauthenticated +prompt is a phishing canvas that trains the human on fake ceremonies, even +though its harvested decision is unredeemable (the `Decision.request` CID +binding, P0 §2.3). In-process, `by`/`sig` MAY be omitted. + +## 3. The render-swap closure + +`Decision.request` = the content-CID of the `PermissionRequest` as issued; +the gate accepts only a matching CID (P0 §2.3 step 1). This binds *what was +shown* to *what was granted* — an attacker cannot show request A and apply +the approval to request B. + +## 4. Surface attestation — shrinking the faithfulness gap + +Effect-binding proves the decision is bound to the data; it does not prove +the *surface* is a faithful renderer. Two complementary attestations raise +the bar so **an unfaithful surface has trouble passing** — the surface +becomes a participant that must prove *what it is* and *what it did*. + +**4.1 Binary attestation — what the surface IS.** A surface's identity (P4: +a keypair) is bound to a **measured code identity** — a reproducible-build +hash, TPM/DICE quote, or platform attestation (Play Integrity / App +Attest). The principal blesses surface *measurements* onto a profile +allowlist (the same allowlist discipline as P1 §4·4, applied to code). A +decision from a surface whose measurement is not blessed is **refused for +actions above a policy-set ceiling** — degrading the residual from "any +surface on earth" to "a known-good build." A tampered renderer has a +different measurement and fails the check. This is remote attestation +(Parno et al.); its primitives are a Tier-1 assumption, its handshake a +Tier-2 (protocol) obligation. + +**4.2 Rendering attestation — what the surface DID (corrected, OB-18/#7).** +The mechanism is a **byte-comparison against a gate-produced canonical +render**, *not* a token that "proves" faithful display. Because `display` is +a deterministic function of `effect` (§1), **the gate produces the canonical +render bytes itself**; the surface's signed render transcript commits to the +bytes it presented; the verifier **byte-compares** the committed render +against the gate's canonical render. Equal ⇒ the surface emitted the right +bytes. + +The **witness token** (a value derived from `(effect, nonce)` that must +appear in `display`) is retained only as an **attention-binding aid** — it +nudges the human to look — and is explicitly *not* proof of faithful +rendering: a malicious renderer can print a misleading partial summary *and* +include the correct token. So the token proves *possession of effect-derived +information*, never *that the human saw the whole effect*. Even the +byte-comparison proves only *what bytes were emitted*, not *what pixels a +possibly-hostile display painted or what the human understood* — §5's +irreducible residual. + +Both compose with the existing gate checklist: high-ceiling actions MAY +require a blessed measurement (4.1) **and** a token-bearing render transcript +(4.2) as part of the `attest` discharge (P0 §3). + +## 5. The residual — faithfulness is *shrunk*, not eliminated + +Even with §4, honesty is preserved (this is the discipline the reviews +praised): binary attestation proves the code is known-good, **not** that +known-good code has no rendering bug; the render transcript proves what bytes +were emitted, **not** what pixels a compromised display driver painted; the +witness-token ceremony assumes the human actually reads. The final analog +gap — human eyes on a possibly-hostile display — is irreducible. So P5: + +- **requires** `display` to be a deterministic function of `effect` (§1), so + it is checkable, and a surface that cannot render `effect` faithfully MUST + refuse rather than show a prettier `display`; +- **offers** binary + rendering attestation (§4) to shrink the residual by + policy ceiling; +- **names** the remainder as irreducible human factors — `attest` for high + ceilings and distinct ceremony UI (newt#1209) mitigate, never eliminate. + +Shrunk, bounded, named — not "solved." A rendering profile that *claimed* +cryptographic faithfulness would be exactly the "prose becomes +authority-bearing protocol" failure the security reviews caught. + +## 6. Proof obligations + +| PO | Statement | Tier | +|---|---|---| +| PO-W | the gate executes the exact `Sealed` whose CID was approved | 3 | +| PO-RES | each action class seals resource *identities*, not mutable handles (OB-10) | 3 + vectors | +| — | render-swap / phishing-canvas closures | 3 (with P0 gate checklist) | +| PO-SB | binary attestation: a decision above ceiling C is honoured only from a blessed surface measurement | 2 (protocol) | +| PO-SR | rendering attestation: committed render bytes == gate's canonical render (byte-compare) ⇒ correct bytes emitted (NOT faithful pixels; token is only an attention aid) | 2 (protocol) | +| residual | display-faithfulness on a hostile display | *shrunk by §4, not eliminated — stated* | + +## Relations +- P0 §2.1/§2.3/§3 (request, decision, attest discharge) · P1 (canonical + CIDs, allowlist) · P4 (surface identity the measurement binds to) · + newt-agent#1209 (ceremony UI consumer) · Landrock-Pedersen 1998 (WYSIWYS) + · remote attestation (Parno et al.) for §4.1 diff --git a/docs/spec/signed-object-profile.md b/docs/spec/signed-object-profile.md new file mode 100644 index 0000000..f443fc5 --- /dev/null +++ b/docs/spec/signed-object-profile.md @@ -0,0 +1,186 @@ +# P1 — Signed-Object Profile + +**Layer:** foundation (no dependencies). **Depends on:** —. +**Depended on by:** P0, P2, P3, P4, P5 (everything). +**Status:** DRAFT. **Teeth:** proptest round-trip vectors + a Lean +canonicalization-injectivity contract (Tier 3); the crypto primitives are +Tier-1 assumptions. +**Owns:** how any object gets a name, a canonical form, and a signature — +and how a verifier decides which algorithms it will honour. + +This profile is the alphabet the other five write in. It contains no +authority semantics; it makes objects *nameable, canonical, and +verifiable*. + +## 1. Identifiers are self-describing + +Fingerprints are **multihash**; keys and signatures are **multicodec**- +tagged; links are **CIDv1**. Comparison is over the opaque bytes *including +the algorithm code* — two hash algorithms never collide silently. The key +is the identity; the fingerprint `H(pubkey)` is its self-certifying *name*. +*BLAKE3 is an implementation detail, not a law.* + +## 2. One schema, one signed byte-string, many views (OB-4) + +An earlier draft said "JSON for interchange, TOML at rest, DAG-CBOR for +signing" *and* "verify over received bytes, never reserialize" — which is +contradictory, because a recipient handed JSON has not received the signed +DAG-CBOR bytes, and converting JSON → DAG-CBOR *is* a reserialization. The +resolution: **the canonical DAG-CBOR bytes are carried, not reconstructed.** + +**The signed-object grammar is ONE normative constructor (OB-13/#2).** A +naive envelope that signs only `cid = H(body)` leaves the interpretation- +bearing fields (`profile`, `codec`, `signer`) *outside* the signature — an +attacker could re-tag the codec or profile without breaking the sig. So the +signature covers a canonical **protected tuple**, not the bare CID: + +```json +{ "profile": "agent-bridle/permission-request/v1", // protected + "codec": "dag-cbor", // protected + "cid": "cid:…", // = H(body); protected + "signer": "b3:…", // protected + "body": "", + "sig": "…" } +``` +``` +protected = canon( "agent-bridle/signed-object/v1", // domain separation + profile, codec, cid, signer ) +sig = Sign(signer, protected) +``` + +Normative bindings (no implementer choice left): +- **`sig` covers `protected`** — profile, codec, cid, signer are all + authenticated; changing any breaks the signature. +- **the body's own domain tuple** (§4·5) MUST equal `(profile, codec)` of the + envelope, and its `signer`/`by` MUST equal the envelope `signer` — an + implementation rejects any mismatch (no split identity across the boundary). +- `signer` is the one canonical location for the key id; `by` in inner-record + examples (P0/P4) is the *same* value surfaced logically, never a second + authority. +- verification (identical in all four languages): + ``` + 1. allowlist codec + algorithms (§4·4) — before touching body + 2. recompute protected; verify sig over it under signer + 3. verify cid == H(body) + 4. decode body; check body domain tuple == (profile, codec, signer) + 5. schema + critical fields; reject unknown authority-bearing fields + 6. construct Sealed + ``` + +**Genesis is non-circular (OB-14/#3).** P2 defines `store_id = H(genesis +record)`, but every body must bind `store_id` (§4·5) — a fixed point at +genesis. Resolution (normative): **the genesis body carries the reserved +sentinel `store_id = 0x00` (`STORE_ID_SELF`); its resulting `cid` becomes the +store's `store_id`**, and every *subsequent* record binds that value. A +verifier resolves `STORE_ID_SELF` to "this record's own cid." The first +ordinary record can therefore be canonically encoded. + +**JSON and TOML are views/containers, never independent authority-bearing +serializations.** A JSON rendering is for humans/non-authority interchange; +the *authority* lives in `body` + `protected`. TOML policy files (#220) wrap +the signed object. Wall-clock is never a coordination primitive — validity +keys on generation counters; RFC 3339 timestamps are provenance *data*. + +## 3. The Memo discipline (WF-2) + +Every wire object is a `Memo`-descendant (content-addressable-python +`data.py`: every value carries its content-id and *reads verify it*). +Capabilities attach by **mechanical criteria**, not by quota: + +- **content-CID — unconditional.** Anything serializable and meaningful + beyond this process has canonical bytes, hence a name. +- **`by` + `sig` — at trust boundaries.** REQUIRED when the object crosses + to a different fingerprint (remote surface, delegated agent, another + host); MAY be omitted in-process — same trust domain, nothing to assert. +- **`parents` — for durability.** Anything appended to a chain-store (P2) + links. +- **Sealed at load.** Objects are constructed *only* through verification + (CID recomputed; sig checked when present) — verified once at the + boundary, immutable after. Nothing enters a kernel unverified. `Sealed` + is the Rust heir of Memo's read-time tamper check. + +Const-correctness for integrity: one unsigned hop breaks the chain of +custody like one non-const cast breaks the guarantee. Applies to **all of +the data layer, none of the resource layer.** + +## 4. Verification rules (the sharp edges) + +1. **Verify over received canonical bytes, never a re-serialization.** + Typed deserialization drops unknown fields; reserializing a parsed + object cannot reproduce the signed digest. Verify the bytes as received, + *then* parse (RFC 8785 pitfall; JWS/COSE practice). +2. **Unknown authority-bearing fields fail closed.** A field the profile + version does not define is *rejected*, not ignored — tolerating it is a + silent downgrade / version-confusion surface. Non-authority annotations + MAY be preserved verbatim only when the profile marks them non-critical + (COSE critical-header model). +3. **Version dispatch, not lenient parsing.** All objects carry + `"v": `; verification dispatches on it. +4. **Algorithm allowlist before dispatch (PO-8).** Self-describing + identifiers let the *object* declare its algorithm — so a verifier that + dispatches on the declared code alone lets an attacker pick a broken + hash (`alg:none` / algorithm-confusion). A verifier MUST check the + declared code against the locally-trusted profile table (§6) **before + hashing or verifying**, and reject anything outside it. Agility lives in + the profile, never on the wire. +5. **Universal domain separation + context binding (OB-6).** *Every* signed + `body` MUST begin with a domain-separation tuple, not just the WebAuthn + challenge: + ``` + ("agent-bridle///", + store_id, thread_id_or_principal_id, generation, ) + ``` + A signature is valid only for its exact `(record-type, store, thread/ + principal, version)` context. Without this, a validly-signed payload can + be replayed **across stores, principals, causal threads, structurally- + compatible record types, and profile versions.** `store_id` is a + normative, cryptographically-bound identifier (P2 §) — "same store" is a + value the signature covers, not prose. Verifiers reject a signature whose + domain tuple does not match the context in which it is being used. + +## 5. Deterministic signatures (why Ed25519 is pinned) + +For Profile v1, signing MUST be **deterministic**: `Sign(sk, message)` +yields one canonical signature encoding for a fixed key and message. +Ed25519 provides this (RFC 8032 derives the nonce from key and message). A +randomized scheme (ECDSA with a random nonce) would produce a different +signature — hence a different content hash — on every re-sign, forking any +chain built over it (P2). Determinism governs **reproducibility**; +collision resistance of `H` governs **tamper-evidence**; they are +independent properties. (Information-theoretically: `H(sig|content,key)=0`. +The prose rule is normative; the identity is just why.) + +## 6. Profile v1 (pins, not laws) + +Each pin states the *property* a replacement must carry: + +| Pin | v1 value | Required property | +|---|---|---| +| Content hash `H` | BLAKE3-256 (multihash `0x1e`) | collision resistance; preimage hardness (L5 self-certification) | +| Signature | Ed25519 (RFC 8032) | **deterministic**; existential unforgeability | +| Canonical encoding | DAG-CBOR (codec `0x71`) | injective canonical serialization (one value ⇒ one byte string) | +| Links | CIDv1 | multihash-native, codec-tagged | + +Rotating `H` is a **re-naming ceremony** (P0·L5): keys sign linkage records +binding their new names; identity never moves. Rotating the signature +scheme is a **re-keying** (full L5 re-ceremony) because the key *is* the +identity. Profile rotation is a negotiated, principal-signed change to the +allowlist (a loosening entry, P0·L2), never a per-object choice. + +## 7. Proof obligations + +| PO | Statement | Tier | +|---|---|---| +| PO-1c | canonicalization is injective; verify-over-received-bytes is sound | 3 (Lean contract) | +| PO-8 | algorithm dispatch is allowlist-gated — no code outside the profile is honoured | 3 | +| WF-2 | the Memo discipline holds structurally on every wire object | vector | + +The kernel (P0) consumes `H` and `Sign` as **abstract injective / one-way +contracts** — this profile's job is to satisfy them, the kernel's job to +assume them. That boundary is what lets Aeneas run without modelling crypto. + +## Relations +- `content-addressable` crate — `ContentId`, canonical DAG-CBOR, + `MerkleNode`, the `Sealed` to build +- agent-mesh#66 — multihash wire format for `Fingerprint` +- #226/#227 — signed loosening entries (shipped) diff --git a/docs/spec/suite.toml b/docs/spec/suite.toml new file mode 100644 index 0000000..961507c --- /dev/null +++ b/docs/spec/suite.toml @@ -0,0 +1,18 @@ +# Ceremony Suite — compatibility manifest (OB-11). +# One atomic target for implementers; profiles still evolve independently. +# When a profile version bumps, update its pin here and re-run conformance. + +suite = "ceremony-suite" +suite_version = "0.3.1" # PROTOCOL FREEZE — authority type + wire grammar frozen + +[requires] +p0 = "0.3" # ceremony-contract — the narrow waist (five laws; Authority = Effect×Assurance×Scope) +p1 = "1" # signed-object — CID/canon/Sealed/allowlist/envelope +p2 = "0.2" # chain-store — causal transcript + anti-rollback anchor +p3 = "0.2" # enrollment — SAS/PoP/anchors +p4 = "0.2" # identity-lifecycle — roles/revocation/recovery +p5 = "0.2" # rendering-security — effect binding + surface attestation + +# Cross-language conformance vectors (Rust/Python/Dart/TS must agree). +# CID is populated once the kernel + vectors exist. +conformance_vectors = "cid:TBD"