Who Proves the Agent Is Yours?

Take the Ashdown instruction, an invented intake matter that recurs through this book. Ashdown Ltd instructs a firm. The client grants the intake agent the right to read and summarise a privileged advice note and to send the public filing. The intake agent passes a narrower grant to a research agent, and another to a drafting agent, which may send the filing and may not read the advice. At tick 4 the drafting agent sends the intake agent a message: put the advice note into my working folder. The intake agent reads the note, under its own valid grant, and does so.

Every grant in that story narrows the one above it, and nothing was forged. The privileged note is now with an agent never allowed to read it and allowed to send the filing out.

"Each hop may only narrow" is the right rule, and it answers a smaller question than the one a client is asking. Three claims follow. First, monotonic narrowing is a short theorem with an old pedigree, but it binds only where something runs the check, and the published OAuth standard for token exchange tells token consumers not to use prior actors in access decisions. Second, narrowing does not stop a confused deputy: every grant can narrow and the breach still happens, because authority moves by asking as well as by delegating. Third, and most contestable: because nothing downstream can widen, the rule moves the whole bet to the root, and a green chain cannot tell a root the client issued from one issued with its stolen key, or a root cut to the task from one cut to anything the task might need. Faced with that choice and a stalling agent, deployers will tend to mint wide roots, and the chain will certify them.

I build verified AI systems for law firms, so I gain if partners start asking who signed the root. Nothing here is legal advice.

I also owe a correction. In Part III of The Soul and the Hands I reported short theorems on capability bounds. Of one, that A ⊆ S and B ⊆ A give B ⊆ S, I wrote, before correcting it, comparing it with CHERI and seL4: "The mathematical content is the same: you cannot amplify authority through delegation." Another, no_amplification, had the hypothesis h_valid : ∀ d ∈ delegations, d ⊆ initial, which assumes every delegation is a subset. Both proofs are subset transitivity. Those systems' results concern what a machine can do. Mine concerned sets, and assumed the thing that needs enforcing.

The theorem, and what it needs

Here is a better version, on the case. A Link records who issued it, under which toy key, the grant it conveys, and how many further hops it allows. A child follows a parent when its issuer is the parent's holder, its grant attenuates the parent's, and it has less depth left. wellFormed asks that of every adjacent pair. The block below is the statement only; the proof is in lean/BuildingInSteel/Delegation.lean, which compiles on Lean v4.29.1 with no libraries beyond the book's case file.

theorem chain_narrowing (root : Link) (rest : List Link)
    (hw : wellFormed (root :: rest) = true) (a : Action) (t : Tick) :
    ∀ l ∈ rest, l.allows a t = true → root.allows a t = true := by

For every well-formed chain, whatever any link allows its own holder to do at any tick, the root allows its holder to do at that tick. That hypothesis has the same shape as the one I just criticised. The difference is that wellFormed is a decidable function over records: a verifier can run it, and on a widened chain it returns false (widening_hop_caught_two_ways). The theorem's real content is an obligation, that something must execute it.

depth_bounds_chain proves a well-formed chain has at most root.depth hops below the root, the idea behind X.509's pathLenConstraint (Cooper et al., 2008, RFC 5280). And the book's case file was not good enough: Grant.narrows has no clause on revocation. plain_narrows_misses_revocation shows an unrevoked child of a revoked parent passing it, and permitting at tick 6 what the parent refuses. So attenuates adds revCovers.

None of this is new. Norm Hardy's confused deputy dates from 1988. SPKI's reduction rule combined two certificates through AIntersect and VIntersect in 1999 (Ellison et al., RFC 2693), an Experimental RFC. UCAN's specification says each delegation "MUST either directly restate or attenuate (diminish) its capabilities" (UCAN specification). What I add is not the rule but a kernel-checked statement of what it leaves open.

What the documents actually say

This is what I read on 02/11/2026. Internet-Drafts carry the IETF's warning to cite them only as work in progress, so treat each draft row as a dated snapshot.

The sentence that matters most is in RFC 8693, which gives chains a syntax and then says:

"For the purpose of applying access control policy, the consumer of a token MUST only consider the token's top-level claims and the party identified as the current actor by the "act" claim. Prior actors identified by any nested "act" claims are informational only and are not to be considered in access control decisions." (section 4.1)

So OAuth's delegation chain is a record of who, as both individual drafts above point out. Any narrowing has happened earlier, at an authorisation server, under what the RFC calls "policy decisions made with respect to the specific needs of individual deployments". So "we use token exchange" is no evidence that each hop narrowed.

The difference is computable. lastTokenAllows reads only the current actor's grant, and wholeChainAllows reads every link. widening_hop_caught_two_ways: a research link that adds a right to send the advice out passes the first and fails the second. last_token_misses_root_revocation: with the root revoked at tick 5 and the leaf not told, the last token still reads at tick 6 and the whole chain refuses. root_revocation_stops_meet proves the general form, and it covers only a verifier reading the current root; how current is the race in Yesterday's Permission. meet_bounded_without_hop_checks adds a design point: intersecting at the verifier gives the root bound for every non-empty chain, well-formed or not. A hop check run by the issuer trusts that issuer. A check run by the verifier, the meet or wellFormed, does not. The analogy to RFC 8693 is mine and is not a model of it.

The deputy

Hardy's story is of a compiler licensed to write in its home directory, given an output file name by a user, which overwrote the billing file. "The fundamental problem is that the compiler runs with authority stemming from two sources" (Hardy, 1988). It "serves two masters".

The opening scene, in Lean. This block is complete as quoted and compiles against the file's definitions.

theorem narrowing_does_not_stop_deputy :
    researchGrant.narrows intakeGrant = true ∧
    draftingGrant.narrows intakeGrant = true ∧
    draftingGrant.permits .draftingAgent readAdvice 4 = false ∧
    blindGate (ownAuthority intakeGrant) confused = true := by decide

Both hops narrow, the requester lacks the read, and the deputy's own check passes. That is one computed case. no_blind_gate_separates is general over gates, on those two requests: no function of actor, act and tick alone can admit the partner's request and refuse the drafting agent's, because they look the same to it. on_behalf_separates computes the escape, a gate that also reads the requester's grant, and on_behalf_no_amplification proves for every request that a pass means the grant supplied for the named requester permits the act.

The attenuating-tokens draft addresses the deputy by carrying designation and authority together, and concedes: "AATs make this possible but do not force it: an agent that also holds a broader token can still act under that one." That is my counterexample in prose. The delegation-chain draft, §9.3, says "a child cannot be induced (e.g. by prompt injection) to exercise authority the parent lacked". True, and in my scene the target is not the child. It is the parent, which has the authority, and the message came sideways. Dantuluri and Sundi set a good standard, that "a fully prompt-injected agent still cannot exceed the authority explicitly delegated to it" (Dantuluri and Sundi, 2026). They report their confused-deputy scenario blocked in their own testbed, but the guarantee as stated is that a hijacked agent "can exercise only its bound, attenuated grant". The intake agent in my scene meets that. It exceeded nothing. The standard bounds authority and does not ask whose purpose the authority served. The pattern has been demonstrated on a shipping product: AppOmni's researcher used second-order prompt injection to make "a seemingly benign Now Assist agent" "recruit more powerful agents", on a platform where agents by default "run with the privilege of the user who started the interaction", and reported that ServiceNow confirmed the behaviours "were intended" (Costello, 2025). That is a demonstration, not a reported harm.

MCP uses the term more narrowly. Its security guidance applies "confused deputy" to OAuth proxies obtaining authorisation codes without proper consent, and forbids token passthrough. Both are correct, and neither addresses one agent asking another over a channel the gate cannot see.

The gate has a further limit. misdeclared_requester_passes shows a deputy naming the partner while acting for the drafting agent, and getting through. An LLM-driven deputy is the wrong component to fill in that field: the attenuating-tokens draft lists the sources of designation as "an invoking principal, prompt injection, tool output, or model error". So the requester must come from something the model cannot edit: a token the caller derived and presented, verified outside the model's reach. That is only available when the request arrived as a request. If the instruction arrived inside a document the agent read, there is no authenticated requester at all. The answer there is architectural: take control flow from the trusted query alone, as CaMeL does, which The Hands discusses. This is sketched here, not proved.

Whose root?

Now the title. wellFormed never reads the first link's issuer. wellFormed_blind_to_root_issuer proves it for every chain: changing who issued the root changes nothing. This block is complete as quoted.

theorem wellFormed_blind_to_root_issuer (root : Link) (rest : List Link) (i : Principal) :
    wellFormed ({ root with issuer := i } :: rest) = wellFormed (root :: rest) := by
  cases rest <;> rfl

self_rooted_chain_narrows computes the consequence. The intake agent issues itself a root with the right to send the advice out, and delegates to the research agent. The chain is well-formed, every key verifies, and chain_narrowing holds of it. Only an anchor list, configuration from outside the chain, refuses it. stolen_key_chain_accepted goes further: a root made with the client's stolen key passes accepted, though the client never issued it, because accepted has no input that could tell. registry_decides_identity needs no theft, only a wrong registry entry. accepted_guarantees is the honest general statement: an anchored issuer, a key matching the registry, and the narrowing bound. Each conjunct concerns configuration or the chain, and none concerns what the client decided.

I am not the first to notice. In 2000 Ellison and Schneier's second risk of public key infrastructure was "Who is using my key?", and their third that an attacker who adds a public key to a verifier's root list can "issue his own certificates" (Ellison and Schneier, 2000). Among the agent drafts, Asor's individual draft, §9.7, is exact: "verification can establish that no hop exceeded the root, never that the root was right." Its §6.4 records trust-anchor provenance as "open and is not solved here". The attenuating-tokens draft puts establishing, rotating and revoking anchors "outside the scope of this specification". A token cannot establish ownership. It can show possession of a key that a registry associates with a name.

English agency law drew this line long ago, and the structure transfers though the doctrine does not: an AI agent is not a person, and I do not claim these rules apply to it. The Supreme Court summarised it in Law Debenture v Ukraine: actual authority "describes a legal relationship between principal and agent created by a consensual agreement to which they alone are parties" [([2023] UKSC 11, para 38)](https://caselaw.nationalarchives.gov.uk/uksc/2023/11). Apparent authority arises from "a representation made by the principal" (para 39). The Privy Council, on appeal from Bermuda and so persuasive rather than binding in England, stated the rule a chain cannot check from inside: "Judges have rightly resisted the notion that an agent can clothe himself with authority" [(East Asia Company v PT Satria [2019] UKPC 30, para 61)](https://caselaw.nationalarchives.gov.uk/ukpc/2019/30), with "rare and unusual" exceptions that turn on what the principal did.

Read as a specification, a registry entry is at most a representation, and para 39 asks for one made by the principal, so an entry the registry's operator got wrong is not even that. Whether the client agreed is a fact about the client. That is the top of the hierarchy in Who Gets to Write the Specification?, turning up one level lower. So the title's question has an answer, and it is not a mathematical one: a person proves it, by an act of consent recorded somewhere the agent cannot write.

A compromised signer is therefore the incident to plan for. The attenuating-tokens draft: a compromised anchor key "breaks the security guarantees of all chains anchored to that key". Its sequence is to replace the key and re-issue roots; I would add treating everything done under the old anchor as suspect until reviewed. Detection is the gap: nothing in accepted fires. The web's answer is Certificate Transparency, logging issuance so that anyone can "notice the issuance of suspect certificates" (Laurie et al., 2021, RFC 9162), itself Experimental. The analogue here is an append-only log of root issuance that the principal or its firm monitors, with a missing inclusion proof treated as a refusal, signers and logs run by separate parties, and an agreed response when two witnesses see different heads. That is a proposal: it is in none of the agent drafts above, I have no implementation, and it is not in the Lean.

No widening puts the whole bet on the root

no_hop_serves_unrooted_need is the contrapositive of the narrowing theorem, proved for every well-formed chain: if the root does not allow an act at a tick, no link can. So, short of a new root, the root must already cover everything its sub-tasks will need, and a model chooses those sub-tasks at run time.

root_width_is_invisible computes the choice on the case. Mid-run the research agent finds it needs the public filing, for the limitation note. A root cut to the task as first understood cannot serve that. A root cut to anything the task might need can, and also carries the right to send the advice out. accepted returns true for both, a root of two actions and a root of six.

MCP has step-up, AuthZEN a requestable denial, A2A an authorisation-required state. Each hands the question upstream, so "only narrow" is workable only with a route back to whoever can issue a wider root, usually a person. The cost moves to that person's queue, and whether a reviewer facing a stream of elevation requests stays a real control is unmeasured here; the third objection below turns on it. What MCP's own guidance documents is the opposite failure: its attack description is scopes "granted up front because the MCP server exposed every scope", it lists "Consent abandonment" and "Scope inflation blindness" among the risks of that design, and its mitigation is incremental elevation. Who narrows matters to the cost. In MasDrift's benchmark, an attenuated policy carried down the chain by the agents eliminated executed unauthorised actions, blocked up to 54.5% of attempted required calls and forfeited up to 36.3 points of completion. Re-anchoring each call to a policy compiled from the original request reduced unauthorised actions without eliminating them, blocked at most 3.5% and moved completion by at most 4.5 points (Xu et al., 2026). That favours a ceiling checked at the verifier over attenuation trusted to each hop, and it weakens the stall half of my incentive argument. It does not touch the width half: that benchmark's policy comes from the request, and whatever compiles it chooses the width.

So consider the incentive, which is an argument and not a measurement. A deployer whose agent stalls has three moves: approve more often, mint wider, or have a classifier cut each task's grant from the request under a role ceiling. The third is the strong reply: on its author's own 600-prompt dataset, adding a classifier closed 84.4% of severity-weighted attack surface, against 27.9% for the ceiling alone (Noyan, 2026). That is not deployment data, the ceiling is still a root someone minted, and accepted cannot tell a classifier's cut from the client's. Minting wider can be a configuration change, it stops the stalls, and it leaves the audit output as green. Approval latency is the limit, and it falls on the people the system exists to save time for. Asor is right that approval policy "belongs at root issuance", and the question for a buyer is what stops that approval being one broad click at onboarding. The drafts I read give no measure of root width, and the Lean only demonstrates that accepted is indifferent to it.

What exists and what does not

Proved generally in lean/BuildingInSteel/Delegation.lean (no sorry, no declared axioms; #print axioms lists at most propext and Quot.sound): chain_narrowing, depth_bounds_chain and no_hop_serves_unrooted_need, for every well-formed chain; attenuates_sound, for every attenuating pair of links; meet_bounded_without_hop_checks, root_revocation_stops_meet and wellFormed_blind_to_root_issuer, for every non-empty chain; accepted_guarantees, for every accepted chain; on_behalf_no_amplification, for every request and pair of grants; and no_blind_gate_separates, for every gate but on the one pair of requests.

Computed on one fixed case, illustrations or counterexamples and not general results: plain_narrows_misses_revocation, last_token_misses_root_revocation, widening_hop_caught_two_ways, narrowing_does_not_stop_deputy, on_behalf_separates, misdeclared_requester_passes, self_rooted_chain_narrows, stolen_key_chain_accepted, registry_decides_identity, root_width_is_invisible.

Assumed and not modelled: unforgeable signatures (Link.key is a toy number), holder binding, replay protection, canonicalisation of what is signed, a shared clock, honest registries. The drafts do that work: Asor links each delegation to its parent by "a cryptographic byte-commitment", and both bind tokens to holder keys, though the attenuating-tokens draft warns its injection guarantee "holds only while the holder private key is out of the model's reach". Nothing in my file connects to a running system, the gap The Proof Passed. The Wrong Thing Ran. examines.

Sketched: the requester field coming from outside the model, and control flow taken only from the trusted query.

Not modelled: information. Action has no hand-off, so the note reaching the drafting agent in my opening is prose, not Lean. Every Query Was Allowed and A Summary Is Not a Permission cover that ground.

Does not exist, as far as I have read: a working-group draft or RFC requiring an enforcement point to verify offline that an agent chain narrows; a measure of root width in any draft above, or a deployment measurement of it stating its sample and method; a log of root issuance required by any agent draft. A vendor selling the remedy says the average agent carries "roughly 10 times more access than its actual workflow requires", with no sample or method on that page (Obsidian Security, 2026). So the third claim is an argument, and prediction 2 tests it.

Objections

"Capability systems solved this decades ago." Largely right, and I concede the mechanism. Hardy's own remedy is a capability that "both identifies the file and authorizes the compiler to write there", and Miller, Yee and Shapiro argue that "pure capability systems have significant advantages" over access lists (Miller et al., 2003). Under that discipline my deputy would act only under what the caller handed it, and the drafting agent has no capability to the advice. What survives is deployment and the root. Dantuluri and Sundi model common framework practice as "broad bearer credentials", and a capability system still starts from someone's root. Verdict: right on mechanism; the second claim concerns a discipline not yet adopted, and the third stands. I would give up the second on seeing a production agent framework with no standing credentials in the path.

"An authorisation server already does this, online, and better." On one trust domain, yes. A server can read current state, while offline chains accept what Asor calls "revocation latency". But the rule must be written into local policy, since RFC 8693 does not impose it; downstream parties must trust the server; and a matter running client to firm to vendor to model provider crosses domains. Identity chaining handles that crossing by asking each server to verify, which a third party cannot repeat from the token. Verdict: a server inside a domain, a verifiable chain across domains. I would drop the second half if cross-domain auditors turned out never to need independent verification.

"Step-up dissolves your third claim." The strongest reply. If elevation is cheap and well reviewed, roots can start narrow; MCP's guidance recommends that. Verdict: it dissolves the necessity, not the incentive, and elevation turns a security property into an attention budget. I would give up the claim if prediction 2 fails, or if reviewers are shown to keep refusing elevation at a meaningful rate after months of use.

"Authority is the wrong layer; information flow is the problem." Miller et al. report Boebert's 1984 claim that "no unmodified capability machine can enforce the *-Property", and call the resulting belief a myth. On either side of that dispute, grants govern acts, and a summary an agent already holds goes wherever its text can go. Verdict: correct and complementary. A chain bounds what may be done, a flow label what may be learned. I would change my mind only if chain checks were shown to imply a flow property.

Goodhart, and what formalising loses

Once "every hop verified" becomes a procurement line, expect it to be satisfied cheaply. The first move is the wide root. The second is naming: attenuates compares action lists, RFC 8693 calls scope semantics "service specific", and whoever defines a scope name decides what narrowing means. The defence is to measure what the chain does not show: what a root allows against what the run used, sampled by a person who knows the matter.

Formalising loses implied authority. The Supreme Court notes in para 38 that "actual authority may be express or implied", and implied authority is what lets a good associate do the obvious thing the partner forgot to mention. A chain has no such category. Some refusals will be wrong, and on a limitation date a wrong refusal is its own harm, the subject of Never Breaks a Rule, Never Finishes. It also shifts power. Whoever can run an anchor and a registry gains, and a small firm that cannot will rent one, so its supplier's registry says whose agent is whose.

What to do on Thursday

If you are a partner, ask whoever runs your tools three questions about one live matter.

1. Show me the root grant for this matter. Who approved it, and what does it allow that this task did not use?
2. If one agent asks another to fetch a document, whose authority is checked, the one who asked or the one who fetched?
3. If the key behind that root were stolen last week, what would have told us?

"We use OAuth" answers none of them. Narrower roots mean more interruptions, and those land on fee-earners.

If you build these systems, the route below is a design sketch, compiled against nothing and not tied to one vendor; everything named is a published specification or draft. The attenuating-tokens draft says each protocol "needs its own binding" and leaves that out of scope. The bindings I found are individual work: draft-prakash-aip-02 carries a chain in an X-AIP-Token header on MCP and a metadata field on A2A. MCP clients "MUST NOT send tokens to the MCP server other than ones issued by the MCP server's authorization server", which I read as reaching such a header, so a chain rooted at a client's anchor needs that authorisation server's cooperation, or a change to that rule, before step 2 can run on MCP.

agent process: no standing credentials, no signing keys in its environment,
               network off except through the gateway
tool call  ->  gateway (MCP or A2A endpoint)
               1. requester = the principal of the token the caller presented
               2. verify the whole chain to a configured anchor; fail closed if
                  any link is missing, expired or of unknown status
               3. decision = chain meet AND requester's right AND policy
                  (AuthZEN Authorization API, COAZ-MCP binding if on MCP)
               4. denied and requestable -> open an approval against the root's
                  author; a new or wider grant means a new root
               5. log root id, chain hash, requester, tool, decision

Sandboxed coding agents make the first line natural: OpenAI's Codex documentation says "By default, the agent runs with network access turned off" (OpenAI, Codex documentation). A sandbox limits what the process can reach, not on whose authority it acts, so the gateway sits outside it. For a first run, have one agent ask another for something the first may not read, and confirm the refusal names the requester. Then count approvals per task, which I have not measured.

Predictions

1. By 30/06/2027, the IETF OAuth or WIMSE working group will have adopted a draft that requires each hop of an offline-verifiable agent chain to narrow, and by 31/12/2027 no such document will have been published as an RFC. Refuted if no such adoption occurs by the first date, or if an RFC appears by the second. The delegate SD-JWT draft as it stands does not count, because limits there are optional.
2. By 31/12/2027, a published measurement of deployed agent credentials, stating its sample and method, will find that most root or initial grants allow at least twice the actions the tasks observed used. Refuted if such a measurement finds otherwise, or if none has been published, in which case my claim that this matters enough to be measured has failed too.
3. By 30/06/2028, a public incident report, advisory or regulator decision will describe harm in production, not a researcher's demonstration, in which one AI agent obtained an effect through a second agent's own valid credential that the first agent's credential did not allow. Refuted if a search at that date of the AI Incident Database, CVE records, and ICO and EDPB decisions finds none, which would suggest cross-agent deputies matter less than I claim, or that nobody is reporting them.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.