Authorization Revocation for Long-Running AI Agents: Root-Scoped Quiescence under Delegation and Asynchronous Execution
arXiv:2609.21284v1 [cs.PL] 18 Sep 2026
GENLIANG ZHU, Accentrust, Canada and Georgia Institute of Technology, USA CHU WANG, Accentrust, Canada and University of Illinois Urbana-Champaign, USA Long-running AI agents outlive initiating processes through credentials, delegated tasks, queues, callbacks, reservations, and provider-side operations. Cancellation, process exit, and credential revocation neither close every pre-cut carrier nor distinguish independently authorized shared work. We define root-scoped authorization quiescence: for each manifested sink, a certificate accounts for every cut-relevant acceptance under the retired root-epoch atom that precedes its local fence and excludes protected acceptance under that atom after the fence, while permitting exact rebind to a current, independently sufficient support. The root-scoped quiescence protocol linearizes a root cut, fences old-root expansion and protected sinks, represents alternative and conjunctive authority as antichains of minimal sufficient root sets, and composes provider-frontier certificates into a cutset over registered old-root paths. Exact channel-token accounting reconciles transfers; missing or conflicting evidence remains indeterminate. Under stated assumptions, we prove post-cut issuer non-expansion, support-sound projection, compositional soundness under exact channel conservation, independent-support preservation, merge-order independence, and crash/replay stability. A provider-free late-effect test suite matches 17/17 registered outcomes. Two cancellation-only and one cut-only execution accept the same class of already scheduled late effect; two cut-plus-fence executions, one restart, and one stale-process execution reject it. A separately implemented checker verifies 17/17 traces and rejects 44/44 consistently rehashed semantic regressions. The certificate establishes root-relative authorization quiescence within its bound manifest and configuration, not global idleness, rollback, or business completion. CCS Concepts: • Security and privacy → Access control; • Mathematics of computing → Distributed computing models. Additional Key Words and Phrases: AI agents, access control, authorization revocation, quiescence, distributed systems, cancellation, effect closure
1
Introduction
Long-running agents routinely outlive the interaction that launched them. A single task can create remote subtasks, durable queue entries, scheduled jobs, webhooks, delegated credentials, reservations, and provider-side operations. Stopping the local process therefore need not stop the task’s authority. Even an acknowledged cancellation can race with a remote completion, and a revoked token can leave a prepared operation or separately delegated credential able to commit. The operational question is not merely whether a controller sent a stop request. It is whether the retired authority has lost every remaining path to a future protected effect and whether every cut-relevant old-atom frontier crossing is terminally accounted. Existing interfaces expose observations that are useful but individually insufficient for that conclusion. MCP task cancellation and A2A cancellation are cooperative control transitions rather than proofs that every underlying effect has stopped [1, 18]. OAuth token revocation invalidates a named token at the authorization server, subject to the deployment’s propagation and mediation semantics [16]. Process exit establishes local process termination. Provider-local closure can establish that one provider has no unresolved effect frontier. None of these observations alone accounts for a Authors’ Contact Information: Genliang Zhu, Accentrust, Vancouver, Canada and Georgia Institute of Technology, Atlanta, Georgia, USA, [email protected]; Chu Wang, Accentrust, Vancouver, Canada and University of Illinois UrbanaChampaign, Urbana, Illinois, USA.
2
Zhu and Wang
pre-cut message already accepted by another provider, a credential derived before revocation, or a shared agent that remains valid under an independent authorization root. This paper studies root-scoped authorization quiescence. Let 𝑟 be an authorization root and 𝑐 a durable cut targeting (𝑟, 𝑒) that retires root epoch 𝑒 and advances issuer state to 𝑒 + 1. A quiescence certificate for 𝑐 asserts that every registered carrier and obligation whose selected support depends on the retired atom is terminated, effect-closed, exactly accounted as pre-fence committed, or atomically rebound to an independently sufficient witness that excludes the retired atom; every cut-relevant acceptance under that atom that precedes its provider-local fence is exactly accounted; every required sink has installed its fence; and every old-atom handoff in the frozen channel frontier is terminally accounted. No protected-sink acceptance ordered after its fence may depend on the retired atom. The assertion is relative to one root and one cut. It neither declares the whole system idle nor revokes work supported by other roots. 1.1
A strict counterexample
Consider a shared remote worker supported by roots 𝑟 𝐴 and 𝑟 𝐵 . Before shutdown, work under 𝑟 𝐴 creates a durable queue message and a provider-side reservation. The controller then receives a successful cancellation response, revokes the initiating token, and observes that the local process has exited. The queue has already accepted the message, so a remote worker can still convert the reservation into a protected effect. Declaring quiescence from the three local observations is false. Blind subtree revocation is not a correct repair. The shared worker may have an independent, still-current witness rooted only in 𝑟 𝐵 . Deleting the worker would over-revoke valid work, while retaining it without changing the selected support could launder 𝑟 𝐴 ’s authority through the shared principal. A sound protocol must therefore solve two problems together: close every effect path selected under 𝑟 𝐴 , including paths crossing provider boundaries, and preserve continuing authority only through an explicit atomic rebind to a support witness that excludes the retired root-𝐴 atom. 1.2
Protocol overview
We present a root-scoped quiescence protocol that establishes and certifies this root-scoped cut. The protocol maintains an outstanding authority–obligation graph. Each live authority instance records an antichain of minimal sufficient root-support witnesses and one currently selected witness. Carriers represent the means by which authority can outlive the initiator—credentials, tasks, messages, triggers, reservations, and prepared effects. Directed channel tokens represent work transferred between adapters or providers. Shutdown begins with a durable epoch transition that prevents new authority from being issued under the retired epoch. Required provider adapters install operation-time fences, enumerate or conservatively cover their local frontier, and drive each covered item to a terminal, effectclosed, pre-fence committed, rebound, or unknown state. An adapter then emits a signed leaf certificate binding the root, cut, coverage manifest, configuration, fence and log watermarks, rebind receipts, local-open set, and outbound and accepted channel tokens. The global combiner accepts a set of leaves only when the manifest is complete, the leaves agree on the cut, no unknown or conflicting state remains, and cross-provider channel tokens balance exactly. Missing evidence yields Indeterminate; known live work yields Not-Quiescent. Neither state is converted into success by timeout. This structure deliberately separates actuation from evidence. Provider-local effect-closure certificates are valuable leaves, but a collection of locally empty leaves is not yet a global proof: a message can be in flight between two locally empty frontiers. Conversely, global cancellation orchestration without provider effect fences cannot exclude a late commit. The protocol composes both layers at one root-epoch cut.
Authorization Revocation for Long-Running AI Agents
1.3
3
Contributions
This paper makes five contributions: (1) It defines root-scoped authorization quiescence and gives strict executions in which cancellation acknowledgement, token revocation, process exit, subtree revocation, or provider-local closure is insufficient. The definition distinguishes cessation of one authorization root from global system idleness and from business-level completion or rollback. (2) It introduces a support algebra for multi-root authority. Minimal sufficient root sets form an antichain, live instances select one witness, and continued use across shutdown requires an atomic rebind receipt to a witness excluding the retired atom. This preserves independent authority without permitting root laundering. (3) It gives an active cut protocol that combines a durable root-epoch transition, issuance freeze, sink fencing, carrier and obligation closure, exact inter-adapter channel accounting, and signed provider leaf certificates. Leaf certificates form a cutset proof rather than an unordered collection of local cancellation claims. (4) It establishes conditional safety and composition results: post-cut non-issuance, no false quiescence, independent-support preservation, merge-order independence, and crash/replay stability. It also identifies an indistinguishability boundary: an opaque endpoint that supplies no sound query, fence, expiry, or terminal receipt cannot contribute a positive quiescence leaf. (5) It implements an executable late-effect test-suite evaluation and a separately implemented trace checker for cancellation races, late effects, crash and restart, missing fences, in-flight channels, alternate roots, opaque endpoints, and certificate replay. Section 7 reports only executions accepted by the registered verifier. 1.4
Scope
The certified safety property covers registered endpoints and protected effect sinks whose authority lineage, carriers, and cross-provider transfers are completely mediated or conservatively represented. It is a claim that no future protected acceptance can depend on the retired root atom and that every cut-relevant old-atom acceptance preceding its provider-local fence is exactly accounted. Irreversible effects committed before those fences remain historical facts; task goal completion, compensation, global process passivity, physical-world cessation, and provider behavior outside the registered evidence boundary are separate properties. The remainder of the paper separates quiescence from adjacent control results (Section 2), states the system and assurance model (Section 3), formalizes the support and cut semantics (Section 4), presents the protocol and instantiations (Sections 5–6), evaluates the registered artifact (Section 7), and closes with related work and the exact assurance boundary. 2
Background and Problem Separation
The protocol composes established control mechanisms, but its decision object is distinct: whether one authorization root can still cause a new protected commit after a particular durable cut. Table 1 states the evidence supplied by adjacent mechanisms and the remaining fact needed for that decision. 2.1
Cancellation is a request, not a closure proof
Long-running task protocols correctly permit cancellation to be cooperative. The current MCP Tasks specification treats cancellation as an eventually consistent task-state operation, and A2A specifies an attempt to cancel rather than a guarantee that all underlying execution has ceased [1, 18]. This design is necessary for remote work that has already entered a provider lifecycle or
4
Zhu and Wang
Table 1. Adjacent observations and the root-scoped quiescence decision. Observation mechanism
or
What it establishes
What remains for root-scoped quiescence
Cancellation ac- a task endpoint accepted or attempted a knowledgement cancellation-state transition
whether underlying work, descendants, prepared effects, and transferred messages can still commit Process exit one observed process terminated whether authority escaped into remote tasks, credentials, triggers, queues, or provider state Token revocation a named token is no longer accepted un- derived credentials, cached authorization, der the issuer’s revocation semantics already accepted work, and effects not mediated by that token Exact delegation- the authority consequences of removing obligations and carrier effects already edge revocation a selected graph edge emitted before or across the revocation cut Provider-local one adapter’s registered local frontier is compatible cut identity, complete effect closure closed at its fence and watermark provider coverage, and messages crossing between leaves Closure-evidence submitted evidence satisfies a declared execution of the root cut, provider actuverifier closure predicate ation, and distributed collection of compatible leaf evidence Distributed termi- a computation is passive and its modeled a root-specific authority cut, multination detection channels contain no messages root preservation, and operation-time provider fences Root-scoped quies- a complete compatible cutset accounts global business completion, rollback, or cence certificate for cut-relevant old-atom pre-fence ac- effects outside the declared mediation ceptances and excludes future protected boundary acceptance under one retired root atom
crossed an irreversible boundary. It also means that the acknowledgement is an input to quiescence, not the quiescence certificate itself. The distinction is phase-sensitive. A proposed task can often be discarded; an accepted task may already own durable queue state; an executing task may have delegated credentials; and a completing task may be racing with a protected commit. Emerging agent-infrastructure guidance likewise distinguishes revocation semantics across task phases rather than treating a transport close as task termination [21]. The protocol records these states as authority carriers and obligations and closes them at the sink that can still accept an effect. Empirical work on agent-framework stop controls has demonstrated cancellation orphans, timeout zombies, replayed execution, and sibling leakage, and places effect enforcement outside the agent runtime [12]. That result establishes the enforcement gap and the value of an external gate. Our decision object adds a root-selected, multi-provider cut, exact cross-provider carrier accounting, and explicit preservation of independently authorized shared work. 2.2
Credential revocation and bounded expiry
OAuth token revocation names a concrete credential and gives clients a standard way to request invalidation [16]. Short-lived or heartbeat-renewed credentials can further bound how long authority survives a lost controller [7]. Usage control treats ongoing authorization, obligations, conditions, and mutable attributes as first-class parts of long-lived access, rather than reducing control to the
Authorization Revocation for Long-Running AI Agents
5
initial request decision [20]. Time-bounded leases likewise make continued rights conditional on an explicit term and fault model [10]. These mechanisms are effective leaf actuators when every use is mediated by the relevant issuer and when derived credentials and accepted operations are covered. Root-scoped quiescence quantifies over the larger consequence graph. A token may have created another token, authenticated a durable job, or authorized a prepare that no longer consults the token at commit. Revoking the initiating credential therefore closes one carrier, not necessarily the entire root cut. The protocol accepts revocation and expiry receipts as local closure evidence while retaining every uncovered descendant, accepted operation, or ambiguous completion as open or unknown. 2.3
Revocation graphs and multiple roots
Graph revocation asks which principals and rights cease to be authorized when an edge or grant is removed. Classical trust-management work models policy changes as explicit state transitions, classifies the semantics of revocation, and gives formal or rule-based accounts of distributed delegation [3, 11, 14, 37]. Exact revocation must preserve authority supported by an alternate valid path; VERA makes this edge-precise objective explicit [15]. Residual-authorization analyses show why current reachability alone can be insufficient when the correct revocation result depends on authorization history [5]. The protocol adopts the alternate-path requirement and extends the decision object along the time and effect dimensions. For each live instance it records an antichain of minimal sufficient root-support sets and a selected witness. Retiring atom 𝑎𝑐 does not delete an instance whose authority can be justified without 𝑎𝑐 ; instead, continued use requires an atomic rebind to a witness that excludes 𝑎𝑐 . The protocol then accounts for obligations and carriers already emitted under the old selection. Thus graph reachability determines who may continue, while cut and frontier evidence determines whether old-root effects can still arrive. 2.4
Provider effect closure and evidence closure
Provider-local closure systems reason directly about durable external effects. The provider-boundary effect-closure model, for example, characterizes future-use, instance, and lineage closure and exposes a provider-local effect frontier [30]. Such a certificate is a natural provider-frontier leaf: it can attest that a registered provider adapter installed the named fence and closed every item in its local coverage manifest. Local closure is not compositional without a shared cut. Suppose provider 𝑃 reports an empty outbound queue immediately before sending a message, and provider 𝑄 reports an empty inbound queue immediately before accepting it. Both local snapshots can be individually true while the composed system still contains a live cross-provider obligation. The protocol therefore binds every leaf to the same root and epoch, records typed SEND and terminal ACK channel facts, and requires exact token-projected cross-leaf accounting before issuing a global certificate. Bounded Agent Closure (BAC) organizes closure evidence for authority, execution, commitment, and operational state and verifies submitted evidence against a declared closure specification [13]. That verification problem is complementary to the execution protocol here. The protocol establishes the root cut, actuates provider fences, collects leaf evidence, and constructs a consistent distributed cut; a closure verifier can validate the resulting evidence object. Keeping these roles separate makes the trusted boundary explicit: orchestration cannot replace evidence, and evidence validation cannot by itself perform shutdown.
6
2.5
Zhu and Wang
Distributed termination detection
Classical termination detection asks when all participating processes are passive and no computation message remains in transit. Dijkstra–Scholten accounts for diffusing computation, Mattern treats asynchronous and non-FIFO communication through message-counting algorithms, and consistentsnapshot techniques make the channel-state problem explicit [4, 8, 17]. The protocol uses the same core lesson: local emptiness is insufficient when messages cross a cut. Authorization quiescence nevertheless differs from computational termination. A process may remain active under an independent root after the target root is quiescent; conversely, all processes may be passive while a durable credential, cron trigger, or prepared provider effect remains able to commit. The relevant unit is therefore a root-selected authority and effect path, and the barrier is enforced at protected sinks rather than inferred solely from process states. 2.6
Three-valued completion
The protocol reports one of three outcomes. Quiescent means the complete registered cutset satisfies the certificate predicate. Not-Quiescent means sound evidence identifies a live authority, obligation, carrier, or unmatched channel token. Indeterminate means the result cannot be proved because coverage, fence installation, state observation, or evidence consistency is missing. This distinction prevents a timeout, partition, stale cache, or opaque endpoint from being interpreted as successful shutdown. 3 3.1
System, Threat, and Assurance Model Assurance statement
We study shutdown of one authorization root while a long-running agent may have delegated work across heterogeneous runtimes and providers. The property is deliberately root-relative and has two distinct enforcement stages. A linearized root-ledger cut retires root-epoch atom 𝑎 and immediately prevents issuer-side creation or expansion of authority under 𝑎. Each effect provider then installs its own locally ordered barrier. An already authorized carrier can reach a provider before that barrier, including after the root-ledger cut; such an acceptance is admissible only when an exact typed receipt places it before the provider barrier and the corresponding future-use frontier is closed. A certificate establishes that all required barriers are installed, all such acceptances are accounted for, and no extension can create a new protected-effect commitment relying on 𝑎. Work supported by a different current root may continue, and an effect already accepted before its local barrier may settle. The certificate therefore means neither that every process has exited nor that previously committed or physical consequences have been undone. It is a positive, mechanically checkable statement about the absence of residual commit authority from the named root within the declared enforcement boundary. The distinction between a request acknowledgement and this assurance is fundamental. A runtime may acknowledge cancellation while a queued message, delegated credential, scheduled trigger, webhook, reservation, or provider operation remains able to cross its commitment point. Root-scoped quiescence requires an authority cut, complete carrier coverage, provider-local effect closure, and exact accounting for handoffs between covered endpoints. 3.2
Components and enforcement boundary
The system contains five logical components. They may be co-located, but their evidence roles remain distinct. (1) The root ledger stores authenticated grants, monotonically increasing root epochs, shutdown cuts, and root phases. It is the linearization authority for retiring a root-epoch atom.
Authorization Revocation for Long-Running AI Agents
7
(2) The shutdown coordinator freezes the coverage manifest for a cut, requests endpoint fences, reconciles cross-endpoint channel tokens, and composes leaf evidence. It cannot declare quiescence by fiat. (3) A runtime adapter enumerates the root-dependent carriers under its endpoint, preserves their support provenance, and closes, terminalizes, or rebinds each carrier through a registered transition. (4) A provider/effect adapter places a monotone fence at the authorization-sensitive commitment boundary and emits a provider-local frontier certificate. The frontier orders accepted commitments relative to that provider’s local barrier; it does not compare heterogeneous provider sequence numbers with the root-ledger sequence. (5) An independent verifier checks signatures, epochs, manifest coverage, leaf compatibility, support witnesses, fence and log watermarks, and channel-token conservation before returning QUIESCENT, NOT_QUIESCENT, or INDETERMINATE.
A carrier is any durable or live object that can preserve, transmit, or exercise authority: a task, child process, delegated credential, session, queue record, timer, cron entry, webhook, reservation, retry record, or provider operation. A channel token names one cross-endpoint handoff. The distinction prevents a local scan from treating an emitted but not yet accounted-for message as absence of work. A protected-effect commitment is the registered point after which an effect can proceed without another authorization decision. Provider profiles locate this point; later delivery or settlement is not misclassified as a new authorization event. The enforcement boundary is declared by a versioned manifest. It lists every runtime endpoint, provider adapter, effect sink, channel class, and profile digest reachable by work selected under the named retired root-epoch atom. Dynamic carriers need not all exist when shutdown begins: their creation events and incoming channel tokens must be covered by a manifest endpoint and by the stable-scan watermark in its leaf certificate. An endpoint lacking a registered enumeration, fence, or frontier mechanism remains visible as indeterminate; it cannot be silently omitted.
3.3
Adversary and fault model
The adversary controls the agent’s planning and every cooperating descendant whose behavior is not part of the trusted enforcement boundary. It may create deep delegation chains, select one of several authorization roots, move work between endpoints, schedule delayed callbacks, retain renewable credentials, and race cancellation against commitment. It may delay, duplicate, reorder, or replay messages; crash a coordinator or adapter at any instruction boundary; exploit stale cancellation acknowledgements; present incomplete or conflicting inventories; and attempt to relabel root-dependent work as independently authorized. Providers and networks may be unavailable or partitioned for an unbounded interval. The adversary cannot forge signatures or collision-resistant digests, rewrite a committed rootledger record, violate the atomicity of a registered fence or rebind transaction, or produce a protected commitment outside every manifested mediation point. These are explicit assurance premises rather than properties inferred from agent cooperation. Compromise of a trusted commit gateway, provider fabrication of authenticated frontier evidence, and an effect path absent from the registered manifest are outside the theorem domain; each is addressed operationally by profile admission and manifest audit rather than by interpreting missing evidence as success.
8
3.4
Zhu and Wang
Assurance assumptions
Table 2 gives the complete premises used by the safety results. Assumptions A1–A9 are safety premises. A10–A11 are needed only for the convergence result; safety remains fail-closed during a partition or permanent provider failure. 3.5
Assets, attack goals, and verdict discipline
The protected asset is the ability to create a new protected-effect commitment using the named retired root-epoch atom. The adversary succeeds if it causes any of the following while a verifier returns QUIESCENT: • an accepted commitment locally ordered after its sink barrier whose selected authorization witness contains the retired root-epoch atom; • a cut-relevant acceptance under the retired atom, ordered before its local fence, lacking an exact PRE_FENCE_COMMITTED receipt and closed provider frontier; • a root-dependent carrier omitted from every compatible leaf; • a cross-endpoint handoff omitted, duplicated, or accepted into an uncovered destination carrier; • a pre-fence commitment used as cover for an additional post-fence effect; • a nominal rebind whose replacement witness still depends on the retired atom, uses a stale root, or lacks an independent authorization decision; or • a certificate composed across different cuts, manifest roots, adapter-profile epochs, or conflicting leaf versions. Verdicts separate a demonstrated blocker from an evidence gap. NOT_QUIESCENT records a verified open carrier, in-flight token, post-barrier commitment, or other concrete counterexample. INDETERMINATE records missing, stale, opaque, or conflicting evidence when no verified counterexample is available. Only QUIESCENT is a release certificate. Neither of the other verdicts is converted to success by timeout, retry exhaustion, majority vote, or an agent’s assertion that it has stopped. The certified statement covers the shutdown generation initiated by the named cut and the locally ordered sink evidence composed for that generation. It does not promise application-level goal completion, global infrastructure idleness, cancellation of work supported solely by other roots, rollback of a pre-fence commitment, erasure of information already observed, or reversal of a physical-world consequence. These exclusions make the certificate’s subject precise: within the declared profile, the retired atom has no residual path to a new protected-effect commitment. 4
Formal Model
This section defines the object named by a root-scoped quiescence certificate, the evidence required to establish it, and nine results used throughout the paper. Proofs appear in Appendix A. 4.1
Root-epoch atoms and machine state
Let R be the set of root identifiers and let 𝐻 be a collision-resistant digest over an injective, length-delimited canonical encoding. A root-epoch atom is 𝑎 = ⟨𝑟, 𝑒, ℎ𝑔 ⟩ ∈ A, where 𝑟 ∈ R, 𝑒 ∈ N is the root epoch, and ℎ𝑔 is the digest of the authenticated grant. Write rid(𝑎) = 𝑟 and rid(𝑊 ) = {rid(𝑎) : 𝑎 ∈ 𝑊 }. Root atoms are not bearer strings. An atom is current for a new issuer decision only when the root ledger contains the same grant digest and epoch in phase ACTIVE. A carrier authorized before retirement can still hold that exact atom while the distributed
Authorization Revocation for Long-Running AI Agents
Table 2. Assurance assumptions for a registered quiescence profile. ID
Assumption
Enforced obligation
A1
Issuer mediation and non-expansion
A2
Authentic canonical evidence
A3
Durable root linearization
A4
Support-provenance completeness
A5
Per-sink fence and frontier soundness
A6
Registry and manifest completeness
A7
Exact channel accounting
A8
Atomic rebind
A9
Crash-safe monotonicity
A10
Eventual evidence stabilization
A11
Finite drain and fair delivery
Every transition that issues, delegates, reactivates, or enlarges authority under a root crosses the manifested root issuer and validates the exact root-epoch atom at its root-ledger linearization point. This premise does not treat exercise by an already authorized carrier as a new issuance. Grants, root atoms, support records, cuts, manifests, fences, channel dispositions, rebind receipts, frontier statements, and certificates use unambiguous canonical encodings and unforgeable authenticators. A cut retiring epoch 𝑒, the advance to 𝑒 + 1, the phase transition, the frozen manifest, and the exact cut-target token frontier commit atomically in a serializable durable ledger; epochs never decrease and a retired atom is never reactivated. The root transaction does not itself install a provider fence. Every carrier and handoff records all policy-relevant minimal authorization supports, the witness actually selected for its current authority, and authenticated parent-to-child provenance. Omission or ambiguity yields an unknown carrier. Every manifested effect sink 𝑝 serializes commitment admission with a durable local barrier 𝑏𝑝 (𝑐 ). The barrier causally follows authenticated observation of cut 𝑐, rejects every later local attempt selected under the retired atom, and yields a frontier that completely enumerates every cut-relevant acceptance under that atom that was outstanding when 𝑐 committed or was admitted from a dependent carrier before 𝑏 𝑝 (𝑐 ), while closing each such commitment’s future-use, instance, and lineage frontier. The frozen manifest covers every runtime, provider, effect sink, and channel class reachable from work selected under the retired atom. Stable scans include all carrier creation and transition events through their stated watermarks. Each cross-endpoint handoff has a globally unique, retry-stable token whose sole authoritative creation event is SEND(𝑡 ). For the retired atom, SEND(𝑡 ) ≺ 𝑐 and the token belongs to the exact frontier frozen by 𝑐. Exactly one authenticated terminal disposition—accepted into a covered carrier, rejected by a fence, or expired under an enforced deadline—has the same canonical token projection; acceptance precedes destination-terminal accounting. One atomic transition preserves the exact operation and effect-envelope digests, selects a complete current support witness excluding the retired atom, installs its fresh root-epoch atoms, and emits a single-use receipt binding those facts. Cut, fence, carrier, channel, and certificate records are durably ordered; an exact retry requires the same request identifier and canonical candidate digest, conflicting identifier/body reuse or certificate reminting is rejected, and recovery never rolls back an epoch, fence, terminal disposition, or closed frontier. For the liveness theorem, every required sink eventually installs its barrier; every manifested runtime/provider endpoint eventually returns a stable scan and the required frontier or authenticated terminal evidence; every transient pre-certification unknown or state disagreement is eventually resolved. An authenticated same-key equivocation is never cleared in place: the generation remains indeterminate unless policy starts a new generation under a fresh evidence key. For the liveness theorem, the cut has finitely many dependent carriers, effects, and tokens; issuer transitions cannot create or expand authority under the retired atom after the cut; every emitted token is eventually delivered to a covered destination or obtains an authenticated fence-reject or enforced-expiry disposition; and every enabled fence, close, typed terminal disposition, or valid rebind action is eventually taken.
9
10
Zhu and Wang
generation drains; its subsequent effect admission is governed by the relevant provider-local barrier, not by reinterpreting the root cut as an atomic cross-provider fence. The security-relevant machine state is 𝑆 = ⟨𝐴, 𝐶, 𝑋,𝑇 , 𝐹, 𝐾, 𝐿, 𝑀, 𝑃⟩. Here 𝐴 is the root ledger; 𝐶 the cut ledger; 𝑋 the carrier registry; 𝑇 the channel-token ledger; 𝐹 the endpoint fence map; 𝐾 the provider commitment/frontier state; 𝐿 an authenticated event log; 𝑀 the registered coverage manifests; and 𝑃 the versioned adapter profiles. Security-changing transitions are serialized within their respective durable domains and use durable idempotency keys. Let ⪯𝑟 be the root ledger’s durable order and, for every endpoint or effect sink 𝑝, let ⪯𝑝 be its durable local admission/log order. Write ≺𝑟 and ≺𝑝 for their strict parts. The global causal relation ≺ is the transitive closure of local durable order, authenticated program order, send-before-accept edges, and observation edges from a committed record to a transition that authenticates that record. Thus events in different durable domains are compared only through ≺, never by comparing their implementation-specific sequence numbers. We use 𝜈𝑑 (𝑜) solely as the local position of event 𝑜 within durable domain 𝑑; in particular, 𝜈𝑟 and 𝜈 𝑝 are positions within ⪯𝑟 and ⪯𝑝 . Definition 1 (Linearized root cut). For a current atom 𝑎𝑐 = ⟨𝑟, 𝑒, ℎ𝑔 ⟩, BeginShutdown(𝑟, 𝑚) commits 𝑐 = ⟨𝑐𝑖𝑑, 𝑎𝑐 , 𝑒 + 1, 𝜈𝑟 (𝑐), ℎ𝑚 , ℎ𝑃 , ℎ𝑇 ⟩ at root-ledger position 𝜈𝑟 (𝑐). The same transaction retires epoch 𝑒 by marking 𝑎𝑐 retired, advances 𝐴(𝑟 ) to the new epoch 𝑒 + 1 in phase DRAINING, and freezes manifest digest ℎ𝑚 = 𝐻 (𝑚), profile digest ℎ𝑃 , and exact cut-target token-frontier digest ℎ𝑇 = 𝐻 (𝑇𝑐 ). The frontier 𝑇𝑐 is defined below from authoritative pre-cut SEND records. Advancing the counter does not issue a successor grant; a later active atom requires a separately authenticated grant transition. The transaction neither revokes the state of a previously authorized carrier nor installs a barrier in any provider domain. Let I𝑟 contain the issuer events that issue, delegate, reactivate, or enlarge authority under root 𝑟 . A1 requires every 𝑖 ∈ I𝑟 to validate its complete selected witness at its own root-ledger linearization point. By contrast, a protected effect has a registered provider-local commitment-admission event 𝑘. For 𝑘 at sink 𝑝, 𝜈 𝑝 (𝑘) is the last mediated local decision after which the effect can proceed without another authorization decision. A settlement, delivery, or physical consequence following 𝑘 is part of the same commitment, not a fresh commitment. We write 𝑎 ∈ auth(𝑘) when the exact selected authorization witness recorded for 𝑘 contains atom 𝑎. 4.2
Minimal support and selected authorization
A carrier may have conjunctive requirements and alternative roots. Treating its roots as a flat union would over-revoke independently authorized work; treating them as an existential set would permit root laundering. Definition 2 (Support antichain). For carrier 𝑥 in state 𝑆, its support antichain is a finite family Σ𝑆 (𝑥) ⊆ 2 A such that every 𝑊 ∈ Σ𝑆 (𝑥) is a sufficient conjunctive authorization witness and no distinct 𝑊 ,𝑊 ′ ∈ Σ𝑆 (𝑥) satisfies 𝑊 ⊂ 𝑊 ′ . The antichain contains all policy-relevant minimal witnesses admitted by the registered derivation profile. The durable field sel𝑆 (𝑥) ∈ Σ𝑆 (𝑥) records the witness actually selected for the carrier’s current authority. Let Current𝑆 (𝑥,𝑊 ) hold when every atom in 𝑊 is current and the authenticated derivation edges joining those atoms to 𝑥 remain valid. A selected witness is an authorization fact, not a planner hint.
Authorization Revocation for Long-Running AI Agents
11
New issuer decisions require Current𝑆 (𝑥, sel𝑆 (𝑥)); effect admission by an already authorized carrier instead presents the exact selected witness to the sink’s barrier rule. This separation preserves the race interval between the root cut and provider fence as explicit evidence rather than assuming it away. For cut 𝑐, let 𝐷𝑐 be the least provenance-closed set containing each carrier present when 𝑐 commits whose selected witness contains 𝑎𝑐 and each carrier later materialized by delivery or acceptance of an outstanding token 𝑡 ∈ 𝑇𝑐 whose support witness contains 𝑎𝑐 . The closure includes these pre-cut transfers when they are delivered or accepted before the corresponding channel or ingress barrier, even if acceptance occurs after the root-ledger cut. A carrier leaves 𝐷𝑐 only by a terminal/effect-closed transition or by the atomic rebind of Definition 3; relabeling a field does not remove the dependency. 𝑝 For each manifested sink 𝑝, let 𝐾𝑐 be the cut-relevant commitment set: every not-yet-closed commitment authorized by 𝑎𝑐 and outstanding at 𝑝 when 𝑐 commits, together with every commitment admitted from a member of 𝐷𝑐 before 𝑏 𝑝 (𝑐). A historical commitment whose future-use, instance, and lineage frontier was already authenticated as closed before 𝑐 is not reopened merely to 𝑝 populate 𝐾𝑐 . This scope captures cut-time provider state and cut-to-barrier races without requiring an unbounded replay of all effects ever admitted under epoch 𝑒. Definition 3 (Atomic independent rebind). Let 𝑜𝑝𝑥 and 𝑒𝑛𝑣 𝑥 be the carrier’s canonical remaining operation and effect envelope. They are immutable across a rebind. Rebind(𝑥,𝑊 ′, 𝑐) is admissible only if 𝑊 ′ ∈ Σ𝑆 (𝑥), 𝑎𝑐 ∉ 𝑊 ′ , Current𝑆 (𝑥,𝑊 ′ ). ′ We call such a 𝑊 an independent support: it excludes the retired atom 𝑎𝑐 . A witness using a different root identifier is the common alternate-root case, not a requirement of the definition. It re-runs the registered authorization decision for 𝑥, atomically changes sel(𝑥) and the carrier authorization epoch while preserving the exact 𝑜𝑝𝑥 and 𝑒𝑛𝑣 𝑥 , and emits a single-use receipt 𝜌𝑥 = Sig(𝑐𝑖𝑑, 𝑥𝑖𝑑, 𝐻 (sel𝑜𝑙𝑑 ), 𝐻 (𝑊 ′ ), 𝐻 (𝑜𝑝𝑥 ), 𝐻 (𝑒𝑛𝑣 𝑥 ), ℎ𝑃 , 𝜈 𝑋 (𝜌𝑥 )). No descendant inherits the rebind merely from ancestry; it must either be covered by the same atomic profile transition or carry its own receipt. 4.3
Carriers, manifests, and channel conservation
A carrier record is 𝑥 = ⟨𝑥𝑖𝑑, 𝑘𝑖𝑛𝑑, 𝑒𝑛𝑑𝑝𝑜𝑖𝑛𝑡, Σ(𝑥), sel(𝑥), 𝑜𝑝𝑥 , 𝑒𝑛𝑣 𝑥 , 𝑝𝑎𝑟𝑒𝑛𝑡𝑠, 𝑠𝑡𝑎𝑡𝑒, 𝑓 𝑟𝑜𝑛𝑡𝑖𝑒𝑟, 𝑒𝑝𝑜𝑐ℎ⟩, where 𝑠𝑡𝑎𝑡𝑒 ∈ {OPEN, EFFECT_CLOSED, PRE_FENCE_COMMITTED, REBOUND, TERMINATED, UNKNOWN}. For an accepted commitment 𝑘 at sink 𝑝, a typed pre-fence receipt is pfc
𝜌 𝑝,𝑘 = Sig𝑝 ⟨𝑐𝑖𝑑, 𝑝, 𝑘𝑖𝑑, 𝐻 (auth(𝑘)), 𝐻 (𝑜𝑝𝑘 ), 𝐻 (𝑒 𝑓 𝑓 𝑒𝑐𝑡𝑘 ), 𝜈 𝑝 (𝑘), 𝜈 𝑝 (𝑏 𝑝 (𝑐)), 𝑠 𝜌 , ACCEPTED_BEFORE_FENCE, ℎ𝑃 ⟩. It verifies jointly with the cut’s authenticated fence record only if 𝑎𝑐 ∈ auth(𝑘), the complete selected witness and the operation and effect digests match the admitted request, the admission and pfc barrier occur in the same durable domain, 𝑘 ≺𝑝 𝑏 𝑝 (𝑐) ≺ 𝜌 𝑝,𝑘 , both local positions have authenticated log inclusion, and 𝑠 𝜌 is the durable receipt-record position. Thus the receipt is finalized only after it can bind the installed barrier; it may account for either a cut-time outstanding acceptance or a cutto-barrier acceptance. State PRE_FENCE_COMMITTED means that every authorization-sensitive
12
Zhu and Wang
commitment associated with the carrier has exactly one such receipt, is named in the provider frontier, and cannot be extended into an additional commitment. It never reclassifies a post-barrier acceptance. A manifest 𝑚 = ⟨𝐸, 𝑄, 𝐺, Π, 𝜂𝑚 ⟩ names runtime/provider endpoints 𝐸, cross-endpoint channel classes 𝑄, commit gateways 𝐺, registered adapter profiles Π, and the manifest epoch 𝜂𝑚 . Its completeness judgment Complete(𝑚, 𝑎𝑐 ) states that every commitment path reachable from 𝑎𝑐 crosses a named gateway and every carrier or handoff on such a path is enumerable by a named endpoint/channel profile. This judgment is an authenticated profile-admission fact checked when the manifest is frozen. Consequently the named gateways and their barriers hit every registered directed commitment path reachable from 𝑎𝑐 ; we call this manifested hitting set the 𝑎𝑐 -relative path cutset. Each handoff has a retry-stable token 𝑡 = ⟨𝑡𝑖𝑑, 𝑠𝑟𝑐, 𝑑𝑠𝑡, 𝑐𝑙𝑎𝑠𝑠, 𝐻 (𝑝𝑎𝑦𝑙𝑜𝑎𝑑), 𝐻 (𝑊𝑡 ), 𝑠𝑒𝑞⟩. An origin endpoint emits exactly one SEND(𝑡). A destination or gateway emits exactly one terminal acknowledgement ACK(𝑡, 𝑑),
𝑑 ∈ {ACCEPT(𝑥), FENCE_REJECT, ENFORCED_EXPIRY}.
For ACCEPT(𝑥), the destination leaf must cover 𝑥 and the accepted carrier’s support projection must include 𝑊𝑡 . Fence rejection and expiry are valid only when the corresponding enforcement evidence is bound to the cut. The SEND(𝑡) record is the sole authoritative token-creation event. For a handoff with 𝑎𝑐 ∈ 𝑊𝑡 , A1 and A7 require SEND(𝑡) ≺ 𝑐. The cut atomically freezes the exact registered old-atom token multiset Ú 𝑇𝑐 = {𝑡 }, 𝑡 : 𝑎𝑐 ∈𝑊𝑡 SEND(𝑡 ) ≺𝑐
where each singleton is a one-element multiset and global token uniqueness makes every multiplicity one. Its digest is ℎ𝑇 . Transport may later deliver an already named token, but it cannot mint or backfill a new old-atom token after the cut. For an accepted handoff, the causal order is SEND(𝑡) ≺ ACK(𝑡, ACCEPT(𝑥)) ≺ TerminalAccount(𝑥). Because SEND(𝑡) and ACK(𝑡, 𝑑) have different types, define the canonical token projection 𝜋𝑡 (SEND(𝑡)) = 𝑡,
𝜋𝑡 (ACK(𝑡, 𝑑)) = 𝑡,
and extend 𝜋𝑡 elementwise to multisets. Equality of projected multisets, together with uniqueness and disposition validity, detects both loss and duplication without equating heterogeneous records. 4.4
Endpoint fences and leaf certificates
For cut 𝑐, endpoint fence 𝑓𝑝 (𝑐) contains a provider-local barrier event 𝑏 𝑝 (𝑐) that binds the retired atom, local profile epoch, and durable fence/log watermark. The adapter authenticates the root cut before installing the barrier, giving the causal edge 𝑐 ≺ 𝑏 𝑝 (𝑐). Every commitment admission at 𝑝 is comparable with 𝑏 𝑝 (𝑐) in ⪯𝑝 : an accepted admission authorized by 𝑎𝑐 must satisfy 𝑘 ≺𝑝 𝑏 𝑝 (𝑐), while every attempt with 𝑏 𝑝 (𝑐) ≺𝑝 𝑘 and 𝑎𝑐 ∈ auth(𝑘) is rejected. A request that straddles cut propagation is classified solely by this local admission order. No comparison is made between 𝜈𝑟 (𝑐) and 𝜈 𝑝 (𝑘). A stable scan begins after the fence and covers every carrier and channel transition 𝑝 through its stated watermark; the provider frontier binds every commitment in 𝐾𝑐 visible at that boundary.
Authorization Revocation for Long-Running AI Agents
13
Definition 4 (Leaf certificate). A leaf from endpoint 𝑝 is the authenticated tuple ℓ𝑝 = Sig𝑝 ⟨𝜒, 𝑠𝑐𝑜𝑝𝑒𝑝 , 𝜔 𝑝 , 𝜇𝑝 , 𝑓𝑝 , 𝑂 𝑝 , 𝐵𝑝 , 𝑅𝑝 , 𝐽𝑝 , 𝑈𝑝 , 𝑣 𝑝 , 𝑑𝑝 ⟩. The compatibility header 𝜒 = ⟨𝑐𝑖𝑑, 𝑎𝑐 , ℎ𝑚 , ℎ𝑃 , ℎ𝑇 ⟩ binds the cut, atom, manifest, profile family, and frozen token frontier. 𝑠𝑐𝑜𝑝𝑒𝑝 is the endpoint’s manifest slice; 𝜔 𝑝 is its evidence-through boundary; 𝜇𝑝 its stable-scan and log-root evidence; 𝑓𝑝 its fence/frontier evidence; 𝑂 𝑝 the multiset of authenticated SEND records; 𝐵𝑝 the multiset of authenticated terminal ACK records; 𝑅𝑝 rebind receipts; 𝐽𝑝 typed pre-fence commitment receipts; 𝑈𝑝 unknown/conflict facts; 𝑣 𝑝 ∈ {𝑄, 𝑁 , 𝑈 } its local verdict; and 𝑑𝑝 the digest of the canonical evidence snapshot projected through 𝜔 𝑝 , whose preimage excludes 𝑑𝑝 and the outer signature. The leaf-record event causally follows 𝜔 𝑝 , and every referenced barrier, typed receipt, rebind, and terminal acknowledgement is recorded no later than 𝜔 𝑝 . A leaf is locally 𝑄 exactly when its manifest slice and stable scan are complete, its fence and 𝑝 pfc provider frontier verify, 𝑈𝑝 = ∅, and 𝐽𝑝 contains exactly one valid 𝜌 𝑝,𝑘 for every 𝑘 ∈ 𝐾𝑐 preceding 𝑏 𝑝 (𝑐) and no receipt for a post-barrier acceptance. In addition, every 𝑥 ∈ 𝐷𝑐 in its slice is one of: (1) EFFECT_CLOSED or TERMINATED; (2) PRE_FENCE_COMMITTED with exact ordered receipts and a matching closed frontier; or (3) REBOUND with a valid receipt to a current witness that excludes 𝑎𝑐 . An authenticated OPEN carrier or accepted post-barrier commitment is a local 𝑁 witness. A leaf exports its sends and terminal acknowledgements but does not decide channel closure in isolation; that decision requires the composite multiset. Missing, stale, opaque, or conflicting evidence without a concrete blocker produces 𝑈 . 4.5
Composition and three-valued decision
Let a partial evidence object be a finite map from manifest leaf identifiers to leaf digests and bodies, together with a conflict marker. Define 𝐸 1 ⊔ 𝐸 2 by keywise union: an absent entry takes the present value; identical entries collapse; two different authenticated values for one key produce the conflict marker. Objects with different compatibility headers also conflict. This definition makes retries idempotent while preserving equivocation evidence. For compatible evidence 𝐸, write Ú Ú 𝑂 (𝐸) = 𝑂𝑝 , 𝐵(𝐸) = 𝐵𝑝 . ℓ𝑝 ∈𝐸
ℓ𝑝 ∈𝐸
Covered(𝐸, 𝑚) holds when the leaf scopes form exactly the required manifest coverage (overlap is allowed only when the manifest declares the same replicated evidence key). ChannelsClosed(𝐸) holds, relative to the cut in the compatibility header, when the projected sends are exactly the frozen frontier, every send precedes the cut, and every send has exactly one valid terminal acknowledgement. Equivalently, token identifiers and multiplicities reconcile under 𝜋𝑡 (𝑂 (𝐸)) = 𝑇𝑐 = 𝜋𝑡 (𝐵(𝐸)), and every accepted token maps to a covered destination carrier. The predicate does not assert equality between SEND and ACK records themselves. Definition 5 (Composite verdict). The verifier computes 𝑉𝑐 (𝐸) as follows. (1) Return 𝑁 if verified evidence contains a concrete open root-dependent carrier, an unacknowledged emitted token under a complete scan, an accepted commitment 𝑘 with 𝑏 𝑝 (𝑐) ≺𝑝 𝑘 and 𝑎𝑐 ∈ auth(𝑘), or an accepted cut-relevant pre-fence commitment for which a complete authenticated scan establishes that its exact ordered receipt or closed frontier is absent.
14
Zhu and Wang
(2) Otherwise return 𝑈 if the header conflicts, the manifest or any leaf scope is absent, a signature/profile/watermark is stale, any leaf is unknown, an endpoint is opaque, or channel conservation cannot be proved. (3) Otherwise return 𝑄 if every leaf is locally 𝑄, all fences and frontiers verify, coverage is complete, and channels are closed. The priority of 𝑁 preserves a known counterexample even when other evidence is unavailable. Let 𝝎 𝐸 be the canonical map from each manifested leaf identifier to its local evidence-through boundary 𝜔 𝑝 , ordered by leaf identifier; it reduces to one sequence in a single-ledger profile. Define the pre-certificate candidate body B𝑞 = ⟨𝑐𝑖𝑑, 𝑟, 𝑒, ℎ𝑚 , 𝝎 𝐸 , 𝐻 (𝐸)⟩,
ℎ𝑞 = 𝐻 (B𝑞 ).
The canonical preimage B𝑞 excludes the request identifier 𝑞𝑖𝑑, its own digest ℎ𝑞 , issuance metadata, and the outer signature. Let 𝑠𝑐 be the verifier-ledger position reserved by the atomic issuance transaction. Only 𝑄 authorizes issuance of C𝑐 = Sig𝑉 ⟨𝜒, 𝑞𝑖𝑑, ℎ𝑞 , 𝐻 (𝐸), 𝐻 (𝑂 (𝐸)), 𝐻 (𝐵(𝐸)), 𝑠𝑐 , QUIESCENT⟩. Certificate issuance is keyed by the canonical request identifier 𝑞𝑖𝑑 and the pre-certificate body digest ℎ𝑞 . After the issuance record (𝑐𝑖𝑑, 𝑞𝑖𝑑, ℎ𝑞 , 𝐻 (𝐸), 𝑠𝑐 , C𝑐 ) commits, an exact retry with the same 𝑞𝑖𝑑 and ℎ𝑞 returns the identical C𝑐 . A different request identifier for the completed cut, or reuse of 𝑞𝑖𝑑 with a different body, is a conflicting remint and is rejected rather than signed. Definition 6 (Root-relative authorization qiescence). A trace is quiescent for cut 𝑐, written 𝑝 RQ(𝑐), when, for every manifested sink 𝑝, 𝑐 ≺ 𝑏 𝑝 (𝑐), every accepted commitment 𝑘 ∈ 𝐾𝑐 with 𝑎𝑐 ∈ auth(𝑘) satisfies 𝑘 ≺𝑝 𝑏 𝑝 (𝑐) pfc
and has an exact 𝜌 𝑝,𝑘 in a closed provider frontier, and no accepted commitment whose authorization contains 𝑎𝑐 is ordered after 𝑏 𝑝 (𝑐). At certificate issuance, every carrier 𝑥 ∈ 𝐷𝑐 is effect-closed, terminal, PRE_FENCE_COMMITTED, or independently rebound, and all 𝑎𝑐 -dependent handoffs in the frozen frontier 𝑇𝑐 are terminally accounted for. Monotone barriers make the same no-admission-under-𝑎𝑐 clause hold in every admissible extension of the certified trace. A later certificate cannot erase an intervening post-barrier violation. 4.6
Safety, composition, and progress results
The following nine results characterize the protocol. The first eight are safety or algebraic results and do not assume eventual provider availability. Lemma 1 (Cut issuer non-expansion). Under A1–A3, after BeginShutdown retires 𝑎𝑐 at 𝜈𝑟 (𝑐), no later issuer transition in I𝑟 may issue, delegate, reactivate, or enlarge authority selected under 𝑎𝑐 . The lemma makes no claim that the root cut itself blocks effect admission by an already authorized carrier; that obligation belongs to each 𝑏 𝑝 (𝑐) under A5. Lemma 2 (Support-sound projection). Under A2, A4, A6, and A7, projecting the authenticated provenance graph onto 𝐷𝑐 includes every carrier and accepted handoff whose currently selected authority depends on 𝑎𝑐 . Removing nonselected alternative witnesses does not remove a selected dependency. Lemma 3 (No root laundering by rebind). Under A2, A4, and A8, a carrier leaves 𝐷𝑐 through Rebind(𝑥,𝑊 ′, 𝑐) only if its continuing authority has a complete, current derivation whose selected witness excludes 𝑎𝑐 . Changing labels, parents, or an unselected alternative cannot establish this condition.
Authorization Revocation for Long-Running AI Agents
15
Theorem 1 (Compositional no-false-qiescence). Under A1–A9, if the verifier issues C𝑐 , then RQ(𝑐) holds. In particular, no compatible execution can contain an unreported cut-relevant pre-fence acceptance under 𝑎𝑐 or an accepted post-barrier commitment authorized by 𝑎𝑐 . Theorem 2 (Noncompositionality and opacity boundary). The model entails two boundary consequences: (1) provider-local 𝑄 leaves do not imply composite 𝑄 without exact channel conservation; and (2) if a reachable endpoint exposes neither complete enumeration nor an enforceable fence/frontier, no observer of the remaining evidence can be both sound and complete for root-relative quiescence. The sound verdict for the second case is 𝑈 . Theorem 3 (Independent-support preservation). Suppose 𝑊 ′ ∈ Σ𝑆 (𝑥), 𝑎𝑐 ∉ 𝑊 ′ , and Current𝑆 (𝑥,𝑊 ′ ). A successful atomic rebind to 𝑊 ′ preserves the carrier’s authorization under 𝑊 ′ while retiring 𝑎𝑐 , and the resulting quiescence certificate for 𝑎𝑐 does not revoke any atom in 𝑊 ′ . Theorem 4 (Merge-order independence). On partial evidence objects sharing a compatibility domain, ⊔ is associative, commutative, and idempotent. Consequently the composite digest and verdict are independent of leaf arrival order and duplicate delivery; authenticated disagreement is retained as conflict and therefore cannot yield 𝑄. Theorem 5 (Crash/replay stability and unrelated-root locality). Under A1–A9, crashes and arbitrary replay of committed protocol messages cannot decrease the root epoch, remove a fence, reopen a closed frontier, duplicate a terminal token disposition, reuse a rebind receipt, or turn a non-𝑄 evidence object into 𝑄 without new valid evidence. Moreover, let 𝑟 ′ ∈ R, 𝑟 ′ ≠ 𝑟 , be absent from the frozen manifest dependencies and from rid(𝑊 ) for every selected witness 𝑊 represented in 𝐸. Advancing the epoch of, or shutting down, root 𝑟 ′ does not invalidate C𝑐 . Theorem 6 (Conditional convergence). Under A1–A11, if every carrier in 𝐷𝑐 eventually becomes effect-closed, terminal, PRE_FENCE_COMMITTED, or validly rebound; every transient pre-certification unknown and resolvable state disagreement clears; and no authenticated same-key equivocation occurs, then the protocol eventually obtains all compatible leaves, reconciles every token in the frozen frontier 𝑇𝑐 , and issues C𝑐 . Until those premises hold, the verifier remains 𝑁 or 𝑈 rather than issuing a false certificate. 5
Root-Scoped Quiescence Protocol
The protocol turns a shutdown request into a durable, root-relative security transition. Figure 1 separates the authority cut from provider actuation and evidence checking. The cut ledger is the sole linearization point for retiring an epoch; adapters then install their own barriers, close local frontiers, and return typed leaves. The aggregator never infers local facts from a cancellation response, and the checker never invokes the controller’s decision procedure. 5.1
Step 1: linearize and seal the root cut
For root 𝑟 at epoch 𝑒, BeginShutdown durably records retirement of 𝑎𝑐 = (𝑟, 𝑒, ℎ𝑔 ) and advances the issuer to the new epoch 𝑒 + 1. The record binds a fresh cut identifier, the endpoint/sink/channel manifest version, the policy and adapter profile digests, and the initial graph commitment. The issuer subsequently rejects any authority-issuing, delegating, reactivating, or enlarging transition whose selected support contains 𝑎𝑐 . This operation is atomic at the authority ledger, not across all providers. The distributed shutdown generation remains draining until its registered leaves prove their adapter-specific barriers. An already authorized carrier can still reach an effect sink before that sink’s barrier; the cut neither
16
Zhu and Wang
durable epoch cut ledger
root authority issuer
support compiler and projection
runtime/provider adapters
leaf/cutset aggregator
root-scoped certificate
ingress, channel, and effect-frontier barriers
independent evidence checker
Fig. 1. Protocol separation. The root cut retires issuer-side creation and expansion of old-epoch authority; adapter-specific barriers and frontier leaves establish local facts; exact cutset aggregation establishes the composed predicate; a separately implemented checker validates the evidence object.
𝐴
selec
ted
𝐴 𝑥 alt 𝑥 and le
𝐵
lab avai
𝐵 {{𝐴}, {𝐵}}: explicit 𝐴 → 𝐵 rebind
{{𝐴, 𝐵}}: no surviving witness
Fig. 2. Minimal-support antichains distinguish alternative from conjunctive authority. Dashed availability is not authorization until an atomic rebind selects it.
erases the carrier nor silently classifies its effect as rejected. Repeating BeginShutdown returns the same cut; it cannot create another retirement point or decrease the epoch. 5.2
Step 2: project actual old-root dependence
The support compiler evaluates the selected witness of each live authority instance. If it contains 𝑎𝑐 , every attached carrier and generator enters the cut’s target set. The complete support antichain is used only to find a possible replacement; its mere existence never edits the selected witness. Figure 2 shows why the distinction matters. The antichain {{𝐴}, {𝐵}} admits independent continuation, but only after a compare-and-swap replaces the 𝐴-selected authorization with a fresh 𝐵-selected instance for the same remaining operation and no wider effect envelope. By contrast, {{𝐴, 𝐵}} is conjunctive: retirement of 𝐴 removes the only sufficient witness, so the carrier must drain, terminate, expire under a trusted bound, or remain nonpositive. 5.3
Step 3: install adapter-specific barriers
Each registered adapter maps the logical cut into enforcement at every place where old-root authority can become durable or cross a protected frontier. Typical barriers include an issuer tombstone, a task-generation fence, a queue ingress epoch check, a trigger disable plus generation watermark, a credential deny epoch, and an effect sink minimum epoch. Every create, accept, trigger, prepare, and commit path checks the current barrier at its own linearization point. An acknowledgement emitted before that check is lifecycle evidence, not closure evidence.
Authorization Revocation for Long-Running AI Agents
17
For sink 𝑝, the adapter first authenticates cut 𝑐 and then installs durable local barrier 𝑏 𝑝 (𝑐), establishing 𝑐 ≺ 𝑏 𝑝 (𝑐). Commitment admissions and 𝑏 𝑝 (𝑐) share the sink’s local total order. A cut-relevant acceptance authorized by 𝑎𝑐 and ordered before 𝑏 𝑝 (𝑐) is first recorded as an accepted admission. After the barrier is durable, the provider finalizes a typed receipt binding the cut, sink, operation and effect digests, complete selected authorization witness, admission position, barrier position, and receipt-record position. This order covers both cut-time outstanding acceptances and cut-to-barrier acceptances. An attempt whose selected support contains the retired atom and is ordered after 𝑏 𝑝 (𝑐) is rejected. This local rule classifies requests concurrent with cut propagation without comparing a root ledger sequence number to a provider sequence number. Adapters classify cut-target objects into typed terminal dispositions: RETIRED, FENCED, trusted EXPIRED, PRE_FENCE_COMMITTED, or REBOUND. The pre-fence disposition is valid only with the ordered receipt and a closed future-use frontier. A prepared or accepted item is not terminal merely because cancellation was requested. An unavailable query or unverifiable fence produces UNKNOWN. 5.4
Step 4: conserve local and transferred carriers
At any evidence revision, an old-root carrier has exactly one accountable location: a provider-local registry, a uniquely identified cross-provider transfer, a terminal/fenced disposition, or a completed rebind. Emission atomically changes ownership from local to in transit. Acceptance of the same token changes it from in transit to destination-local; rejection produces a terminal receipt. The oldatom token-creation record precedes the root cut and is included in its frozen token frontier; a later delivery cannot create a new token under that epoch. An accepted acknowledgement precedes any terminal accounting of the destination carrier. Tokens are exact identities, not an aggregate counter, so two different messages cannot cancel arithmetically. Since send and terminal acknowledgement records have different types, composition compares their canonical token projections, 𝜋𝑡 (𝑂 (𝐸)) = 𝜋𝑡 (𝐵(𝐸)), together with disposition validity; it never asserts equality of the heterogeneous records. For FIFO channels, marker order can determine the cut. For non-FIFO channels, the profile supplies unique sequence identities, a gap-free watermark, and terminal receipts. A channel that satisfies neither profile remains Indeterminate. This rule directly excludes the execution in which both endpoints report local emptiness while one message lies between their scans. 5.5
Step 5: produce provider-frontier leaves
Table 3 lists the minimum logical content of a leaf. A production encoding can add provider-specific receipts, but it cannot omit a field used by the composition predicate. The signature authenticates origin and content; semantic soundness comes from admission of the adapter contract and its evidence source. 5.6
Step 6: compose the cutset
The aggregator accepts revisions only under an exact-key merge. Repeating an identical fact is idempotent; two values for the same fact key are conflicting. Headers, manifests, configurations, cut identities, and profile versions must agree. Compatible leaf facts form a join-semilattice, so the result is independent of leaf arrival order, duplication, or aggregation tree. Known blockers dominate the verdict: any live old-root carrier, unaccounted or post-barrier accepted operation, generator, or unmatched in-flight token yields Not-Quiescent. In the absence of a known blocker, missing coverage, a leaf marked unknown, a stale fence, a token gap, or a configuration conflict yields Indeterminate. The aggregator returns Quiescent only when the issuer cut is durable, coverage is exact, every required barrier is installed, all cut-target carriers have admissible dispositions, channel tokens close, and every continuation either excludes the retired atom by verified rebind or is effect-closed.
18
Zhu and Wang
Table 3. Logical leaf-certificate obligations. Field group
Bound fact
Acceptance condition
Identity
provider, adapter profile, key identity, schema version root, retired epoch, cut id, cut-record digest manifest/configuration/graph-scope digests; covered ingress, frontier and channels fence receipts, provider-local admission/barrier positions, log watermarks open carriers, generators, accepted operations, typed terminal dispositions
admitted and unambiguous
Cut header Coverage
Barrier evidence
Local state
Transfer state Rebind state
Uncertainty Integrity
5.7
typed SEND and terminal ACK records with unique token maps exact old/new root-epoch atoms, selected witness, operation and envelope digest unavailable queries, conflicts, gaps, stale observations evidence root, evidence-through sequence, snapshot digest, issued time, signature
exact agreement across leaves union equals sealed manifest
causal observation of the cut and valid local ordering no known old-root live blocker; every cut-relevant old-atom pre-fence acceptance has its exact receipt exact projected accounting; ACCEPT binds a covered destination carrier independently current support and atomic replacement empty for a positive leaf every referenced fence, receipt, and ACK precedes the signed leaf
Certificate issuance and replay
The certificate binds the cut-record digest, graph root, endpoint and sink catalog digests, fence and terminal receipt roots, alternate-support proof root, configuration digest, issuance sequence, and certificate identity. Its issuance transition moves the generation from draining to quiescent in the same durable transaction. An exact retry carrying the same request identifier and canonical candidate digest returns the identical committed certificate. A different request identifier for the completed generation, or reuse of the identifier with a different body, is rejected as a conflicting remint. A changed manifest, adapter profile, policy, or root epoch requires a new cut and new evidence. 6
Protocol Instantiations
The protocol is provider-neutral, but a leaf is meaningful only through a concrete adapter contract. This section specifies the executed reference core and the correspondence obligations that any deployment profile must satisfy. A logical endpoint shape in the reference artifact is not evidence about a remote service. 6.1
Reference ledger and protected sink
The reference implementation uses a file-backed ledger with canonical JSON, domain-separated SHA-256 digests, a contiguous hash-linked event log, and write–fsync–rename–directory-fsync persistence. Mutating transactions take an exclusive file lock, reload the durable state while holding that lock, and validate the complete state before committing. Thus, a process that opened the ledger
Authorization Revocation for Long-Running AI Agents
19
before a concurrent cut cannot authorize from its stale in-memory snapshot or overwrite the cut with a lost update. Each root is ACTIVE, DRAINING, or QUIESCENT. A durable cut increments the root epoch and freezes the obligation identifiers whose selected witness contains the retiring root. Sink fences record the minimum admitted epoch; the reference authorization check requires the exact grant-bound atom set selected for the obligation, the registered obligation/sink binding, and satisfaction of the sink-local fence. The root cut prevents creation of new authority from the retired atom, but deliberately does not stand in for the sink fence: an already scheduled old-atom attempt remains admissible in the cut-only arm until the protected sink installs its barrier. The ledger enforces exact selected witnesses for both alternative and conjunctive supports, monotone obligation and channel transitions, conflict-free leaf records, registered global token identity, and current alternate roots for explicit rebind. Root identifiers in a support template are instantiated into exact current grant-bound atoms when a witness is selected or rebound; the alternate-root case advances root 𝐵 to epoch 2 before rebind and admits only that epoch-2 atom. A terminal channel cannot be reopened, an unregistered leaf token cannot be introduced as evidence, and a strict subset of a conjunctive witness cannot authorize an effect. The reference channel path records a typed SEND binding token identity, source, destination, payload, authorization atoms, and emission sequence. Its terminal acknowledgement binds a disposition and evidence; an ACCEPTED disposition additionally names the destination carrier into which the token was admitted. A Quiescent leaf is admitted only after the relevant sink fences, obligation receipts, and terminal channel acknowledgements have already entered the durable log. The leaf binds an evidenceThroughSequence and a digest of the endpoint-local evidence snapshot through that sequence, so a later record cannot retroactively satisfy an earlier positive leaf. A pre-fence commitment is terminally accounted only by a typed receipt created after the sink barrier and binding the cut, obligation, operation, effect, sink, exact selected authorization atoms, admission sequence, and barrier sequence. The executed pre-fence case covers both an accepted admission that is already outstanding when the cut occurs and a second admission accepted between the cut and barrier; each receives its own exact post-barrier receipt. Certificate retry identity is the pair (requestId, candidateDigest): an exact pair returns the same committed certificate, reuse of the request identifier with another candidate body is rejected, and a different request identifier cannot remint the same generation. This is a provider-free executable semantics: no network request, cloud resource, credential, payment, or production effect is performed. A protected effect is an inert typed record whose acceptance is decided at the local sink.
6.2
Cancellation-race worker
The late-effect test suite forks an independent worker process. In every causal-separation case, the worker first acknowledges that the protected unit has been scheduled; only then may the controller cut or fence. The harness next observes an explicit EFFECT_READY barrier, sends CANCEL, and requires the first matching post-cancel arrival to be CANCEL_ACK; an earlier effect arrival fails the case. Each case also emits a case-bound, nonce-bearing, hash-linked harness transcript. The worker retains the already scheduled unit and, only after enqueuing the acknowledgement, presents the same old-atom effect to the parent-side protected sink. The three arms differ only in the intervention applied after scheduling: (i) cancellation only leaves the old effect admissible; (ii) a root cut without a sink fence prevents new authority expansion but still leaves that already scheduled effect admissible; and (iii) the same cut followed by the sink-local fence rejects the identical effect at its linearization point. The design therefore identifies the fence, rather than cancellation timing or work creation timing, as the cause of rejection.
20
Zhu and Wang
Table 4. Endpoint correspondence contracts for conforming deployments. Endpoint
Persistent carrier
Required barrier/evidence
Nonpositive condition
MCP asynchronous task
task state, provider work, descendants
cooperative ack without terminal/frontier evidence
A2A delegated task
remote task, artifact, delegated child
Credential issuer
access/refresh token and derived credentials
Durable queue or trigger
message, retry, cron, webhook, generator
Effect reservation/gateway
reservation, prepare, settlement
cut-bound cancel receipt, terminal query, descendant/transfer coverage, protected sink fence task correlation, terminal or fence receipt, outbound child tokens issuer tombstone/introspection, propagation bound, derived-token closure ingress generation fence, gap-free watermark, accepted-message terminal receipts cutoff-aware reserve/commit gate and terminal/no-effect receipt
unsupported cancel, missing child catalog, late artifact path unknown derivation, cache bypass, untrusted expiry forgotten generator, watermark gap, unfenced consumer ambiguous prepare/commit, bypassable effect sink
Durability cases reconstruct the ledger after fencing and exercise a process that opened the ledger before the cut. The latter must reload the cut under the transaction lock before evaluating its attempt. Further cases exercise dual pre-barrier admission accounting with post-barrier receipts, leaf snapshot ordering, typed channel SEND/terminal-acknowledgement accounting, exact certificate retry versus body conflict and remint, epoch-2 alternate-root rebind, conjunctive-witness enforcement, ghost leaf-token rejection, and the irreversibility of terminal channel state. The checker validates the recorded transcript chain, nonce, registered message order, rejection entries, and their bindings to durable events. The transcript is evidence about this harness execution; it is not presented as an observation of an external provider. These executions test concrete process, ordering, and persistence behavior while remaining isolated from external providers. 6.3
Endpoint correspondence contracts
Table 4 defines representative correspondence contracts for concrete adapters. MCP and A2A cancellation responses retain their specified lifecycle meanings; an adapter may add only evidence obtained from authenticated query, fence, receipt, and sink interfaces [1, 18]. A profile that cannot supply a required field must report it as unavailable, causing the affected leaf to remain Indeterminate. 6.4
Runtime shutdown IR
A runtime adapter maps native task, session, and tool events into the following shutdown IR: ⟨targetRoot, rootEpoch, caller, taskCorrelation, endpointCatalogDigest, sinkCatalogDigest, barrierPolicyDigest, runtimeBoundary⟩. The IR does not treat a runtime as providing root-scoped quiescence by itself. It makes correlations and omitted evidence mechanically visible. A conforming mapping freezes its source boundary,
Authorization Revocation for Long-Running AI Agents
21
produces the complete normalized object, and fails closed when a root, epoch, task, endpoint, sink, policy, or runtime identity field is absent or misbound. Runtime-specific lifecycle events remain inputs to the provider and sink contracts; they do not replace them. 6.5
External-field correspondence
A provider profile classifies each protocol or service field as direct, derived under an explicit rule, supplementary deployment evidence, or unavailable. MCP task state, A2A lifecycle state, OAuth revocation and introspection, and queue or scheduler receipts each cover only part of the leaf schema [1, 16, 18, 23]. A profile cannot treat the union of unrelated documents as one implementation: it identifies the concrete source for every required field, and any unavailable field keeps the corresponding leaf Indeterminate. 6.6
Cryptographic and trust profiles
The reference artifact uses content digests to make deterministic replay and tamper checking explicit; it does not present those digests as provider authentication. A deployment profile additionally binds leaf signing keys, key status, signature algorithm, replay domain, certificate schema, and provider identity. Even a valid signature proves only which admitted principal made the assertion. Coverage and semantic truth continue to depend on complete mediation, authoritative observations, and the leaf contract stated in Section 3. 7
Evaluation
The evaluation tests the provider-free durable-ledger artifact, including strict causal separation among cancellation-only, cut-only, and cut-plus-fence control. It evaluates the executable protocol invariants and does not transfer those results to unexecuted runtime or provider interfaces by renaming a logical endpoint as a deployed service. 7.1
Research questions
RQ1: Separation. Can an acknowledged cancellation still yield a protected effect under the baseline, while a root cut and sink fence reject the identical old-epoch attempt? RQ2: Decision soundness. Do known live obligations and channels remain Not-Quiescent, and do missing endpoint or fence facts remain Indeterminate? RQ3: Precision. Can shutdown of root 𝐴 preserve the same remaining work under an independently sufficient current root 𝐵 through an explicit exact-witness rebind, without reusing 𝐴’s grantbound authorization atom? RQ4: Durability and evidence integrity. Do persisted fences survive restart and stale-process attempts; do transaction locks prevent lost updates; and do post-barrier exact commitment receipts, evidence-bounded leaves, typed channel sends and terminal acknowledgements, exact request/body retry semantics, remint rejection, channel monotonicity, and a separately implemented checker preserve the certificate boundary? 7.2
Executable 17-case late-effect test suite
The refreshed corpus contains 17 cases (Table 5). Each case runs in a fresh temporary ledger. For the three causal-isolation arms, the worker reaches a STARTED barrier before cancellation, cut, or fence, so the protected unit is scheduled before the interventions diverge. The harness then observes
22
Zhu and Wang
EFFECT_READY, sends cancellation, and accepts only an actual CANCEL_ACK-before-effect arrival order. Every case also carries a case-bound nonce and hash-linked harness transcript. The runner embeds the registration for reporting, while the checker holds a separate 17-case oracle and imports no controller, corpus, worker, or adapter module. It independently recomputes the transcript and ledger hash chains, leaf evidence snapshot digests, certificate semantic snapshot digests, and resultset digest. It then checks the registered transcript order and rejection entries, their bindings to durable effect/intervention records, the root generation, exact selected authorization atoms, and each effect decision reconstructed from its obligation binding and event-time sink fence. It further checks cut-bound fence records, post-barrier commitment receipts, leaf evidence boundaries, typed channel sends and acknowledgements, post-cut effects, send-before-cut and accepted-ack-beforedestination-terminal causality, channel monotonicity, and certificate request/body identity. This reconstruction establishes consistency and registered semantics of the serialized evidence; process scheduling before it was recorded and behavior of unexecuted external services are outside that checker’s observation domain. The worker is a real child process, but endpoint labels in this layer denote logical shapes, not claims about remote MCP, A2A, OAuth, or scheduler implementations. Effects are inert typed records evaluated by a local protected sink. The stale-process case opens a second ledger instance before the cut and attempts the protected effect only after the first process commits the cut and fence. The case fails if the second process can authorize from its stale snapshot or overwrite the intervening state. The pre-fence case separately admits one effect before the cut and one after the cut but before the barrier, then requires both exact receipts to be durably finalized after the barrier before its positive leaf. The channel case records a typed send between distinct logical endpoints and an ACCEPTED terminal acknowledgement naming the destination obligation before that obligation’s terminal receipt and the two endpoint leaves. This construction isolates causal, accounting, and persistence distinctions while keeping the experiment deterministic and provider-free.
7.3
Comparison boundary
The executed baselines are cancellation acknowledgement alone and a root cut without a sink fence. They share the same scheduled unit and protected-effect oracle with the complete cut-plus-fence arm, so the comparison isolates the mechanism responsible for rejecting the late effect. Process exit, token revocation, subtree cascade, graph-targeted revocation, and conjunctions of endpointterminal states are analyzed through their stated semantics and the formal counterexamples in Sections 2 and 4; they are not reported as measured remote-service baselines. A provider-local closure verifier remains a compatible leaf mechanism rather than a substitute for the root-scoped composition protocol.
7.4
Adversarial checker evaluation
The separate checker additionally faces 44 semantically modified and consistently rehashed traces. The mutations cover accepted-effect and fence safety; effect-code, operation, carrier, and authorization-atom binding; cut-frontier completeness and root-epoch causality; exact pre-fence accounting; leaf, certificate, and request identity; typed channel payload, destination, and terminalstate integrity; and complete worker, retry, and rejection transcripts. Cross-case substitutions are resealed under the receiving case, so rejection depends on semantic reconstruction rather than a stale digest. The suite also rejects a SEND moved after its frozen cut and an accepted acknowledgement moved after destination-terminal accounting.
Authorization Revocation for Long-Running AI Agents
23
Table 5. Provider-free 17-case late-effect test-suite registration. Scenario group
Cases
Registered outcome
Registered distinguishing fact
Cancellation acknowledgement only
2
baseline false-stop
Root cut without sink fence
1
Not-Quiescent
Root cut and sink fence
2
Quiescent
Restart and stale-process interleaving
2
Quiescent
Alternate-root rebind
1
Quiescent
Opaque endpoint / missing fence
2
Indeterminate
Typed pre-fence commitments
1
Quiescent
Open obligation / in-flight token
2
Not-Quiescent
Exact retry / body conflict / remint
1
replay safe
Conjunctive witness enforcement
1
rejected
Ghost leaf token
1
rejected
Terminal channel reopen
1
rejected
late epoch-1 effect accepted after acknowledgement already scheduled old-atom effect remains admissible identical already scheduled effect rejected at the sink persisted barrier is reloaded under the transaction lock exact current root-𝐵 epoch-2 atom replaces, rather than edits, root-𝐴 authorization absent evidence never becomes a positive certificate two exact receipts, finalized after the barrier, account for pre-cut-outstanding and cut-to-barrier admissions known carrier blocks positive certification the same request/body pair is idempotent; same-ID/different-body and different-ID attempts are rejected a strict subset of the selected conjunction cannot authorize an unregistered token cannot appear in frontier evidence distinct sender/receiver leaves reconcile a pre-cut send and accepted terminal ACK bound before destination termination; terminal state is irreversible
7.5
Metrics and acceptance criteria
Primary registered outcomes are false-quiescence certificates, post-certificate old-root frontier crossings, unknown-to-Q collapses, residual authority and obligation counts, exact phase/code matches, alternate-root preservation, and replay/tamper detection.
24
Zhu and Wang
Table 6. Fresh-run evidence for the executable 17-case layer. Registered check
Fresh result
Status
Expected case verdict and effect outcome Separate checker agreement Cancellation-only / cut-only late effects accepted Cut-plus-fence, restart, and stale-process late effects rejected Root decision totals
17/17 17/17 2/2 and 1/1
pass pass pass
2/2, 1/1, and 1/1
pass
Quiescent: 6; Not-Quiescent: 3; Indeterminate: 2 1/1 and 2/2 admissions receipted 1/1, 1/1, and 1/1
pass
pass
1/1 each
pass
11/11 1/1 and 1/1
pass pass
44/44
pass
Alternate-root epoch-2 rebind / dual pre-fence accounting Exact retry / same-ID body conflict / different-ID remint Conjunctive witness / ghost token / terminal reopen Evidence-bounded positive leaves Typed channel send / terminal ACK destination binding Semantically rehashed checker regressions rejected
pass
The artifact gate requires 17/17 registered runner outcomes, 17/17 separate checker decisions, rejection of all 44/44 semantically rehashed regressions, zero false certificates, and zero registered post-certificate old-root crossings. Every insufficient-evidence case must remain Indeterminate; every known live carrier must remain Not-Quiescent; and every registered independently authorized alternate-root case must be preserved. Performance is descriptive and does not serve as evidence for safety. 8
Executable Evidence
The evaluated system is the executable durable-ledger artifact, its 17-case late-effect test suite, and the separately implemented checker. Numerical outcome claims enter this section only from fresh runner and checker receipts whose digests bind the complete trace set. The refreshed runner matches all 17 registered outcomes, and the refreshed separate checker agrees on all 17 traces and rejects all 44 semantically modified and consistently rehashed regressions. Table 6 reports this executable evidence. 8.1
Causal-isolation criterion
All three arms use the same ordering: the worker reports STARTED before intervention, reports EFFECT_READY before cancellation, and enqueues CANCEL_ACK before emitting the same old-atom effect. The parent consumes the first matching post-cancel arrival without type-selective reordering. Both cancellation-only cases acknowledged intent and accepted the effect. The cut-only case prevented new authority expansion but accepted the already scheduled effect because no sink barrier existed. Both cut-plus-fence cases rejected that effect at the protected sink. The restart and stale-process cases also rejected it, for four mechanism rejections in total. The comparison
Authorization Revocation for Long-Running AI Agents
25
therefore attributes rejection to the sink-local fence, rather than to cancellation timing, process exit, or post-cut work creation. 8.2
Typed decision and identity criteria
The two insufficient-evidence cases remained Indeterminate. The open obligation, in-flight channel, and accepted cut-only effect remained Not-Quiescent. Six cases reached Quiescent, and no nonpositive case carried a root-𝐴 quiescence certificate. The alternate-root case begins with support antichain {{𝐴}, {𝐵}} and an exact selected root-𝐴 witness. The execution first advanced active root 𝐵 to epoch 2. The rebind then atomically instantiated the alternative support as the exact current root-𝐵 epoch-2 atom before root-𝐴 certification and permitted the protected effect only under that atom. The conjunctive case rejected an obligation selected under {𝐴, 𝐵} when it presented only 𝐵. These cases distinguish independent preservation from authority laundering by label deletion or stale-epoch substitution. The pre-fence case admitted two effects under the retiring atom: one before the cut whose commitment remained outstanding at the cut, and one after the cut but before the sink barrier. Only after the barrier did the ledger finalize a separate typed receipt for each admission. Each receipt binds the cut, obligation, operation, effect, sink, exact selected authorization atoms, admission sequence, and barrier sequence; the case reached Quiescent only after both receipts were present. Each positive leaf binds the last preceding evidence sequence and a digest of its endpoint-local evidence snapshot. The ledger admits such a leaf only after the applicable fence, obligation receipt, and typed terminal channel acknowledgement. The terminal-channel case recorded a typed send from one logical endpoint to another before the cut, followed by an ACCEPTED acknowledgement bound to the destination obligation before that obligation’s terminal receipt and before both endpoint leaves; the later attempt to reopen the token was rejected. Leaf admission also rejected the unregistered ghost token. 8.3
Durability and checker separation
The restart case reconstructed the ledger after the cut and fence and rejected the old-atom attempt. The stale-process case opened a second instance before the cut; its later transaction reloaded the durable state under the exclusive lock and rejected the same class of attempt. Together they exercise persistence, stale-snapshot exclusion, and lost-update prevention at the authorization boundary. The certificate identity case returned the same committed certificate for an exact retry of the same (requestId, candidateDigest) pair. It rejected reuse of that request identifier with a different candidate body as a request conflict and rejected a different request identifier as a remint of the committed generation. The ledger’s state validator accepted the contiguous event sequences and predecessor digests in every final state. The checker carries its own case oracle and implements canonicalization and domain-separated hashing independently. It neither imports nor calls the ledger, runner, worker, or corpus. It recomputes every durable-event and harness-transcript hash-chain link, every leaf evidence-snapshot digest, every certificate semantic digest, every case digest, and the result-set digest. Its case rules reconstruct each effect decision from its obligation binding and event-time sink fence, as well as the cut frontier, exact current support atoms, receipt and fence ordering, typed channel send/acknowledgement bindings, destination carrier for an accepted acknowledgement, sendbefore-cut and accepted-ack-before-destination-terminal causality, certificate request/body identity, and registered negative-operation outcomes. Its refreshed oracle agreed on 17/17 traces and reproduced the runner’s result-set digest. Agreement is therefore a distinct implementation check, not a second invocation of the controller’s verdict function.
26
Zhu and Wang
For child-process and rejected-operation evidence, the checker validates the case-bound nonce, transcript chain, registered entry order, rejection code, and correspondence to the durable intervention/effect records. It does not claim an independent observation of facts outside the serialized execution, such as behavior of a remote provider that this provider-free harness never invoked. A separate adversarial regression harness modifies certified traces and then recomputes the affected event chain, leaf and certificate digests, transcript chain where applicable, case digest, and result-set digest. The checker rejected 44/44 such traces. The registered mutations exercise effect/fence decision reconstruction; cut, root-epoch, obligation, receipt, leaf, and certificate identity; cut-frontier and negative-leaf completeness; exact alternate and conjunctive support; pre-cut and cut-to-barrier accounting; channel authorization, payload, destination, SEND, acknowledgement, and terminal causality; and worker, stale-process, retry, and rejected-operation transcripts. Several mutations splice internally well-formed fields from a different registered case and then reseal every affected digest. The checker therefore rejects the resulting trace by independently reconstructed semantics, not because the mutation left a stale outer hash. In particular, it rejects a SEND moved after the frozen cut and an accepted acknowledgement moved after the destination carrier’s terminal receipt. This gate prevents a later certificate from concealing an earlier registered safety violation even when the modified trace is rehashed consistently. 8.4
Claim discipline
The executable evidence comprises the durable ledger, protected-sink authorization path, childprocess race harness, 17-case registration, and separate checker described above. Its refreshed runner matched 17/17 registered outcomes, the checker agreed on 17/17 traces, and the checker rejected 44/44 semantically rehashed regressions. The executable evidence further includes exact post-barrier accounting of both registered pre-barrier admissions, evidence-bounded positive leaves, typed channel send/terminal-acknowledgement binding, exact-current epoch-2 alternate-root rebind, request/body-bound certificate retry, and case-bound hash-linked harness transcripts. The cross-provider composition results follow from the formal model and proof obligations in Section 4. The provider-free artifact supplies an executable instantiation of the ledger, cut, fence, carrier, channel, rebind, leaf, and certificate invariants. Endpoint names in its 17-case corpus are semantic categories, not assertions of runtime or remote-provider conformance. A deployment claim requires concrete adapters to satisfy the correspondence contracts in Section 6; no such claim is inferred from this artifact. This scope preserves a one-to-one mapping between every empirical sentence and the system that produced its receipt. 9 9.1
Related Work Task cancellation and credential revocation
MCP Tasks and A2A expose asynchronous task lifecycles and cancellation operations [1, 18]. Their cooperative semantics avoid promising an impossible instantaneous rollback once remote work has advanced. The protocol treats their acknowledgements and terminal states as evidence about registered task carriers, then additionally closes derived authority, provider obligations, and cross-provider messages at a root-epoch cut. Stop Means Stop measures cancellation and timeout enforcement gaps in agent frameworks and evaluates an external effect gate with fence-on-cancel [12]. The protocol takes external mediation as an admitted leaf capability and targets the distinct composition question: one retiring authorization root across heterogeneous providers, in-flight channels, and shared carriers with independently sufficient support.
Authorization Revocation for Long-Running AI Agents
27
OAuth token revocation standardizes invalidation of a named access or refresh token [16]. Heartbeat and short-lived credentials provide a temporal bound on authority persistence when renewal stops [7]. These are useful closure mechanisms for credential leaves. The compositional quiescence predicate is broader: it covers effects already accepted under the credential, descendants and triggers derived from it, and continuing shared work whose support must be rebound to another root. 9.2 Agent tool execution and adversarial inputs ToolEmu demonstrates scalable risk testing for language-model agents operating over consequential tool surfaces [26], while AgentDojo evaluates tool-using agents over untrusted data under promptinjection attacks [6]. These systems establish the practical importance of adversarial tool execution but do not define an authorization-retirement predicate. The protocol therefore treats plans and tool-supplied inputs as untrusted and places its claim at authenticated, mediated effect sinks. 9.3
Temporary authority and the effect boundary
Lingering Authority makes temporary resource/effect capabilities explicit in a request–grant– invoke monitor and rejects replay of epoch-bound handles once their grant episode closes [28]. Its guarantee assumes a sound typed catalog and complete mediation. It also states the precise concurrency boundary relevant here: a call permitted before closure but still in flight must be serialized before the effect or revalidated immediately at that effect. The protocol supplies the subsequent root-wide accounting layer. A retiring grant atom is cut across a declared set of heterogeneous endpoints; work may remain live only through an independently sufficient alternateroot witness; each cut-relevant carrier must be closed or rebound; and each cut-relevant old-atom acceptance preceding its local barrier must receive an exact typed disposition in a provider leaf. Temporary Authority, Permanent Effects defines commit-time authorization in terms of witness freshness, causal priority, effect binding, and eligibility, and evaluates a fail-closed monitor on protected commit surfaces [29]. That rule is a natural sink-adapter obligation for the root-scoped quiescence protocol. It decides whether one proposed durable effect may cross its commit boundary; the root-scoped protocol additionally establishes which authorization epoch is retiring and composes the outstanding carriers, provider frontiers, and cross-provider messages needed to certify that no further commit attributable to that root remains possible. AID-Guard carries authorization through one provider-atomic effect and one reservation lineage, revalidates the immutable request and provider state at commit, and retains ambiguity until a terminal result or certified no-effect with a delivery fence permits release or one successor [33]. Its analysis explicitly treats revocation ordered after a durable submission as non-retroactive: the submitted request must be reconciled, not presumed cancelled. This is exactly the class of obligation a provider-frontier leaf must settle. The composition unit differs: AID-Guard’s conditional uniqueness property is per reservation and supported provider contract, whereas the protocol retires one selected root across a coverage manifest, atomically rebinds shared work to an independently sufficient root, and reconciles tokens crossing provider leaves before issuing the root-relative certificate. AIRGuard derives step-level authority and enforces normalized tool actions at runtime. EBL-Core binds one fully materialized candidate to typed evidence and a verifiable Decision Derivation in an Execution Release Contract, then governs a separate single-use Execution Grant whose redemption and revocation are linearized [22, 36]. These systems reinforce the operation-time mediation expected of a registered protected sink. Their decision unit is an action or grant; rootscoped quiescence additionally freezes one authorization epoch, accounts for its already admitted
28
Zhu and Wang
commitments and durable carriers, and composes closure evidence across the declared provider cut. 9.4
Revocation and residual authority
Classical authorization research established the policy layer on which agent revocation builds. Delegation Logic casts distributed authorization as a proof-of-compliance problem over policies and credentials [14]. State-transition trust management makes policy-changing actions explicit [3]; revocation classifications separate distinct semantic choices [11]; and RDM2000 gives a rule-based account of multistep role delegation and revocation [37]. DW-RBAC specializes delegation and revocation to workflow tasks [34]. These models determine which authority survives a policy transition. The protocol adds a different post-decision obligation: it must drain, fence, or rebind carriers and effects already admitted under the retired root across a declared provider cut. VERA targets exact graph revocation and preserves authorization that remains reachable through valid alternate roots [15]. ResidualAuth studies the state that must be retained to compute correct authorization after revocation [5]. The protocol shares the precision goal but asks a subsequent distributed question. After choosing what remains authorized, can any carrier or in-flight obligation selected under the retired root still produce a protected commit? The support antichain and atomic rebind receipt connect exact multi-root preservation to the epoch cut; provider frontiers and channel tokens then cover consequences released before their provider-local barriers, including consequences admitted while the root cut was propagating. Bounded Agents’ Agentic Principal Chain carries restricted authority and cross-step composition state along delegation, and Earned Authority constrains evolving agents with a fixed effect ceiling and evidence-governed changes below it [19, 38]. Both make authorization history and nonamplification explicit while a grant remains usable. The protocol addresses the complementary retirement predicate: after a particular root atom is cut, it certifies that no manifested carrier or in-flight transfer can use that atom for a future protected acceptance. This difference separates the protocol from subtree cascade. Cascading along all descendants can eliminate some late effects, but it over-revokes shared principals and still need not close a message, reservation, or prepared commit already transferred outside the enumerated subtree. The protocol closes the root-selected effect consequence while preserving a principal only through a new selected witness that excludes the retired atom. 9.5
Agent and provider closure
Distributed proof construction shows how authorization evidence can be assembled across credential holders without collapsing policy proof into a central oracle [2]. The verifier here also composes authenticated evidence, but its evidence concerns post-cut carrier and effect closure rather than proof that a new access request is authorized. Bounded Agent Closure provides a closure vocabulary spanning authority, execution, commitment, and operational state, together with verification of submitted closure evidence [13, 24]. The protocol is an active execution protocol for producing a particular root-scoped evidence object across heterogeneous endpoints. It begins with an atomic epoch cut, performs issuance freeze and sink fencing, requires explicit alternate-root rebind, and composes compatible provider leaves with exact channel accounting. The two abstractions consequently meet at an evidence interface: closure criteria define what a leaf must prove, while the protocol establishes and collects those facts under crash, replay, and partition. The provider-boundary effect-closure work formalizes provider-local effect closure, including future-use, instance, and lineage closure and an explicit effect frontier [30]. The protocol uses this class of result as a leaf certificate rather than reproducing provider semantics at the global layer. Its
Authorization Revocation for Long-Running AI Agents
29
contribution is the cross-provider root cutset: manifest completeness, root/epoch compatibility, fence watermarks, alternate-root receipts, and balanced inter-leaf channel tokens. The construction also shows why the union of locally quiescent statements is unsound without a consistent cut. CONTINUITY specifies assume–guarantee contracts that preserve authenticated security context across heterogeneous controls and requires each realized effect to retain a current end-to-end authorization witness [39]. The protocol adopts the same general lesson that locally valid controls do not compose automatically, but proves a different temporal predicate. It installs an active retirement cut for one root, closes cut-relevant historical commitments at provider-local barriers, preserves only exact alternate-root rebinds, and balances channel tokens before issuing a negative authorization claim: the retired atom cannot support another protected acceptance within the manifest. 9.6
Distributed termination and snapshots
Dijkstra–Scholten termination detection proves passivity and message exhaustion for a diffusing computation; Mattern develops message-counting algorithms for asynchronous, potentially nonFIFO communication; and Chandy–Lamport snapshots capture a consistent global state including channel contents [4, 8, 17]. The protocol imports their treatment of in-flight messages and cut consistency. Its target property is different: authority is scoped to a selected root witness, protected sinks enforce an epoch fence, and a process may remain active under an unrelated root. Durable non-process carriers—credentials, remote jobs, triggers, and prepared effects—also remain relevant even when all observed processes are passive. 9.7
Access-control foundations
Least privilege and complete mediation require authority to be both minimized and checked at the protected operation [27]. Zero-trust architecture likewise places policy enforcement near resources rather than inferring trust from network position [25]. UCONABC extends one-shot access decisions with ongoing authorization, obligations, conditions, and mutable attributes for long-lived usage [20]. The protocol specializes that continuing-control principle to retirement: it also accounts for work admitted before the final fence, which a later access denial cannot retroactively erase. Leases provide a complementary time-bounded right under explicit clock and failure assumptions [10]; a lease expiry is therefore admissible only when the registered profile proves those assumptions and covers derived work. The protocol applies these principles to shutdown: a control-plane status cannot substitute for a sink fence, and a credential or task is not considered closed merely because its initiator disappeared. The resulting certificate is an auditable authorization fact tied to a root, epoch, manifest, and set of effect-mediating leaves. The Authorization-Execution Gap frames a broader divergence between a principal’s intended authorization and realized execution, identifying delegation incompleteness, channel corruption, and composition fragmentation as structural sources and motivating authorization-integrity checks during execution [35]. The protocol instantiates a narrower protocol question after one authorization root has been selected for retirement. It does not infer principal intent or diagnose all three sources; it certifies the cut, support transfer, provider obligations, and channel accounting required for root-relative quiescence under an explicit policy and manifest. Kubernetes finalizers and garbage collection illustrate durable, deferred resource deletion with controller-owned cleanup keys and owner/dependent lifecycle rules [31, 32]. A finalizer can instantiate one provider leaf, but clearing it does not by itself cover external effects, authorization support, or channels into other providers.
30
9.8
Zhu and Wang
Positioning summary
The closest mechanisms solve complementary slices. Cancellation requests a state change; token revocation closes one credential; process exit observes one runtime; graph revocation computes surviving authority; provider closure proves a local effect frontier; evidence frameworks validate declared closure; and termination detection closes process/message activity for one modeled computation. The protocol composes the missing conjunction: an executed root-epoch cut, precise multi-root support transfer, provider-local frontier certificates, and exact cross-provider channel closure. Its certificate claims only that conjunction and does not rename any adjacent result as global shutdown. 10
Assurance Boundary
The root-scoped quiescence protocol makes a strong root-relative claim: cut 𝑐 targets (𝑟, 𝑒), retires epoch 𝑒, advances issuer state to 𝑒 + 1, and a valid certificate excludes every future registered protected-sink acceptance whose selected support contains the retired atom. Any cut-relevant old-atom acceptance before its provider-local fence is bound to an exact pre-fence commitment receipt finalized after that fence. Continuing work is permitted only when an atomic rebind receipt selects an independently sufficient witness that excludes the retired atom. The claim follows from the formal predicate and the deployment premises below; it does not depend on interpreting cancellation, silence, or timeout as success. 10.1
Certified property and non-equivalent statements
The certificate means root-scoped authorization quiescence. Four nearby statements are deliberately kept distinct: • Global idleness would require every process and task to stop. Root-scoped quiescence allows shared work to continue under an independent root. • Business completion would require the task’s objective and external workflow to reach a domainspecific terminal outcome. The certificate addresses the ability of the retired root to cause a new protected commit. • Rollback would undo effects committed before the applicable provider-local fence. The protocol records such effects as pre-fence committed; compensation is a separate authorized workflow. Classical saga execution makes compensation an explicit application-level action for a long-lived transaction, rather than an automatic consequence of abort or revocation [9]. • Universal physical cessation would cover uninstrumented and unmediated real-world consequences. The certificate covers the registered authority graph, endpoints, channels, and protected sinks named by its manifest. These distinctions strengthen auditability: a verifier can determine exactly which proposition was certified rather than inferring a broader notion of “stopped.” 10.2
Deployment premises
The trusted computing base contains the durable cut ledger, certificate verifier, cryptographic keys, registered adapter logic, authoritative state observations, and the protected sinks that enforce fences. Agent plans, task messages, cancellation responses, and provider data not authenticated by a registered profile are untrusted inputs. An adapter may narrow its claim when the provider exposes less state; it may not fill missing evidence with a successful status.
Authorization Revocation for Long-Running AI Agents
31
Table 7. Premises for the root-scoped no-false-quiescence result. Premise
Required deployment fact
Durable cut lineariza- the root epoch transition and issuance tion freeze have one durable linearization point and survive restart Support-sound projec- every admitted live authority instance tion exposes its minimal sufficient rootsupport witnesses and selected witness a continuing instance changes support No root laundering only through an atomic receipt selecting a current witness that excludes the retired atom Complete carrier cov- credentials, tasks, descendants, trigerage gers, reservations, prepared operations, and other registered persistence mechanisms are enumerated or soundly upperbounded Sink mediation and every protected commit crosses a regisfencing tered sink that rejects the retired epoch after installing the named cut fence Leaf authenticity and leaf signatures, identities, manifests, cut compatibility identifiers, configurations, and watermarks are authenticated and mutually compatible Exact channel ac- every cross-leaf authority or obligation counting transfer has a unique authenticated precut SEND in the frozen token frontier and a matched terminal ACK; ACCEPT binds a covered destination carrier before its terminal accounting Crash-safe evidence ledger transitions, fence state, termistate nal receipts, and certificate issuance are replay-safe and durably ordered expiry-based closure uses an authentiLease-time validity cated time source and the profile’s stated skew and propagation bound
10.3
Result when the fact is unavailable no positive certificate for that cut
uncovered or ambiguous support is Indeterminate the instance remains dependent on the retired atom
uncovered carriers remain open or unknown
an unfenced or bypassable sink cannot sign a positive leaf conflicting or replayed leaves are rejected
unmatched, late-created, duplicated, causally inverted, or unbound tokens prevent global quiescence
recovery resumes in nonterminal or indeterminate state expiry is not accepted as closure evidence
Threats covered by the protocol
The safety model includes an agent that continues after cancellation, creates descendants immediately before shutdown, replays old credentials or certificates, duplicates requests, and attempts to preserve retired authority through a shared principal. It includes message reordering and duplication, controller crash and restart, delayed receipts, cancellation–completion races, stale observations, and network partitions. These events can delay a certificate or force Indeterminate; under the premises in Table 7, they cannot justify a false positive. Compromise of the certificate signing key, protected sink, authoritative provider state, host kernel, or registered adapter violates a named premise. Likewise, an external endpoint that offers no sound terminal query, no fence, no bounded expiry, and no independently observable effect state is opaque for this purpose. The correct protocol result for such a leaf is Indeterminate. This is
32
Zhu and Wang
also the information-theoretic boundary: two remote executions can present the same observations while only one retains a late effect, so no observer restricted to those observations can distinguish them soundly. 10.4
Evidence-layer interpretation
The formal proof establishes safety for all traces satisfying the model premises. The executable state machine demonstrates that the registered protocol and fault schedules realize those transitions. The separately implemented trace checker validates event-chain integrity and registered invariants without calling the controller’s decision procedure. Provider or runtime adapters establish only the profiles they implement. A successful finite evaluation therefore supports conformance of those executions; the universal statement comes from the conditional proof, and deployment admission comes from checking the premises for each leaf. Each evidence layer has a distinct role. Authenticated observations establish provider facts, exact channel accounting establishes the global cut, registered executions establish the tested protocol paths, the conditional proof supplies the model-wide result, and signatures bind assertions to their issuers. The certificate composes these layers through cut identity, manifest, configuration digest, watermarks, and leaf digests. 10.5
Safety, availability, and conditional completion
No-false-quiescence is a safety property. Certificate availability is a separate liveness property. Eventual certification requires that every required adapter and sink recover, fences eventually install, messages are eventually delivered or reach an authenticated terminal state, leases expire within their admitted bounds, and fair retry makes durable progress. A permanent partition or permanently opaque endpoint can therefore prevent a certificate while preserving safety. Operationally, the three outcomes have fixed meanings. Quiescent authorizes reliance on the root-cut property. Not-Quiescent identifies known work that must be closed or rebound. Indeterminate identifies an evidence or observability gap that must be resolved or isolated. Policy may escalate or contain either nonpositive result, but may not relabel it as quiescence. 11
Conclusion
Stopping a long-running agent is an authorization problem, not a synonym for closing its initiating process. Cancellation acknowledgement, token revocation, and process exit each close a useful local object, yet durable tasks, derived credentials, triggers, prepared effects, and cross-provider messages can preserve the retiring root’s ability to commit. Provider-local closure likewise becomes a global result only when the leaves describe one compatible cut and account for work crossing between them. The protocol establishes that cut explicitly. A durable root-epoch transition freezes new issuance; operation-time fences block the old epoch at protected sinks; an outstanding authority–obligation graph tracks persistent carriers; provider leaves certify local frontiers and watermarks; and channel tokens close the cross-provider boundary. Minimal root-support antichains and atomic rebind receipts preserve valid shared work without transferring the retiring root through another principal. The resulting certificate has a precise meaning: within its authenticated coverage manifest and mediation premises, every cut-relevant acceptance authorized by the retired atom and preceding its provider-local fence is terminally accounted, and no registered protected-sink acceptance ordered after its fence can select that atom. Known residual work is Not-Quiescent; missing, conflicting, or opaque evidence is Indeterminate. Neither cancellation success nor elapsed time can silently promote either state to quiescence.
Authorization Revocation for Long-Running AI Agents
33
This separation gives heterogeneous agent systems a compositional shutdown contract. Task protocols continue to manage lifecycle intent, credential issuers continue to revoke tokens, provider adapters continue to prove local effect closure, and distributed evidence verifiers continue to validate their declared predicates. The protocol binds those facts to one root-scoped authorization cut, making “stopped” a verifiable security assertion rather than a control-plane impression. A
Proofs of the Quiescence Results
We reason over finite prefixes of accepted traces of the transition system in Section 4. A rejected operation may append a diagnostic event but does not alter roots, selected support, carrier authority, fences, frontiers, or terminal channel dispositions. Cryptographic and storage claims are invoked only through the numbered assumptions in Table 2. A.1
Trace notation and preservation facts
Write 𝑜1
𝑜2
𝑜𝑛
𝑆 0 −→ 𝑆 1 −→ · · · −−→ 𝑆𝑛 for an accepted trace. Events within the root ledger are ordered by ⪯𝑟 ; events within endpoint or sink 𝑝 are ordered by ⪯𝑝 . Cross-domain reasoning uses only the causal happens-before relation ≺ of Section 4. In particular, no proof step compares a root-ledger position with a provider position. A transition selects atom 𝑎 if its authenticated authorization record names a selected witness containing 𝑎. A1 mediates issuer transitions, whereas A5 mediates protected commitment admissions through the corresponding provider-local barrier. By A3, A5, and A9, root epochs, cuts, barriers, and terminal evidence are monotone in their respective domains. Two elementary preservation facts will be used repeatedly. First, no transition other than a registered authorization or rebind transition changes sel(𝑥). Second, a terminal acknowledgement for token identifier 𝑡𝑖𝑑 is inserted under a uniqueness constraint binding the full canonical token. Replaying the same acknowledgement is idempotent; changing its disposition is a conflict, not a second valid state. By A1 and A7, an old-atom token-creation record precedes the cut, and an accepted acknowledgement precedes every terminal transition of its covered destination carrier. A.2
Cut and support lemmas
Proof of Lemma 1. Let 𝑖 ∈ I𝑟 be the first issuer transition after 𝑐 in ⪯𝑟 that attempts to issue, delegate, reactivate, or enlarge authority with a selected witness containing 𝑎𝑐 = ⟨𝑟, 𝑒, ℎ𝑔 ⟩. The atomic transaction for 𝑐 retires epoch 𝑒, advances the stored root epoch to 𝑒 + 1, and places the root in DRAINING. A3 makes those changes monotone. A1 requires 𝑖 to validate the exact grant digest and epoch at its own root-ledger linearization point; A2 prevents substitution of a different canonical atom. Thus 𝑎𝑐 is not current for 𝑖, and acceptance contradicts A1. This argument is intentionally limited to issuer-side non-expansion. An already authorized carrier can retain 𝑎𝑐 and reach a sink after 𝑐 but before that sink installs 𝑏 𝑝 (𝑐). Such an admission is classified in ⪯𝑝 , must precede 𝑏 𝑝 (𝑐), and must receive the typed receipt and closed frontier required by A5. An attempt after 𝑏 𝑝 (𝑐) is rejected by the sink fence. Delivery or settlement following an accepted admission is part of that same commitment event and is not a new issuer transition. □ Proof of Lemma 2. Consider the authenticated carrier-provenance graph in creation order. For a carrier 𝑥 present when the cut commits, A4 requires its complete minimal support antichain and actual selected witness to be stored with its creation or latest authorization record. Therefore 𝑎𝑐 ∈ sel(𝑥) places 𝑥 in the base set of 𝐷𝑐 . A different witness in Σ(𝑥) cannot change this fact: by Definition 2, alternatives are distinct conjunctive supports, while sel(𝑥) names the one that actually authorized the current carrier.
34
Zhu and Wang
An outstanding cut-time token whose recorded support contains 𝑎𝑐 is an explicit base edge even if its destination carrier has not yet materialized. A7 either gives that token a rejecting/expiry disposition or binds acceptance to a covered destination carrier, which the closure definition of 𝐷𝑐 places in the projection. For the induction step, suppose every dependent carrier created through event 𝑗 is in the projection. If such a carrier emits a cross-endpoint handoff, A7 gives the handoff one canonical token and binds its selected support digest. On acceptance, the destination record names that token and projects its support into the new carrier. The closure rule for 𝐷𝑐 therefore includes the destination carrier. If the token is rejected or expires, no destination carrier is created. If its disposition is absent, the emitted token remains an explicit unresolved edge; it is not interpreted as absence. A6 ensures that the endpoint and channel class appear in the frozen manifest, including carriers materialized after the cut but before the stable-scan watermark. Induction covers every finite creation prefix. A4 maps missing or ambiguous provenance to UNKNOWN, so the verifier reports 𝑈 instead of deleting the node. Thus every carrier and accepted handoff selected under 𝑎𝑐 is included, while discarding a nonselected alternative witness cannot discard the selected dependency. □ Proof of Lemma 3. The only nonterminal transition that removes 𝑥 from the dependent projection is Rebind(𝑥,𝑊 ′, 𝑐). Its guard verifies that 𝑊 ′ is a complete registered minimal support, that 𝑎𝑐 ∉ 𝑊 ′ , and that every atom and derivation edge in 𝑊 ′ is current. A8 further requires a fresh authorization decision and one atomic transaction that changes the selected witness and carrier epoch while emitting 𝜌𝑥 . Consequently there is no intermediate accepted state in which the carrier continues under neither witness, or in which it claims 𝑊 ′ while exercising the old witness. The same guard compares the canonical operation and effect-envelope digests with the carrier’s pre-transition record; any substitution or widening fails, and 𝜌𝑥 binds the unchanged values. A label edit changes none of the authenticated fields in 𝜌𝑥 . A parent edit breaks its provenance digest. Selecting an alternative that still contains 𝑎𝑐 , contains a stale atom, or is not in Σ(𝑥) fails the guard. Finally, descendants not covered by the atomic profile retain their old selected records and remain in 𝐷𝑐 . Therefore a successful departure from 𝐷𝑐 proves a complete current derivation independent of the retired atom, rather than merely renaming the dependency. □ A.3
Composite safety and necessary evidence
Proof of Theorem 1. Assume the verifier issues C𝑐 . By Definition 5, all leaves have the same compatibility header, the frozen manifest is complete, every required scope is covered, all signatures and watermarks verify, every required provider barrier and frontier is present, and exact channel conservation holds. Each barrier authenticates the cut before installation, so 𝑐 ≺ 𝑏 𝑝 (𝑐), without any comparison of root and provider sequence numbers. Lemma 2 therefore makes the union of the leaf projections complete for 𝐷𝑐 . First consider the certified prefix. Suppose a sink 𝑝 accepted a commitment 𝑘 selected under 𝑎𝑐 with 𝑏 𝑝 (𝑐) ≺𝑝 𝑘. A5 requires the local barrier to reject precisely that admission. Moreover, the authenticated local log and stable frontier expose an acceptance after the barrier as a concrete 𝑁 witness. Either fact contradicts issuance of 𝑄. Every cut-relevant acceptance under 𝑎𝑐 ordered before 𝑏 𝑝 (𝑐), including one causally after 𝑐 but before barrier installation, must instead appear in pfc 𝐽𝑝 with its exact 𝜌 𝑝,𝑘 . Verification checks the common local domain, operation and effect digests, pfc
strict causal order 𝑘 ≺𝑝 𝑏 𝑝 (𝑐) ≺ 𝜌 𝑝,𝑘 , authenticated admission and barrier positions, and closure of the future-use, instance, and lineage frontier. The leaf evidence-through boundary is later than the barrier, receipt, and every referenced terminal acknowledgement, so a leaf cannot be signed
Authorization Revocation for Long-Running AI Agents
35
first and completed retrospectively. Missing or conflicting evidence yields 𝑈 , while contradictory evidence yields 𝑁 ; neither permits the certificate. Now consider any admissible extension after issuance and suppose it contains the earliest new commitment authorized by 𝑎𝑐 , at sink 𝑝. The monotone barrier 𝑏 𝑝 (𝑐) already exists, so the new admission is later in ⪯𝑝 and A5 rejects it. The carrier cases independently reach the same conclusion. An effect-closed or terminal carrier cannot reach a commit gateway. A PRE_FENCE_COMMITTED carrier can settle only the exact effects named by its typed receipts because its future-use, instance, and lineage frontier is closed. An independently rebound carrier’s selected witness excludes 𝑎𝑐 by Lemma 3. Lemma 1 also excludes creation or expansion of new issuer-side authority under 𝑎𝑐 . A cross-endpoint handoff cannot escape these cases. Exact projected-token equality gives every token in the frozen frontier one valid terminal disposition, and every acceptance maps causally to a covered destination carrier before its terminal accounting. By A7 and ChannelsClosed(𝐸), the sole authoritative creation event for each old-atom token is SEND(𝑡), SEND(𝑡) ≺ 𝑐, and 𝑡 ∈ 𝑇𝑐 . Every relevant endpoint barrier causally follows the authenticated cut, so SEND(𝑡) ≺ 𝑐 ≺ 𝑏 𝑝 (𝑐). After the barrier, the registered channel profile rejects new ingress selected under 𝑎𝑐 or records a concrete blocker. Consequently every dependent carrier has a certified terminal, closed, PRE_FENCE_COMMITTED, or independently rebound state, all old-atom handoffs in 𝑇𝑐 are accounted for, every cut-relevant old-atom pre-fence acceptance is typed and closed, and no post-barrier admission under 𝑎𝑐 exists in the prefix or any extension. These are precisely the clauses of RQ(𝑐). □ Proof of Theorem 2. For part (1), consider two manifested endpoints 𝑝 and 𝑞. Endpoint 𝑝 has closed its local carrier after emitting token 𝑡, and exports SEND(𝑡) ∈ 𝑂 𝑝 . Before delivery, 𝑞’s stable local inventory contains no carrier. Both endpoints can truthfully report that their local carrier sets are closed, yet 𝑡 can subsequently create a destination carrier if no terminal disposition or destination fence is required. The local statements alone are identical to a trace in which 𝑡 was rejected. The composite distinguishes the traces only by requiring a unique ACK(𝑡, 𝑑) and, for acceptance, coverage of the resulting carrier. Equivalently, composition requires equality of the canonical token projections 𝜋𝑡 (𝑂 (𝐸)) and 𝜋𝑡 (𝐵(𝐸)); it does not equate the differently typed send and acknowledgement records. Therefore local closure does not compose without token conservation. For part (2), fix all visible evidence and consider an opaque reachable endpoint 𝑝. In world 𝑤 0 , 𝑝 has no residual root-dependent carrier. In world 𝑤 1 , it has one delayed callback holding 𝑎𝑐 and able to commit a protected effect. By hypothesis, 𝑝 exposes neither an inventory capable of distinguishing these states nor a fence/frontier that eliminates the callback’s effect path. Every observation available to a verifier outside 𝑝 is therefore the same in 𝑤 0 and 𝑤 1 . Any deterministic or randomized verifier receiving the same observation has the same output distribution in the two worlds. If it returns 𝑄, it is unsound in 𝑤 1 ; if it never returns 𝑄, it is incomplete in 𝑤 0 . No observer of the remaining evidence is both sound and complete. Recording the missing endpoint as 𝑈 preserves soundness and identifies the exact evidence or enforcement capability needed to resolve the verdict. □ A.4
Preservation, algebra, and recovery
Proof of Theorem 3. By premise, 𝑊 ′ is a registered sufficient witness, excludes 𝑎𝑐 , and is current. Definition 3 re-runs authorization under 𝑊 ′ and atomically installs it as the selected witness. The resulting carrier therefore has exercisable authority derived from every atom in 𝑊 ′ , not from 𝑎𝑐 . Retiring 𝑎𝑐 changes neither the epoch nor the grant digest of an atom in 𝑊 ′ , so the cut cannot invalidate that derivation.
36
Zhu and Wang
The rebind receipt proves the support change to the leaf verifier, permitting the carrier to leave 𝐷𝑐 without being terminated. The composite certificate names 𝑎𝑐 and is evaluated only against dependencies selected under that atom; it contains no transition revoking an atom in 𝑊 ′ . Thus the protocol removes exactly the retired root’s contribution while preserving independently supported work. A later change to an atom in 𝑊 ′ is handled by its own epoch transition and is outside this certificate’s effect. □ Proof of Theorem 4. Fix compatibility header 𝜒. For each leaf identifier, the merge rule is the scalar operation ⊥ ⊔ 𝑧 = 𝑧,
𝑧 ⊔ 𝑧 = 𝑧,
𝑧 ⊔ 𝑧 ′ = conflict
(𝑧 ≠ 𝑧 ′ ),
with conflict ⊔ 𝑧 = conflict. This is the join on a flat domain whose bottom is absence and whose top is authenticated conflict. Its case definition is associative, commutative, and idempotent. Finite pointwise products of such joins retain all three properties. Header disagreement maps to the same absorbing conflict element, so it does not change the argument. The canonical composite serialization sorts leaf identifiers and token keys; therefore equal maps have equal composite digests independent of message arrival order. Definition 5 is a pure function of that map, its verified facts, and the frozen manifest. Duplicate delivery changes none of them. Different authenticated bodies under one leaf identifier remain at conflict, which triggers 𝑈 and cannot be overwritten by a later duplicate. The digest and verdict are consequently merge-order independent. □ Proof of Theorem 5. Partition a crash around each security-changing transaction’s durable linearization point. Before the point, recovery observes no transition and a retry may execute normally. After the point, recovery observes the complete transition and the same idempotency key returns its committed result. A3 and A9 make epoch advances, cut records, fences, terminal carrier states, closed frontiers, and terminal token dispositions monotone. A retry proposing a different body under the same key is authenticated conflict, never a replacement. An old grant request names retired epoch 𝑒, so every later issuer transition fails after the cut advances 𝑟 to 𝑒 + 1. A replayed carrier message is handled separately at its manifested endpoint: before the local barrier it remains an explicitly accounted transfer or acceptance, and after the barrier it is rejected. A replayed fence or close record is idempotent. A second token disposition violates the unique canonical token binding and becomes a conflict. A rebind receipt is bound to 𝑐𝑖𝑑, carrier id, old and new support digests, exact operation and effect-envelope digests, profile digest, and a single-use transition key; replay can neither rebind another carrier, widen its effect envelope, nor create a second accepted transition. For certificate issuance, the authenticated certificate binds 𝑞𝑖𝑑 and ℎ𝑞 , and the durable issuance record commits (𝑐𝑖𝑑, 𝑞𝑖𝑑, ℎ𝑞 , 𝐻 (𝐸), 𝑠𝑐 , C𝑐 ), where ℎ𝑞 digests the canonical pre-certificate body. Repeating that exact identifier and candidate digest finds the durable record and returns the identical signature and certificate identity. Reusing 𝑞𝑖𝑑 with a different body is an idempotency conflict; using another request identifier for the already completed 𝑐𝑖𝑑 is a conflicting remint. A9 rejects both cases. Certificate replay therefore states the same historical fact and cannot upgrade different evidence or mint a second certificate for the generation. For locality, let root identifier 𝑟 ′ ≠ 𝑟 be absent from the frozen manifest dependencies and from rid(𝑊 ) for every selected witness 𝑊 represented by 𝐸. Advancing 𝑟 ′ ’s epoch or changing its ledger phase alters none of 𝜒, the leaf bodies, channel reconciliation, rebind receipts, or frontier facts on which 𝑉𝑐 (𝐸) depends. The canonical projection used to verify C𝑐 is unchanged. Hence unrelatedroot advancement cannot invalidate the root-relative certificate, while any shared selected witness would, by definition, make the root related and require fresh evidence. □
Authorization Revocation for Long-Running AI Agents
A.5
37
Conditional convergence
Proof of Theorem 6. Lemma 1 prevents issuer-side creation or expansion of authority selected under 𝑎𝑐 after 𝑐. A10 and fair execution install every manifested 𝑏 𝑝 (𝑐); A5 then prevents further commitment admissions under 𝑎𝑐 at each sink. Pre-cut tokens delivered or accepted while barriers are propagating remain in 𝐷𝑐 through their exact channel records rather than escaping the population. A11 directly supplies finiteness of the complete cut-dependent population of carriers, effects, and tokens, and ensures that each emitted token is eventually delivered to a covered destination or obtains an authenticated fence-reject or enforced-expiry disposition. After the last required barrier is durable, consider the finite set of unresolved cut obligations. It contains one obligation for every dependent carrier not yet closed, terminal, PRE_FENCE_COMMITTED, or rebound; every token without a valid terminal disposition; every missing fence/frontier attestation; every transient pre-certification unknown or resolvable state disagreement; and every missing compatible leaf scope. Token acceptance transfers the same causal obligation from in transit to a covered destination carrier, so it does not remove the obligation from this set prematurely. Under A7, A10, A11, and the theorem premises, fair execution eventually discharges each member. Monotonicity prevents a discharged terminal fact from reopening, and A10 clears transient pre-certification unknowns and state disagreements. An authenticated same-key equivocation is absorbing for the generation and would permanently preclude 𝑄; the theorem’s no-equivocation premise excludes that case rather than treating it as clearable evidence. The resulting compatible evidence covers every manifest scope and every provider frontier. Each 𝑝 acceptance in 𝐾𝑐 precedes its local barrier and has an exact typed receipt, every continuing carrier has an admissible state, and 𝜋𝑡 (𝑂 (𝐸)) = 𝜋𝑡 (𝐵(𝐸)) with each acceptance linked to a covered carrier. A5 excludes an accepted post-barrier commitment, so there is no 𝑁 witness; A10 leaves no 𝑈 fact. Definition 5 returns 𝑄, and the verifier issues C𝑐 . Before all obligations discharge, a concrete open element produces 𝑁 or a missing, opaque, or conflicting fact produces 𝑈 ; neither authorizes a certificate. □ References [1] A2A Project. 2026. Agent2Agent (A2A) Protocol Specification, Version 1.0.0. Protocol specification. https://a2aprotocol.org/v1.0.0/specification/ Accessed 12 September 2026. [2] Lujo Bauer, Scott Garriss, and Michael K. Reiter. 2005. Distributed Proving in Access-Control Systems. In 2005 IEEE Symposium on Security and Privacy. IEEE Computer Society, Oakland, CA, USA, 81–95. doi:10.1109/SP.2005.9 [3] Ajay Chander, Drew Dean, and John C. Mitchell. 2001. A State-Transition Model of Trust Management and Access Control. In Proceedings of the 14th IEEE Computer Security Foundations Workshop. IEEE Computer Society, Cape Breton, Nova Scotia, Canada, 27–43. doi:10.1109/CSFW.2001.930134 [4] K. Mani Chandy and Leslie Lamport. 1985. Distributed Snapshots: Determining Global States of Distributed Systems. ACM Transactions on Computer Systems 3, 1 (Feb. 1985), 63–75. doi:10.1145/214451.214456 [5] Moonwon Choi, Seokho Jeong, and Seunggeun Lee. 2026. ResidualAuth: What Authorization State Must Language Agents Preserve under Revocable Delegation? arXiv:2609.08062 [cs.AI] https://arxiv.org/abs/2609.08062 Version 1, submitted 8 September 2026. [6] Edoardo Debenedetti, Jie Zhang, Mislav Balunović, Luca Beurer-Kellner, Marc Fischer, and Florian Tramèr. 2024. AgentDojo: A Dynamic Environment to Evaluate Prompt Injection Attacks and Defenses for LLM Agents. In Advances in Neural Information Processing Systems, Vol. 37. Curran Associates, Inc., Vancouver, BC, Canada, 82895–82920. doi:10.52202/079017-2636 [7] Saurabh Deochake. 2026. Heartbeat-Bound Hierarchical Credentials: Cryptographic Revocation for AI Agent Swarms. arXiv:2605.20704 [cs.CR] https://arxiv.org/abs/2605.20704 Version 1, submitted 20 May 2026. [8] Edsger W. Dijkstra and Carel S. Scholten. 1980. Termination Detection for Diffusing Computations. Inform. Process. Lett. 11, 1 (1980), 1–4. doi:10.1016/0020-0190(80)90021-6 [9] Hector Garcia-Molina and Kenneth Salem. 1987. Sagas. In Proceedings of the 1987 ACM SIGMOD International Conference on Management of Data. Association for Computing Machinery, San Francisco, CA, USA, 249–259. doi:10.1145/ 38713.38742
38
Zhu and Wang
[10] Cary G. Gray and David R. Cheriton. 1989. Leases: An Efficient Fault-Tolerant Mechanism for Distributed File Cache Consistency. In Proceedings of the 12th ACM Symposium on Operating Systems Principles. Association for Computing Machinery, Litchfield Park, AZ, USA, 202–210. doi:10.1145/74850.74870 [11] Åsa Hagström, Sushil Jajodia, Francesco Parisi-Presicce, and Duminda Wijesekera. 2001. Revocations—A Classification. In Proceedings of the 14th IEEE Computer Security Foundations Workshop. IEEE Computer Society, Cape Breton, Nova Scotia, Canada, 44–58. doi:10.1109/CSFW.2001.930135 [12] Sajjad Khan. 2026. Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives. arXiv:2607.14166 [cs.SE] https://arxiv.org/abs/2607.14166 Version 3, revised 8 August 2026. [13] Moon Lee. 2026. From Revocation to Closure: Verifying Attributable Consequences in AI Agent Decommissioning. RISU Technical Note 2026-01. RISU Institute. doi:10.5281/zenodo.22005109 [14] Ninghui Li, Benjamin N. Grosof, and Joan Feigenbaum. 2003. Delegation Logic: A Logic-Based Approach to Distributed Authorization. ACM Transactions on Information and System Security 6, 1 (Feb. 2003), 128–171. doi:10.1145/605434. 605438 [15] Lifei Liu, Haoran Yu, and Xiaochong Jiang. 2026. VERA: Authority-Preserving Edge Revocation for Federated AI-Agent Workflows. arXiv:2608.30091 [cs.AI] https://arxiv.org/abs/2608.30091 Version 1, submitted 30 August 2026. [16] Torsten Lodderstedt, Stefanie Dronia, and Marius Scurtescu. 2013. OAuth 2.0 Token Revocation. RFC 7009. Internet Engineering Task Force. doi:10.17487/RFC7009 [17] Friedemann Mattern. 1987. Algorithms for Distributed Termination Detection. Distributed Computing 2, 3 (1987), 161–175. doi:10.1007/BF01782776 [18] Model Context Protocol Contributors. 2026. Tasks. Model Context Protocol Tasks extension specification, 2026-07-28. https://tasks.extensions.modelcontextprotocol.io/specification/2026-07-28/tasks Draft extension specification; accessed 12 September 2026. [19] Xabier Muruaga. 2026. Bounded Agents: Delegation Security for Multi-Agent AI Systems. arXiv:2608.15888 [cs.AI] https://arxiv.org/abs/2608.15888 Version 1, submitted 16 August 2026. [20] Jaehong Park and Ravi Sandhu. 2004. The UCONABC Usage Control Model. ACM Transactions on Information and System Security 7, 1 (Feb. 2004), 128–174. doi:10.1145/984334.984339 [21] Soohong Daniel Park and Imran Siddique. 2026. Architectural Requirements for Supporting AI Agents on the Internet. Internet-Draft draft-daniel-ai-agent-internet-architecture-03. Internet Engineering Task Force. https://www.ietf. org/archive/id/draft-daniel-ai-agent-internet-architecture-03.html Work in Progress, published 28 August 2026. [22] Suliu Qin, Haomin Zhuang, Yujun Zhou, Yufei Han, and Xiangliang Zhang. 2026. AIRGuard: Guarding Agent Actions with Runtime Authority Control. arXiv:2605.28914 [cs.CR] https://arxiv.org/abs/2605.28914 Version 1, submitted 27 May 2026. [23] Justin Richer. 2015. OAuth 2.0 Token Introspection. RFC 7662. Internet Engineering Task Force. doi:10.17487/RFC7662 [24] RISU Institute. 2026. Frozen Bounded Agent-Closure Engine v0.3: Normative Phase-1 Specification. Normative software specification. https : / / github . com / risu - research / bounded agent - closure / blob / a46456f028cd3dd1d386111b1faab890a26ae5e9 / SPEC . md Frozen at commit a46456f028cd3dd1d386111b1faab890a26ae5e9; accessed 12 September 2026. [25] Scott Rose, Oliver Borchert, Stu Mitchell, and Sean Connelly. 2020. Zero Trust Architecture. Special Publication 800-207. National Institute of Standards and Technology. doi:10.6028/NIST.SP.800-207 [26] Yangjun Ruan, Honghua Dong, Andrew Wang, Silviu Pitis, Yongchao Zhou, Jimmy Ba, Yann Dubois, Chris Maddison, and Tatsunori Hashimoto. 2024. Identifying the Risks of LM Agents with an LM-Emulated Sandbox. In International Conference on Learning Representations. OpenReview.net, Vienna, Austria, 27031–27098. https://proceedings. iclr.cc/paper_files/paper/2024/hash/7274ed909a312d4d869cc328ad1c5f04-Abstract-Conference.html [27] Jerome H. Saltzer and Michael D. Schroeder. 1975. The Protection of Information in Computer Systems. Proc. IEEE 63, 9 (Sept. 1975), 1278–1308. doi:10.1109/PROC.1975.9939 [28] Igor Santos-Grueiro. 2026. Lingering Authority: Revocable Resource-and-Effect Capabilities for Coding Agents. arXiv:2606.22504 [cs.CR] https://arxiv.org/abs/2606.22504v1 Version 1, submitted 21 June 2026. [29] Igor Santos-Grueiro. 2026. Temporary Authority, Permanent Effects: Commit-Time Authorization for LLM Agents. arXiv:2607.10487 [cs.CR] https://arxiv.org/abs/2607.10487v1 Version 1, submitted 11 July 2026. [30] Igor Santos-Grueiro. 2026. When Does Authorization End? Effect Closure at Provider Boundaries. arXiv:2609.02866 [cs.CR] https://arxiv.org/abs/2609.02866 Version 1, submitted 2 September 2026. [31] The Kubernetes Authors. 2025. Finalizers. Kubernetes documentation. https://kubernetes.io/docs/concepts/ overview/working-with-objects/finalizers/ Last modified 27 April 2025; accessed 12 September 2026. [32] The Kubernetes Authors. 2026. Garbage Collection. Kubernetes documentation. https://kubernetes.io/docs/ concepts/architecture/garbage-collection/ Accessed 12 September 2026.
Authorization Revocation for Long-Running AI Agents
39
[33] Yingzhe Tong, Leyu Dai, and Songhui Guo. 2026. AID-Guard: Stateful Authorization for Delegated Agent Effects. arXiv:2608.21159 [cs.CR] https://arxiv.org/abs/2608.21159v1 Version 1, submitted 21 August 2026. [34] Jacques Wainer, Akhil Kumar, and Paulo Barthelmess. 2007. DW-RBAC: A Formal Security Model of Delegation and Revocation in Workflow Systems. Information Systems 32, 3 (May 2007), 365–384. doi:10.1016/j.is.2005.11.008 [35] Baoyuan Wu, Qingshan Liu, Adel Bibi, Irwin King, and Siwei Lyu. 2026. The Authorization-Execution Gap Is a Major Safety and Security Problem in Open-World Agents. arXiv:2605.11003 [cs.CR] https://arxiv.org/abs/2605. 11003v1 Version 1, submitted 10 May 2026. [36] Mengting Wu, Lin Wang, Yong Zhang, and Jiang Deng. 2026. From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions. arXiv:2609.11596 [cs.CR] https://arxiv.org/abs/2609.11596 Version 1, submitted 10 September 2026. [37] Longhua Zhang, Gail-Joon Ahn, and Bei-Tseng Chu. 2003. A Rule-Based Framework for Role-Based Delegation and Revocation. ACM Transactions on Information and System Security 6, 3 (Aug. 2003), 404–441. doi:10.1145/937527. 937530 [38] Zhaoxi Zhang and Xiaomei Zhang. 2026. Are You Still the Agent I Authorized? Earned Authority under a Fixed Ceiling for Evolving Agents. arXiv:2607.23586 [cs.AI] https://arxiv.org/abs/2607.23586 Version 1, submitted 26 July 2026. [39] Chris Zheng and Geng Yang. 2026. CONTINUITY: Security-Context Contracts for Composable LLM Agent Controls. arXiv:2609.05269 [cs.CR] https://arxiv.org/abs/2609.05269 Version 1, submitted 4 September 2026.