A Formal Analysis of Agent Payment Protocols

Ke Jiang; Mohan Yu; Yuan Chang; Mohit Kumar Jangid; Jianyu Niu; Cong Wang; Yinqian Zhang

cs.CRAug 30, 2026

A Formal Analysis of Agent Payment Protocols

Authors: Ke Jiang, Mohan Yu, Yuan Chang, Mohit Kumar Jangid, Jianyu Niu, Cong Wang, Yinqian Zhang

Organizations: Southern University of Science and Technology · Indian Institute of Technology · City University of Hong Kong

Abstract

Agent payment protocols are emerging as a key transaction layer for autonomous commerce, enabling AI agents to purchase goods and services and execute payments on users' behalf. Unlike conventional payment flows, they distribute user intent, delegated authority, credential use, settlement, and fulfillment across multiple actors and stages, creating security dependencies that no single message or participant can enforce. Yet these guarantees remain largely implicit across evolving specifications, schemas, and reference implementations, with little systematic formal analysis. We formalize four representative agent payment protocols: x402, MPP, ACP, and AP2 in Tamarin. Using a common abstraction of the agent payment lifecycle, we construct source-grounded models that capture each protocol's roles, state, trust assumptions, and lifecycle transitions. Rather than assuming a complete property taxonomy, we use source-backed verification questions and counterexample traces to expose missing bindings, state constraints, and cross-stage correspondences, consolidating them into 18 shared security principles. Across 86 verification cases, our analysis reproduces 46 known or calibration cases and identifies 40 previously undocumented formal-consistency findings. For each retained violation, we isolate the missing protocol relation, construct a minimally strengthened reference model, and reverify the intended property. We further evaluate the new x402 findings across three implementations and validate ten representative findings through implementation PoCs, SDK/schema-level witnesses, and source-aligned executable traces spanning five security principles. Our results show that delegated authorization must remain consistent with its resulting economic and service effects across actors, states, and protocol stages.

Figures & tables

Domains	Concerns	Principal roles	Lifecycle span	Guiding question
Integrity	Binding; semantics; authorization	User, agent, wallet, provider, facilitator, registry	Intent and discovery through authorization, settlement, and result	Do identities, terms, authority, and protocol semantics remain consistent across actors and stages?
Payment	Uniqueness; budget; scope	User, wallet, provider, facilitator, ledger	Authorization through verification, metering, settlement, and recovery	Does each authorized payment produce only its intended economic effects and remain within its authorized scope and budget?
Service	Selection; delivery; lifecycle	User, agent, registry, provider, facilitator	Discovery through execution, delivery, settlement, and recovery	Does execution preserve the selected service and terms, and remain consistent through delivery, failure, and recovery?

TABLE I : High-level verification boundaries for agent payment protocols.

Fig. 1 : Four-stage verification workflow, arranged as two stages per row. Each case begins with a source-backed question. Tamarin checks an executable evidence model, while the researcher explains any counterexample. A normative case is compared with a matched reference; a model correction or a new question returns to an earlier stage.

Fig. 2 : Workflow-style formalization of the Cardano Finality-before-Delivery case. In the evidence trace, the amber box is reached only after both mempool-based delivery and rollback. In the patched trace, the crossed dashed line denotes that

\langle tx,m\rangle

cannot enable delivery; confirmed delivery remains reachable. Here, local label contains event parameters rather than wire messages.

Domain	ID	Property family	Canonical relation
Integrity	P1	Complete Terms Binding	All roles that authorize, verify, settle, or deliver agree on the complete payment context.
	P2	Authorization Completeness	Every economic effect is covered by prior authorization for recipients, bounds, fees, and delegated authority.
	P7	Subject and Entitlement Consistency	The authenticated subject, payer, authorizer, and service recipient agree or are linked by explicit delegation.
	P9	Canonical Transport Semantics	All accepted encodings and transports resolve to the same payment context at every consuming role.
	P12	Extension, Version, and Scheme Downgrade Safety	Unsupported or ambiguous variants cannot weaken the selected protocol semantics.
	P18	Actor, Endpoint, and Key Authenticity	Accepted actors, endpoints, and keys resolve to the intended trusted bindings rather than attacker controlled substitutes.

TABLE II : Cross protocol security property families used in our verification. Each property denotes a canonical relation instantiated by protocol specific Tamarin lemmas.

Panel of Table 5 — TABLE III : P1–P18 coverage. 03 marks the property at which a counterexample was retained as a new finding.

x402 finding(s)	Coinbase [ 38 ]	Thirdweb [ 34 ] / x402-rs [ 39 ]
01, 03, 05, 14, 25	Reproduced	Reproduced
09, 12	Reproduced	Mitigated
08, 19, 24, 28, 29, 30	Reproduced	N/A

TABLE IV : Cross-implementation validation of x402 findings.

Case	Property	Validation level	Validated evidence
x402-28	P9 Canonical Transport	Implementation PoC	A non-canonical MCP challenge reaches automatic payment creation.
ACP-18		Contract / conditional	The OpenAPI contract permits unsigned mutating requests; under a post-TLS trust-boundary failure, no mandatory end-to-end body integrity remains.
x402-01	P18 Actor Authenticity	Client implementation PoC	Payment terms presented through the transport boundary reach payload creation without an explicit server-provenance check.
AP2-17		SDK witness	A distinct Merchant object is accepted through display-field fallback matching when stable IDs are empty.
AP2-02	P1 Complete Terms Binding	SDK witness	Closed-mandate verification can omit validation of the final-checkout binding.
ACP-15		Schema / contract	The authentication-result object does not bind the authoritative final checkout context.

TABLE V : Representative validations derived from formal counterexamples.

Panel of Figure 8 — Fig. 3 : End-to-end x402 workflow used in the formal model. Solid arrows form the core request, verification, settlement, and delivery path. Dashed arrows denote optional discovery and receipt extensions. Dash-dotted arrows denote the facilitator–blockchain handoff represented by Tamarin state facts rather than a prescribed wire encoding.

Panel of Figure 9 — Fig. 4 : End-to-end MPP charge workflow used in the formal model. Solid arrows form the common challenge, credential, settlement, and delivery path. The dotted self-arrow denotes local authentication of the challenge. The dashed arrow denotes payment-method fulfillment whose concrete exchange is intentionally left to the selected payment method.

Panel of Figure 10 — Fig. 5 : End-to-end AP2 workflow. Solid arrows form the shopping, mandate, credential, checkout, and payment backbone. Dotted self-arrows denote local selection, signing, or verification. Dashed arrows denote the optional payment-network path. Dash-dotted arrows show the logical distribution of one payment receipt, which the idealized Tamarin model compresses into the processor-to-merchant receipt and the merchant’s final success response.

Panel of Figure 11 — Fig. 6 : End-to-end ACP workflow. Solid arrows form the checkout, delegated-payment, payment-processing, and order-completion backbone. Dashed arrows denote buyer-facing interactions whose transport is outside the protocol interfaces. Dash-dotted arrows denote optional checkout operations and the conditional delegated-authentication path.

Finding	Evidence source	Issue summary	Properties	Match strength
x402
X402-02	[ 17 ] , Sec. 4.2; [ 16 ] , implementation audit; M3	Payment authorization does not bind the requested resource (“pay A, get B”).	P1, P15	Direct
X402-04	[ 17 ] , Sec. 4.1; [ 16 ] , Attack I-A; [ 35 ] , Free Shopping; SR4	Verification, settlement, and finality are decoupled, permitting delivery before failed settlement.	P4, P6, P13	Direct
X402-06	[ 17 ] , Sec. 5.2	A dynamic request can exceed the remaining payable allowance before failure is detected.	P8, P13	Direct
X402-07	[ 17 ] , Sec. 5.2	Concurrent dynamic requests share an unlocked allowance snapshot.	P3, P6, P8	Direct
X402-10	[ 16 ] , Attack II; M3; repository PRs 2307, 2469	A payment idempotency identifier is not bound to the request/resource fingerprint.	P1, P3	Direct

TABLE VI : Public evidence and P1–P18 coverage for the 46 known/calibration cases. Abbreviations: Sec., section; PR, pull request; RFC, Request for Comments; M, mitigation; D, attack subcase; SR, security rule; EVM, Ethereum Virtual Machine; SVM, Solana Virtual Machine; SIWX, Sign-In-With-X; and MCP, Model Context Protocol.

Explore similar work

Beyond the Mandate: A Systematic Security Analysis of the Agent Payments Protocol (AP2)
Aug 24, 2026Avital Aviv, Parth A. Gandh, Ron Bitton +1LLM Agent Security AI Agent Security
Ben-Gurion University of the Negev Beer-Sheva, Israel
SoK: Security of Autonomous LLM Agents in Agentic Commerce
Apr 15, 2026Qian'ang Mao, Jiaxin Wang, Ya Liu +3LLM Agent Security Agentic Commerce
Nanjing University · Southern University of Science and Technology · City University of Hong Kong
RAILS: Verification-Native Clearing For Agentic Commerce
Jun 7, 2026Adrian de Valois-Franklin, Alex BogdanAgent Reliability Agentic Commerce
Evolutionairy AI · Toronto, Canada

Aug 24, 2026J/K move · Enter open · S save

Beyond the Mandate: A Systematic Security Analysis of the Agent Payments Protocol (AP2)

Avital Aviv, Parth A. Gandh, Ron Bitton, Asaf Shabtai

Ben-Gurion University of the Negev Beer-Sheva, Israel

LLM Agent Security AI Agent Security AI Agent Auditing

Open paper AskPDF arXiv

The Agent Payments Protocol (AP2), introduced by Google, enables large language model (LLM)-driven shopping agents to authorize and execute payments on behalf of users. Its signed Checkout and Payment Mandates protect the integrity of transaction data after signing. Agent interactions and external inputs that shape a transaction before authorization remain outside that protection, including Agent-to-Agent Protocol (A2A) messages and Model Context Protocol (MCP) tool calls. Prior work identified replay and prompt-injection attacks in AP2 v0.1. AP2 v0.2 addresses some of these issues but adds capabilities and deployment assumptions that require renewed analysis. We present a systematic security analysis of AP2 v0.2 based on its roles, transaction lifecycle, deployment architectures, and trust boundaries. We divide the lifecycle into five phases and identify five deployment architectures. Using MAESTRO (Multi-Agent Environment, Security, Threat, Risk, Outcome), we model four threat actors, eleven attack surfaces, eighteen adversary capabilities, and six attacker goals. The resulting catalog contains 48 threats spanning five attack families. We score these threats with the Artificial Intelligence Vulnerability Scoring System (AIVSS), identifying eight that reach the High band in at least one architecture. Because no complete public AP2 deployment was available, we build a testbed spanning all five architectures and develop five proof-of-concept demonstrations covering all eight High-risk threats and their mitigations. We also develop a deployment-aware scanner that maps applicable threats to static, cross-role consistency, and adversarial checks. Our analysis shows that valid mandate signatures alone do not ensure that an agent-mediated transaction reflects the user's intent when its pre-authorization context is manipulated.

Abstract

Explore similar work

Beyond the Mandate: A Systematic Security Analysis of the Agent Payments Protocol (AP2)

SoK: Security of Autonomous LLM Agents in Agentic Commerce

RAILS: Verification-Native Clearing For Agentic Commerce