Source-linked AI summary
Runtime Authorization for Resources Acquired by AI Agents
Genliang Zhu, Chu Wang
TL;DR
Transaction and fulfillment checks do not determine whether an acquired resource may become usable authority, a gap that spans agentic resource acquisition. The paper proposes quarantined, provenance-bounded activation over actual capabilities and current acquisition graphs. Across registered tests, the architecture rejects unsafe traces, and none of the 16 unsafe staged MCP-to-Docker paths adds an unauthorized Docker start request.
Problem
Agent transactions can validate payment and fulfillment without deciding whether the actual returned resource may become usable authority.
Source: §1 · pp. 1–2Method
The architecture quarantines outputs and admits resolved capabilities through a provenance-bounded activation decision over a typed acquisition hypergraph and relational envelope.
Source: §1.2 · p. 2, §11 · p. 45Results
None of the 16 unsafe paths in the registered 18-case staged MCP-to-Docker composition added an unauthorized Docker start request.
Source: §11 · p. 46Takeaways & Limitations
Payment, budget, identity, tool, and provider-native controls retain their roles but do not serve as activation certificates for newly acquired resources.
Source: §11 · p. 46The guarantee covers registered resource-to-authority transitions under authenticated or independently observed evidence and complete mediation, not general right-acquisition safety or hidden real-world consequences.
Source: §1.4 · p. 3, §10.3 · p. 45
Abstract
from arXiv · showhide
By acquiring compute, credentials, accounts, services, and other agents, autonomous AI agents can introduce new authority into a task. Payment, budget, OAuth, mandate, and fulfillment checks can validate transaction conditions without deciding whether a returned resource may become usable authority. This post-fulfillment activation gap spans tool-mediated creation, inter-agent delegation, and agentic commerce. We present a provenance-bounded runtime authorization architecture. It quarantines acquired outputs, resolves their actual capabilities from authenticated provider evidence through a versioned resolver, and activates them only through a current activation transaction that checks the resolved manifest, provenance, epochs, and a downward-closed relational envelope over a typed resource-capability hypergraph. The envelope preserves correlated identity, effect, data, delegation, and graph-wide limits. Single-use effect permits are revalidated and consumed at effect linearization. Under explicit assumptions, we prove eight safety properties covering quarantine, backing, non-amplification, split non-evasion, crash/retry, refunds, epochs, and effect confinement. Across five resource classes, reference semantics accepted 20/20 benign traces and rejected 40/40 registered unsafe traces over 810 events; an independent checker agreed on 60 base and 40 refinement traces and rejected 89/89 tamper tests. Frozen Codex and Gemini Model Context Protocol (MCP) client components completed 54/54 deterministic local stdio calls. In a registered 18-case staged MCP-to-Docker composition, both benign paths completed, and none of the 16 unsafe paths added an unauthorized Docker start request. A five-source audit classified 1,248 field pairs across 32 units; no unit alone supplied a complete activation profile.
1 Introduction
Acquisition can create new authority even when transaction-side checks pass, so the paper places a separate authorization decision after fulfillment and before resource use. It formalizes this decision with a provenance-bounded architecture and evaluates it within registered, mediated profiles.
1 Introduction
- Transaction-side checks can validate payment, budget, OAuth, and tool conditions without deciding whether a returned resource may become executable authority.The same authorized cloud-create call can return resources with different action surfaces.Source: §1 · p. 1
1.1 The post-fulfillment activation gap
- Activation is a new authorization decision over the actual resource capability and the complete current acquisition graph, distinct from proposal, reservation, dispatch, quarantine, and resolution.A paid, delivered output can still be denied activation; a refund does not necessarily destroy a live capability.Source: §1.1 · p. 2
1.2 Approach
- A typed resource-capability hypergraph and relational, downward-closed envelope preserve correlated identity, co-possession, cardinality, delegation, and graph constraints across grants in one authority domain.Each active hyperedge has one ordinal-indexed output; multiple outputs occupy distinct, independently admitted singleton-output edges.Source: §1.2 · p. 2
- The architecture quarantines provider outputs, resolves authenticated provider state into an actual-capability manifest, and activates only after validating provenance, epochs, the prospective graph, and a single-use permit.Later protected uses revalidate current lineage and consume a single-use effect permit at the effect linearization point.Source: §1.2 · pp. 2–3
1.3 Contributions
- The paper contributes an indistinguishability result, a quarantine-before-activation protocol, eight conditional safety results, and an evaluation spanning five resource classes and independent checking.The evaluation also includes runtime mappings, MCP client components, and a staged MCP-to-Docker composition.Source: §1.3 · p. 3
1.4 Scope
- The guarantee is limited to registered, decidable profiles with completely mediated outputs, identity aliases, and protected effects; arbitrary right-acquisition safety is outside its scope.Missing or indeterminate in-domain evidence cannot authorize activation.Source: §1.4 · p. 3
2 Background and Problem Separation
Existing controls authorize operations, transactions, identities, or declared capabilities, while this paper addresses a separate decision over the actual resource returned after fulfillment. It argues that this decision must preserve relations among capabilities and resources rather than relying only on independent attributes or numeric limits.
2.1 Authorization before and after acquisition
- Authorization and governance approaches address subjects, objects, actions, environments, and allowed autonomy, while this architecture applies them to a transition that adds resources or principals to an agent task.The added decision is over post-fulfillment activation, not a replacement for the existing layers.Source: §2.1 · p. 4
2.2 Commerce and payment protocols
- Commerce protocols provide checkout, payment, order, and fulfillment records, but the decisive activation input is the separately resolved authority of the delivered resource.A correctly delivered resource can still have a default identity or behavior that exceeds the task envelope.Source: §2.2 · p. 4
2.3 OAuth, agent protocols, and tool execution
- OAuth, MCP, A2A, and task-scoped controls provide authentication, delegation, and operation-time inputs; they do not by themselves admit a newly returned resource or principal into the active graph.The admission question arises after an authorized invocation returns authority not yet represented in that graph.Source: §2.3 · p. 5
2.4 Dynamic capabilities and acquisition
- Dynamic-capability governance and negotiation govern declarations and bindings, whereas this architecture governs the distinct transition from a tool call to a provider-created resource with semantic authority.The tool manifest can remain unchanged while the call creates a credential, account, entitlement, or new principal.Source: §2.4 · p. 5
2.5 Why a relational graph is necessary
- Independent allowlists and numeric vectors cannot preserve all acquisition policies, such as forbidding one beneficiary from holding both sensitive-read and external-publish capabilities.Graph-wide conditions such as a maximum number of active descendants are not effect-set inclusion checks.Source: §2.5 · p. 5
3 System, Threat, and Assurance Model
The system inserts quarantine, provider-evidence resolution, and activation between external fulfillment and usable authority. Its threat model includes coordinated adversarial acquisition and retries, while its guarantee depends on authenticated evidence and complete mediation within registered profiles.
3.1 Actors and enforcement boundary
- The enforcement path runs from provider-created output through quarantine and profile-specific resolution to activation-monitor publication of a brokered handle and effect-broker mediation.The architecture separates successful acquisition from executable authority.Source: §3.1 · p. 6, Figure 1 · p. 6
- The agent receives a nonexportable brokered handle rather than raw provider credentials; profiles lacking containment require a remote gateway that consumes the activation permit before use.An interface supporting neither pattern is not an activatable profile.Source: §3.1 · p. 6
3.2 Adversary
- The adversary may coordinate descendants and exploit valid calls, free tiers, aliases, concurrent orders, refunds, retries, crashes, stale profiles, or epoch changes.The model does not allow forged trusted signatures, compromised monitors, broken quarantine, or effects outside declared mediation boundaries.Source: §3.2 · p. 6
3.4 Assets and attack goals
- The protected asset is exercisable authority, and attack goals include unrooted executable resources, envelope violations, premature publication, duplicate active authorities, refund-based resurrection, and stale effects.Unmediated offline resources and hidden provider behavior outside registered evidence profiles are outside the theorem domain.Source: §3.4 · pp. 6–8
4 Formal Model
The formal model represents protected effects, semantic capabilities, actual instances, and acquisition envelopes so that authorization concerns both individual authority and its provenance-bounded aggregate.
4.1 Episodes and semantic capabilities
- An episode records the fields consumed by operation-time policy, including invoking subject, beneficiary, effect, target, data domain, purpose, recipient, state predicate, and validity interval.A target must map uniquely to its registered data domain under the committed map version and digest.Source: §4.1 · p. 8
- A capability descriptor records an episode set together with structural limits such as redelegability, delegation depth, descendant and concurrency bounds, multiplicity, validity, and continuing obligations.Obligations are compared by whether satisfaction of one entails satisfaction of the other across states and episodes.Source: §4.1 · p. 8
- Canonicalization assigns equivalent descriptors the same stable identifier, making the restriction relation a partial order on canonical descriptors.A restricted descriptor is no wider in each structural dimension.Source: §4.1 · p. 8
- An actual capability instance is modeled as an immutable tuple whose canonical instance and provider identities, controller root, beneficiary, actual-manifest root, and epochs distinguish it from surface account names or aliases.Possession of an identifier alone does not make an instance executable.Source: §4.1 · p. 9
4.2 Relational acquisition envelopes
- Independent allowlists for effects, domains, and subjects can admit a forbidden combination because they lose whole-policy correlations.The envelope therefore evaluates relational constraints rather than assuming the Cartesian product of allowed fields is safe.Source: §4.2 · p. 9
- The root envelope binds its issuer, canonical control root, task, contracts, safety predicate, authorized sources and providers, purposes, validity, evidence profiles, reservation profile, and epochs.The grant identifier preserves provenance but does not define the aggregation boundary.Source: §4.2 · p. 9
- The model distinguishes an authority domain from an individual grant so that the envelope can apply to the relevant aggregate rather than treating each grant as an independent boundary.The supplied definition identifies the authority domain as a formal object associated with a grant.Source: §4.2 · p. 9
Its joint safety decision is the conjunction
This section presents activation safety as a current, provenance-bound decision over the acquired resource and normalized shared-domain graph, with single-use permits revalidated at effect linearization. It explains why transaction conditions and componentwise or monetary checks alone cannot ensure the joint envelope, and states eight assumption-bounded safety theorems.
Its joint safety decision is the conjunction
- Joint policy predicates are downward-closed and grant-label-extensional, so fresh grant IDs cannot reset shared-domain limits on counts or co-possession.Policies may constrain worker counts, co-possessed capabilities, redelegation, or data paths; utility and availability are handled by a separate goal predicate.Source: Its joint safety decision is the… · p. 10, §4.3 · p. 11
4.3 Registered conversions and the acquisition hypergraph
- Registered conversions resolve authenticated provider state into typed manifests, fail closed on unbounded unresolved fields, and add outputs as fresh, root-bound edges in an acyclic acquisition hypergraph.The base profile rejects conversions whose capability inputs derive from different roots, while policy accounting still aggregates all roots in the same authority domain.Source: §4.3 · pp. 10–11
4.4 Machine state and authenticated objects
- Acquisition permits authorize dispatch and quarantine only; outputs remain inaccessible until resolved, and activation permits bind exact manifests, graph state, epochs, and single-use slots.A durable outbox is installed before provider send and supplies retries after recovery; prepared outputs remain quarantined until activation commits, and currentness includes valid lineage and matching predecessor rows.Source: §4.4 · pp. 12–14
4.5 Transitions
- CommitActivation rechecks candidate shared-domain safety and atomically consumes its slot with the active row; CommitEffect repeats currentness checks and consumes an effect slot at linearization.Time, epoch, grant-currentness, and dependent-row changes trigger refresh and fencing before a state is observable; mismatches, concurrent time advances, fences, and replays abort before the protected effect.Source: §4.4 · p. 13, §4.5 · pp. 16–17
- Refund settlement changes source evidence without removing the capability; verified destruction requires proof of non-usability and fences dependent descendants, while late successes return to quarantine.The destruction transition retains immutable provenance and advances the affected domain revision.Source: §4.5 · p. 17
4.6 Inductive safety properties
- I1–I5 require exact manifest-bound activations, quarantine before authority, one current rooted derivation, valid conversion edges, and the relational global envelope over all live roots.Created, received, or resolved status alone is insufficient for execution; a valid local conversion bound does not replace the global predicate.Source: §4.6 · p. 17
- I6 permits an effect only when its bound row, active handle, current derivation, episode conditions, epochs, and unused single-use slot validate atomically with the immutable receipt.Source: §4.6 · pp. 17–18
4.7 Necessity and separation results
- A transaction tuple alone cannot decide activation soundly and completely when identical tuples can resolve to outputs that differ in envelope admissibility.Activation therefore needs authenticated post-fulfillment observation or a provider profile that soundly bounds the actual output.Source: §4.7 · p. 18
- Component allowlists can miss correlated co-possession violations, and zero-price acquisitions can violate cardinality or co-possession despite monetary compliance.Source: §4.7 · p. 18
4.8 Safety theorems
- Under stated assumptions, Theorems 1–4 establish quarantine non-authority, backed activation, acquisition non-amplification across grants, and split non-evasion under normalized equivalent additions.The split result requires later fragments to revalidate against the updated domain revision and projection; the first fragment that would cross the envelope is rejected.Source: §4.8 · p. 19
- Theorems 5–7 ensure retries cannot duplicate activation, refunds cannot release semantic capacity, and epoch advances invalidate old permits and handles.Capacity changes require an authorized fence or verified destruction; changed resources require resolution and activation against current state.Source: §4.8 · p. 19
- Theorem 8 confines each accepted effect to a unique single-use permit, a current acquisition derivation, a satisfied relational envelope, and valid episode conditions.The effect result and receipt are atomically bound to that permit.Source: §4.8 · p. 20
5 Provenance-Bounded Activation Design
The design separates acquisition from authority creation: outputs remain quarantined until authenticated provider evidence resolves their actual capabilities and a current activation transaction admits them. Relational graph checks govern both activation and later effects, while durable state and recovery rules preserve those decisions across retries, refunds, and crashes.
5. Provenance-Bounded Activation Design
- The typed, closed acquisition IR rejects unknown kinds, profiles, or fields, while root-bound stable request keys prevent retries or transport-ID changes from creating new semantic slots.The design uses narrow runtime and provider adapters around a common broker, authorization kernel, and separate effect broker; model-generated text is not an authorization input.Source: §5.1 · pp. 20–21, §5 · p. 20
5.2 Three orthogonal state axes
- Commerce, delivery, and authority persist as separate state coordinates, allowing payment settlement, quarantine, and activation outcomes to coexist without a single linear status flag.A multi-output operation has one commerce coordinate but separate delivery coordinates and activation slots for each output ordinal.Source: §5.2 · p. 21
5.3 Proposal and quarantine
- Proposal reserves source authority and persists a current, exact outbox record before dispatch; authenticated receipts enter broker-controlled quarantine, and provider timeouts remain indeterminate.PersistOutboxIfCurrent rechecks the operation, permit, reservation, root, epochs, and clock before dispatch.Source: §5.3 · pp. 21–22
5.4 Resolution and atomic activation
- A versioned resolver derives actual capabilities from authoritative provider state, and activation rechecks the manifest, provenance, epochs, envelope, and single-use slot before publishing a current handle.Unknown required fields need a registered conservative upper bound or resolution fails; commit repeats current-state checks to prevent a time-of-check/time-of-use change.Source: §5.4 · pp. 22, 24, 25
5.5 Relational aggregate evaluation
- The relational envelope evaluates the combined active graph, preserving correlated limits that separate field checks miss and admitting safe output prefixes while leaving violating outputs quarantined.The aggregate check accounts for alias collapse and joint capability possession; each output ordinal has its own activation slot.Source: §5.5 · p. 25
5.6 Operation-time use
- Protected use requires a current lineage and normalized effect inside the capability closure, then revalidates and consumes an exact single-use permit at effect commitment.The permit binds the episode, handle, active record, authority domain, epochs, and root revision; deployments must bind its verification and consumption to effect acceptance.Source: §5.6 · pp. 25–26
5.7 Refunds, retirement, and late results
- Refunds change commerce state, not authority: an active capability remains counted until authoritative destruction or a registered permanent receiver fence proves it cannot be exercised.Late provider success returns to quarantine and must pass ordinary current-state resolution and activation; recovery cannot activate directly from an old permit.Source: §5.7 · p. 27
6 Protocol and Runtime Instantiations
The protocol mappings keep commerce, identity, and tool protocols within their own evidence scopes and add separate post-fulfillment authorization. Runtime adapters and a local container profile instantiate the required interception, resolution, quarantine, activation, and effect-commit boundaries.
6.1 Agentic Payment Protocol
- AP2 checks validate transaction evidence, not an activation certificate or actual-capability manifest; an experimental delivery attestation is explicitly separate from AP2.A successful AP2 check remains logically independent of later resource resolution and activation.Source: §6.1 · p. 28
6.2 UCP, A2A, and MCP
- UCP records commerce and fulfillment evidence, A2A Agent Cards support discovery, and MCP binds tool calls; none alone establishes that a returned resource may become active authority.For MCP, resource-producing results go to quarantine, and use of an acquired handle is separately mediated.Source: §6.2 · p. 28
6.3 Agent-runtime mappings
- Separate Codex and Gemini adapters map audited final MCP client-call requests into shared obligations, requiring stable request identity and complete request context at the broker boundary.The registered profile excludes generic shell execution, direct network access, raw container sockets, and unregistered MCP servers from its complete-mediation claim.Source: §6.3 · p. 29
- The frozen client harness exercises deterministic stdio calls through each runtime’s discovery and dispatch path, while task and request context is supplied as sidecar data bound to observed tool calls.The Codex capture point is source-audited but not directly executed by the harness.Source: §6.3 · pp. 29–30
6.4 Container-resource and composed runtime profile
- The local container profile creates without starting, inspects and resolves the container, then gates start on a certificate and reinspection of that same container.The safe profile pins the image by digest and requires isolation settings; configuration drift invalidates the start certificate.Source: §6.4 · p. 30
- The container experiment establishes broker-side pre-dispatch mediation only, not durable activation-record atomicity, arbitrary cloud policy, compromised-engine containment, or engine-internal effect finality.Its deterministic stimulus uses no model, remote MCP transport, provider, or complete CLI session, and patches no upstream production source.Source: §6.4 · p. 31
6.5 Provider-specific cloud mappings
- Cloud adapters retain native role-passing and service-account controls as evidence, then project registered common fields into the shared manifest; behavior outside that profile remains provider-governed.The cross-provider theorem applies to the registered common fields.Source: §6.5 · p. 31
7 Registered Evaluation
The registered evaluation tests separation, safety, utility, portability, and cost across resource classes and staged integrations. Its finite-run results are tied to frozen fixtures and independent relationship checks; universal safety claims remain conditional proof results, not extrapolations from those runs.
7.1 Questions and hypotheses
- The primary safety criterion is zero unauthorized activation and protected-effect escape in the finite registered denominator; universal claims instead rely on conditional proofs.The registered unsafe families include stronger outputs, splitting, co-possession, retries, stale epochs, and effect-binding drift.Source: §7.1 · p. 32, §7.2 · p. 32
7.2 Resource fixtures
- The primary matrix contains 40 unsafe and 20 benign fixtures across five resource classes, with eight unsafe transforms and four benign controls per class.Separate suites cover 40 refinement traces, runtime-client calls, and local container configurations.Source: §7.2 · pp. 32–33
7.3 Mandatory separating witnesses
- Three release-gate witnesses test paid-but-overpowered credentials, excess free descendant acquisitions, and refund-restored budget while an earlier credential remains active.Additional witnesses combine separately admissible read and publish capabilities, substitute a stronger provider version, and deliver outputs after timeout and retry.Source: §7.3 · p. 33
7.4 Observation-limited separation predicates
- Six observation-limited predicates are tested against the same 60-case corpus, where acceptance is measured only for each registered predicate–fixture pair.Each predicate must pass a baseline self-check; these instruments are not implementations or emulations of external protocols or systems.Source: §7.4 · pp. 33–34
7.5 Independent checker and mutants
- The independent checker reconstructs identities, authority domains, graph-envelope fit, epochs, single-use slots, commit ordering, refund semantics, and effect bindings without importing the reference decision machinery.The 89 registered negative tests do not replace the arbitrary-hypergraph proof obligations.Source: §7.5 · p. 34
- The relationship verifier checks all 40 refinement traces and verifies permit, output, handle, effect, source-reservation, destruction, replay, and target-mapping bindings.It also checks two fail-closed target-map probes and four logical-time advance events.Source: §7.5 · p. 34
7.6 External-source closure
- The external audit covers 32 frozen public-source units across AP2, UCP, A2A, MCP, and RepliBench, establishing field closure rather than attack prevalence.It classifies evidence for each of 39 activation fields across all five registered resource classes.Source: §7.6 · p. 34
7.7 Metrics and reporting
- Reported metrics separate safety, benign completion, latency, and evidence size, with each result bound to frozen records, versions, profiles, and stable error codes.Container execution and runtime-adapter mapping are reported separately from policy-kernel time.Source: §7.7 · pp. 34–35
8 Evaluation Results
The evaluation tests registered semantics, protocol mappings, runtime integrations, and source evidence under explicitly bounded settings. Results support the registered safety outcomes, while finite executions do not establish performance or behavior beyond their stated profiles.
8.1 Semantic separation and independent reconstruction
- 89/89 checker tamper tests were rejected, including independent mutations of every top-level acquisition-permit, activation-permit, effect-permit, and effect-receipt field.The field-complete subsets rejected 23/23, 25/25, 16/16, and 10/10 mutations, respectively.Source: §8.1 · p. 35
- 20 benign traces completed and 40 unsafe traces rejected across five resource classes; the reference execution and independent checker agreed on every fixture.Unsafe rejections occurred during activation, delivery, or effect commit; the registered result table covers safety and composition outcomes.Source: §8.1 · p. 35, Table 7 · p. 39
- All 40 refinement traces agreed under independent reconstruction, including checks of activation and publication currentness, output association, and effect currentness.Expiry, epoch, and manifest drift rejected publication; an unrelated state update and safe graph growth were accepted.Source: §8.1 · p. 35
8.2 Protocol and public-source closure
- The five-source audit classified 1,248 field pairs across 32 units, and no unit supplied a complete activation profile.Only 11 fields were native authenticated, six required an authenticated sidecar, one was independently observable, and 1,230 were unavailable from the source unit.Source: §8.2 · p. 36
8.3 Runtime, crash, and resource evidence
- 54/54 frozen upstream MCP client processes completed deterministic local stdio calls, while the Codex higher-level PreparedMcpCall boundary was source-audited but not executed.The Gemini path reached Client.callTool; the executed Codex path reached RmcpClient::call_tool.Source: §8.3 · p. 37
- The crash harness preserved registered safety outcomes across activation and effect cuts, but did not model hardware loss or faults inside the filesystem’s atomic-write primitive.It also rejected all 32 effect-permit replays and 192 receipt substitutions.Source: §8.3 · p. 37
- Across 18 staged MCP-to-Docker cases, both benign paths completed and all 16 unsafe attempts issued zero unauthorized Docker start-command requests.Twelve cases reached Docker quarantine; four authorized first starts reached effect-permit commit and broker-mediated dispatch.Source: §8.3 · pp. 37–38
8.4 Cost and repeatability
- The local kernel benchmark measured fixed-fixture in-memory phases, while durable I/O, network, provider execution, container creation, and production concurrency were excluded.The 60 serialized traces totaled 2,691,339 bytes; repeated deterministic payloads were compared byte-for-byte, while timing fields remained measurements.Source: §8.4 · p. 38
9 Related Work
Related work supplies foundations for stateful authorization, agent-tool mediation, commerce controls, and cloud identity. This paper distinguishes its focus as deciding whether a delivered provider resource and its relations may enter the active authority graph.
9.1 Protection, usage control, and stateful authorization
- Prior protection and stateful-authorization work models rights acquisition, mutable attributes, and authorization over existing relations; this work controls admission of a newly delivered resource into the active graph.The paper also frames its certificate as checkable evidence for the post-fulfillment transition.Source: §9.1 · p. 41
9.2 Agent authorization and dynamic capabilities
- Agent authorization and runtime systems govern invocations, identity, or declared capabilities, whereas this architecture resolves and authorizes a newly delivered account, credential, environment, or principal before it joins the model.The paper describes ACS as a portable intervention and observability plane whose Guardian supplies policy semantics, not as a guarantee of this activation policy.Source: §9.2 · pp. 41–42
9.3 Payment, commerce, and resource budgets
- Payment, commerce, and resource-budget controls address transaction formation, authorization, or scalar limits; the paper instead holds transaction authorization and fulfillment fixed while evaluating the delivered resource’s semantic authority.A free account, a refunded purchase with a live credential, or co-possession can evade conclusions drawn from scalar limits alone.Source: §9.3 · pp. 42–43
9.4 Cloud identity and autonomous replication
- Native cloud IAM constrains resource–identity bindings and remains in use as evidence, while the proposed architecture applies a common activation invariant across registered resource classes.Resource-acquisition and replication studies motivate descendant acquisition as a security event; this paper contributes access-control semantics rather than a new replication benchmark.Source: §9.4 · p. 43
10 Assurance Boundary
The assurance claim is conditional on registered profiles, evidence quality, and complete mediation. The operational boundary keeps transaction, delivery, and authority as separate state transitions, with only current activation advancing authority.
10.1 What each evidence layer establishes
- Executable evidence tests named observable projections and rejection boundaries of the refinement obligation, not a universal proof for unexecuted states or undeclared deployment paths.The formal results remain conditional mathematical statements; finite observations validate registered implementations and source profiles without enlarging their assumptions.Source: §10.1 · p. 44
10.2 Fail-closed profile admission
- A profile requires policy-relevant output fields to be authenticated, independently observable, or conservatively upper-bounded; failures of quarantine, alias resolution, terminal-state queries, or effect mediation leave the corresponding guarantee unavailable.A narrower profile may still conform when its observable fields and mediation points satisfy the contract.Source: §10.2 · pp. 44–45
10.3 Scope of the guarantee
- The guarantee covers registered resource-to-authority transitions under authenticated or independently observed evidence and complete mediation, not general right-acquisition safety, hidden consequences, objective alignment, or sidechannel resistance.Evaluation is limited to provider-free traces, inert credentials, and local containers under stated profiles; finite zero observations characterize those executions.Source: §10.3 · p. 45
10.4 Operational consequence
- Transaction success may advance commerce state and provider delivery may advance delivery state, but only a current activation record may advance authority state.The separation applies across payment, identity, runtime, and provider systems; adapters must not collapse those transitions.Source: §10.4 · p. 45
11 Conclusion
The conclusion places authorization for acquired resources after fulfillment and before first activation. Its architecture and evidence support that decision within a registered, mediated profile, not an unrestricted production or network-provider setting.
11 Conclusion
- An authorized acquisition does not itself authorize exercising the returned resource, which may be a durable credential, execution environment, service entitlement, or new principal.Such authority may outlive the transaction.Source: §11 · p. 45
- The architecture quarantines outputs, resolves actual capabilities, and admits them through a current activation transaction over provenance, epochs, and the complete prospective graph.It preserves capability occupancy across refunds and consumes a single-use effect permit at effect commit.Source: §11 · p. 45
- In an 18-case staged MCP-to-Docker composition, both benign paths completed and all 16 unsafe attempts issued no unauthorized Docker start request.The evidence concerns frozen client components and broker-mediated local starts, not a complete interactive or model-driven session, network-provider execution, or production deployment.Source: §11 · p. 46
- Payment, budget, identity, tool, and provider-native controls retain their roles but are not treated as the activation certificate for a newly acquired resource.The proposed rule is to require a separate, auditable transition from acquisition to authority.Source: §11 · p. 46
A Proofs
The appendix formalizes transition preservation over finite accepted traces and invokes cryptographic, atomicity, identity, and provider-resolution assumptions only through A1–A11.
- The preservation argument ranges over finite traces generated by Section 4’s accepted transition relation.Source: A Proofs · p. 46
- Rejected transitions leave the security state unchanged.Source: A Proofs · p. 46
- Cryptographic verification, durable atomicity, canonical identity, and conservative provider resolution enter only through assumptions A1–A11.Source: A Proofs · p. 46
A.1 Auxiliary definitions
This section defines guarded transition and refinement semantics for runtime authorization and proves safety properties that bind effects to acquired resources’ current capabilities, provenance, and shared-domain policy. It addresses split operations, crashes, refunds, epoch changes, and why transaction, componentwise, or monetary checks alone are insufficient.
A.3 Safety theorem proofs
- Activation-slot uniqueness and co-commitment preserve at-most-once authority through crashes and retries, without guaranteeing eventual activation.The active row and consumed-slot record commit together; deterministic republication yields the same handle, and recovery uses guarded transitions.Source: §A.1 · p. 47, §A.3 · p. 52
A.1 Auxiliary definitions
- Under A1–A11, invariants I1–I6 hold after every prefix of every fault-extended accepted trace.The proof combines preservation by activation and other accepted transitions with crash and finite-recovery preservation.Source: §A.1 · p. 50
A.2 Separation propositions
- Transaction tuples alone cannot determine activation safety, componentwise allowlists miss correlated capabilities, and monetary compliance does not guarantee acquisition safety.Distinguishing provider worlds requires authenticated actual-output evidence or a sound profile upper bound; zero-price enrollments can exceed a descendant-count limit despite satisfying a spend budget.Source: §A.2 · pp. 50–51
A.1 Auxiliary definitions
- Only successful CommitActivation creates active authority; executable handles require publication for a durable active record.A current derivation requires one live root, authorized source evidence or seeds, committed same-root edges, current epochs and descriptors, active durable rows, and a matching published handle. Implementation refinement requires accepted-step simulation, rejected-step stuttering, and crash recovery from durable state, but does not prove refinement for an unexamined deployment.Source: §A.1 · pp. 46–47, §A.3 · p. 51
A.3 Safety theorem proofs
- Every executable capability has a current derivation from one live provenance root, while relational safety constrains all live roots sharing its authority domain.The domain-wide predicate additionally constrains identities, counts, co-possession, and topology across sibling grant identifiers.Source: §A.3 · p. 51
- Downward-closed domain checks prevent split non-evasion: if a fully activated interleaving would make the aggregate unsafe, its final fragment is rejected.Safe prefixes may remain active; intervening time, epoch, grant-currentness, fence, or destruction changes refresh the projection before the argument restarts.Source: §A.3 · pp. 51–52
- A refund changes commerce evidence but not active authority, so restored money cannot resurrect a semantic slot by itself.The capability remains in the domain projection unless separately fenced, narrowed through ordinary activation, or verified destroyed.Source: §A.3 · p. 52
- After a bound epoch advances, stale activation and effect permits cannot commit, and an old handle cannot obtain a current replacement permit.Activation records and permits bind the complete epoch vector; effect permits also bind the current domain revision.Source: §A.3 · p. 52
- An authority-domain change advances its revision and invalidates a prepared effect permit; only re-resolution and new activation can bind the changed resource to the new epoch vector.The proof’s commit guard checks the domain revision and epoch vector against the permit.Source: §A.3 · p. 53
- Commit checks the complete episode, row root, authority domain, target-to-domain map, epochs, revision, expiry, obligations, and safety envelope before accepting an effect.It also requires the requested effect to belong to the resolved capability and the episode to remain current.Source: §A.3 · p. 53
- Accepted effects remain within the resource’s actual capability and current shared-domain envelope, and cannot be detached from acquisition provenance by a prepare-to-commit race.The commit atomically records effect acceptance and consumes the previously unused effect slot.Source: §A.3 · p. 53
- Substitution, intervening activation or epoch changes, and replay cause commit to abort before the protected effect; success atomically consumes the effect slot.The permit’s epoch or domain-revision check catches intervening fencing, destruction, or grant issuance.Source: §A.3 · p. 53