PaperlayerView exact revision on arXiv

Source-linked AI summary

A Formal Analysis of Agent Payment Protocols

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

arXiv:2609.00060v1cs.CRcs.AI

TL;DR

Agent payment protocols distribute authorization and transaction effects across actors and stages, but the security relations connecting them remain largely implicit. This paper formalizes x402, MPP, AP2, and ACP in Tamarin using source-grounded verification questions and counterexample traces, identifying and repairing cross-stage inconsistencies across 86 cases. The results support preserving consistent authorization, payment, and service relations across protocol lifecycles.

  • Problem

    Security relations connecting authorization, payment, settlement, and fulfillment remain largely implicit across heterogeneous specifications, schemas, and implementations, while stateful composition makes violations difficult to detect from isolated messages.

  • Method

    The paper formalizes x402, MPP, AP2, and ACP in Tamarin using a common lifecycle abstraction, source-grounded models, verification questions, counterexample traces, and minimally strengthened reference models.

  • Results

    Across 86 source-mapped verification cases, the analysis reproduces 46 known or calibration cases and identifies 40 previously undocumented formal-consistency findings, with representative x402 findings validated through implementations and executable evidence.

  • Takeaways & Limitations

    Agent payment security depends on preserving consistent authorization, payment, settlement, and service relations across actors, states, and protocol stages.

  • Takeaways & Limitations

    The analysis targets protocol semantics rather than complete deployments, so counterexamples and verified properties apply only to the encoded models and stated trust boundaries.

Abstract

from arXiv · show

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.

I. INTRODUCTION

Agent payment protocols distribute authorization, payment, settlement, and fulfillment across actors and stages, leaving key security relations implicit. The paper formalizes four protocols in Tamarin and combines systematic verification with practical validation to identify and repair cross-stage inconsistencies.

  • Motivation: Four protocols—x402, MPP, AP2, and ACP—support agent-mediated payments through differing roles, artifacts, and transaction designs.x402 and MPP integrate payment with HTTP, ACP coordinates checkout, and AP2 uses signed mandates for delegated authority.
  • Motivation: Agent payment workflows separate authorization, payment, settlement, and fulfillment across participants and times, so locally valid steps may compose inconsistently.A user may authorize a task before the final merchant or terms are fixed.
  • Method: The analysis formalizes x402, MPP, AP2, and ACP in Tamarin using source-grounded, counterexample-guided models that preserve protocol-specific semantics.The methodology defines a common verification boundary while deriving each protocol’s executable semantics independently from pinned sources.
  • Results: 18 security properties are instantiated in 86 source-mapped verification cases, reproducing 46 known or calibration cases and identifying 40 previously undocumented findings.Each retained violation is linked to a missing protocol relation, minimally repaired, and reverified.
  • Validation: Ten representative findings spanning five security properties are validated across three x402 implementations through PoCs, SDK/schema witnesses, and executable traces.The paper also reports responsible disclosure to the corresponding developers and maintainers.

B. Tamarin Prover

The paper uses Tamarin to analyze cryptographic protocols through symbolic state transitions and trace formulas. Its verification framework compares heterogeneous payment protocols by examining source-backed relations across roles, lifecycle stages, and security domains without imposing a common execution model.

  • B. Tamarin Prover: Tamarin models protocol messages and evolving state as symbolic multiset-rewriting facts, with rule applications forming traces over concurrent executions.Linear facts represent consumable state, while persistent facts represent reusable information.
  • Verification Method: Security properties are trace formulas whose proofs cover all admitted traces, while failed proofs can expose counterexamples, missing bindings, state constraints, or assumptions.Counterexample traces reveal relevant protocol events and causal dependencies.
  • Verification Framework: The verification framework combines threat assumptions, a scope of security-relevant lifecycle relations, and a workflow that turns each relation into a source-backed Tamarin case with a matched reference.This enables cross-protocol comparison while preserving protocol-specific semantics.
  • Threat Model: The analysis uses a Dolev–Yao adversary that can intercept, modify, suppress, reorder, and replay messages, initiate concurrent sessions, and reuse credentials.The agent is not trusted to preserve the user’s transaction context, while cryptographic primitives and uncompromised long-term keys are assumed secure.
  • Verification Scope: The scope covers integrity, payment, and service relations across identities, terms, delegated authority, economic effects, fulfillment, recovery, and information exposure.Concrete questions are refined by concern, participating roles, and connected lifecycle stages.
  • Verification Scope: Common lifecycle stages and abstract roles support comparison, but protocols may merge, reorder, or omit stages, and the scope excludes general model quality and unrelated cryptographic or regulatory issues.Only source-supported roles, artifacts, actions, states, and stages are instantiated for each protocol.

C. Verification Workflow

The workflow turns source-grounded security questions into validated Tamarin cases, attributes counterexamples, and compares each retained case with an executable matched reference. Cross-protocol relations are consolidated only after independent source validation and verification.

  • Step 1: Define a source-grounded property: Each case begins with a concrete property grounded in pinned specifications, schemas, examples, and repository artifacts.The sources determine the actors, states, conditions, and whether a constraint is mandatory, optional, absent, or repository-observed.
  • Step 2: Build and validate the evidence model: The evidence model encodes only source-supported behavior, preserving missing or optional checks rather than strengthening the protocol to force the property.Reachability is checked before interpreting universal results, preventing vacuous proofs from unreachable flows.
  • Step 3: Verify and attribute the result: Tamarin proves the property or returns a counterexample that researchers attribute using transitions, events, state, context, ordering, and adversary deductions.Cases are classified as modeling errors, environmental assumptions, specification-admitted behavior, repository-observed behavior, or negative controls.
  • Cross-protocol consolidation: Candidate relations exposed by counterexamples are retained only after source validation and a separate verification case, then equivalent relations are consolidated across protocols.The consolidated property families guide another scan until no new candidate relation is identified.
  • Step 4: Compare against a matched reference: A retained case is compared with a matched reference that changes only the investigated guard, binding, or state transition.Both models must remain executable: the evidence model reaches the violating behavior, while the reference preserves the intended effect and satisfies the property.

IV. TAMARIN MODELING

The modeling process reconstructs source-defined protocol executions, preserves their roles, orderings, branches, and optionality, and projects focused cases into executable Tamarin state machines. The Cardano example shows how both violating and normal deliveries remain reachable for matched analysis.

  • Source reconstruction: Protocol reconstruction fixes participating roles, message directions, stage order, and conditional branches before focused Tamarin encoding.Each case then projects only the transitions needed for its verification question while preserving source-defined permitted orderings.
  • Cardano case: The Cardano case retains both mempool-based early delivery and confirmed delivery because the schema permits mempool status while confirmation is recommended rather than mandatory.This preserves source optionality instead of silently imposing a stronger confirmation rule.
  • State-machine abstraction: The abstract Cardano machine contains facilitator, blockchain, resource-server, and client roles, linked by transaction identifier and status-dependent control states.Status is either mempool or confirmed, while reported status alone does not assert finality.
  • Execution paths: The two modeled executions separate a violating mempool-delivery-and-rollback path from a normal path that confirms the same transaction before delivery.The mempool path exposes the finality mismatch, while the confirmed path preserves successful delivery.
  • Tamarin encoding: Tamarin rules encode fresh transactions, alternative linear facts, state transitions, and sender-qualified actions that expose the modeled events.The mempool inclusion rule supports both permitted status reporting and later confirmation.

B. Stateful Cross-Role Encoding

The encoding represents protocol evolution with linear state facts and reusable persistent facts, while action facts record actor-specific operations and shared transaction context. Carrying the same context across roles enforces cross-role binding without adding ordering beyond the source.

  • State and rule encoding: Each protocol operation becomes a multiset-rewriting rule that consumes required facts, produces successor facts, and records an action fact.Linear facts model evolving payment state, while persistent facts represent reusable configuration or trust state.
  • Transition template: A transition maps source states and fact multisets to a role-specific operation recorded with its relevant transaction, session, credential, or payment terms.One abstract state may map to several facts when later operations require independent continuations.
  • Cardano instantiation: The Cardano mempool state is encoded by two facts from one inclusion rule, enabling both status return and later confirmation for the same transaction.These facts represent alternative continuations, not separate transactions.
  • Cross-role binding: Cross-role binding carries the same transaction through inclusion or confirmation, facilitator status, resource delivery, and rollback.Sender-qualified actions prevent a correspondence lemma from using confirmation of one transaction to justify delivery of another.
  • State constraints: The modeled ordering requires status before delivery and delivery before rollback, while mempool delivery does not require confirmation.The encoding therefore preserves the source’s ordering without silently adding a confirmation dependency.

C. Comparative Verification and Attribution

The analysis compares source-grounded protocol cases through explicit correspondence checks, counterexample attribution, matched repairs, and manual consolidation into cross-protocol property families.

  • Comparative verification: Each running case asks whether the required event correspondence holds across specification and patched theories, using the same transaction context and event relation.For finality-before-delivery, confirmation of the same transaction must precede resource delivery.
  • Counterexample attribution: The specification model admits delivery after mempool status without prior confirmation, including a trace where the delivered transaction later rolls back.This behavior is retained only after checking event bindings, transition use, assumptions, and source permissions.
  • Matched repair: The matched patched model rejects mempool-based delivery while preserving the confirmed-status path and the service event.The changed transition consumes the mempool state and enters rejection; confirmed delivery remains reachable.
  • Attribution workflow: A counterexample identifies a violated explicit lemma, while any adjacent relation must return as a separately sourced and verified case.This prevents Tamarin from being treated as an automatic generator of new properties.
  • Cross-protocol properties: The resulting taxonomy groups independently verified lemmas by shared relations while preserving protocol-specific actors, contexts, and event order.The 86 cases receive primary families, with secondary mappings for cross-cutting consequences; coverage does not assert every family for every protocol.

E. Verification Guarantees and Scope

Verification results are guarantees about completed symbolic models and their stated assumptions, not automatic claims about external protocol implementations or exhaustive security properties.

  • Model guarantees: A verified lemma excludes every violating trace generated by the model, whereas a falsified lemma supplies an admitted violating trace.The trace set includes the rules, equations, and trust assumptions of the specific case model.
  • Model assumptions: Universal proofs quantify over all public-actor instantiations rather than one fixed client, server, facilitator, or ledger identity.Actor identity is shared across rules only when the theory explicitly carries the actor term between them.
  • Scope limits: The guarantees remain model-relative because translation fidelity requires human review and the verification boundary does not establish implementation, model, or property completeness.The fixed-point rescan supports systematic coverage only within the retained verification boundary.
  • Verification execution: 11,949 lines of Tamarin code and 529 lemmas comprise the four protocol models, with 269 exists-trace, 101 falsified all-traces, and 159 verified all-traces lemmas.A fresh aggregate run completed in 99.68 seconds of wall-clock time and accepted every expected result.
  • Coverage: Table III maps 86 verification cases to 18 properties, with 40 circled identifiers marking retained counterexamples.Cases may appear under multiple properties, while an uncircled identifier does not by itself indicate absence of a finding.

B. Known Issues

The study calibrates its methodology against documented behavior, then identifies and validates previously undocumented formal-consistency issues across four protocols and selected x402 implementations.

  • Calibration: Known or calibration cases are grounded in prior analyses, official specifications, security guidance, repositories, issues, pull requests, and RFCs.These cases test whether evidence models reproduce documented behavior while matched references verify corresponding constraints.
  • Unknown issues: 40 previously undocumented formal-consistency issues were identified: 13 in x402, 12 in MPP, 10 in AP2, and 5 in ACP.They span integrity, payment, and service cases involving bindings, parsing, duplicate effects, settlement, delivery, and payment-artifact disclosure.
  • Stateful composition: Formal verification exposes violations that static source analysis alone may miss by composing individually permitted events across time and state.MPP-14 combines persisted spend, a lost response, and retry to produce double counting; atomic idempotency excludes the trace while preserving successful execution.
  • Practical validation: Every unknown case received the PoC procedure, with a standalone issue report prepared for each of the 40 findings.Representative findings were selected for further practical validation across five security properties.
  • Implementation fidelity: Across three x402 implementations, findings may reproduce universally or only where the required schemes, extensions, or execution modes are supported.x402-01, 03, 05, 14, and 25 reproduce across all three implementations, while other findings are limited by implementation feature support.
  • Representative findings: The x402 MCP transport can allow conflicting structured and textual payment representations to reach payment creation without first establishing semantic equality.The patched reference requires both representations and their semantic equivalence before authorization or payload creation.
  • Representative findings: ACP-18 leaves end-to-end request semantics conditionally unbound beyond TLS because Signature and Timestamp are optional in mutating-operation contracts.The formal violation assumes a post-TLS trust-boundary failure, not a broken TLS channel.

B. Actor, Endpoint, and Key Authenticity (P18)

The section examines how missing identity, context, retry, and payment–service bindings can admit formally inconsistent agent-payment behavior. It emphasizes that fixes must enforce the missing relation at the security-critical stage.

  • P18 requires authorization-relevant actors, endpoints, and keys to bind to the intended trusted principal.
  • AP2 checkout verification may validate the approved open checkout while omitting the expected final-checkout binding unless the caller supplies its transaction identifier.
  • AP2 authentication results can lack merchant, checkout, amount, audience, freshness, and single-use context, so the contract cannot establish final-checkout ownership alone.
  • MPP retry accounting can duplicate a logical request when spent state updates precede a lost response and no stable idempotency record exists.
  • x402 and MPP expose opposite payment–service correspondence failures: service may precede protected payment, or payment may finalize before recoverable delivery.
  • The findings show that individually valid artifacts can become insecure when provenance, context, effects, or state diverge across protocol stages.

VII. DISCUSSION

The discussion argues that agent-payment security depends on relations preserved across actors, stages, and state transitions, not on isolated message validity. It positions the work as a cross-protocol formal complement to prior analyses and derives practical design principles from the findings.

  • The models cover only protocol semantics and stated trust boundaries, so counterexamples do not imply that every implementation or deployment exhibits the behavior.
  • The 18 properties capture relations identified within the verification scope rather than a complete definition of agent-payment security.
  • Many violations arise when locally valid authorization, payment, settlement, and service decisions refer to inconsistent identities, terms, or states end to end.
  • Formal verification exposes violations involving retries, reusable credentials, delayed settlement, and asynchronous delivery that may not appear in isolated message analysis.
  • The design implications call for consistent constraints across specifications and machine-readable artifacts, explicit cross-stage bindings, and security-state treatment of retries and failures.
  • The work provides a common specification-level analysis of x402, MPP, AP2, and ACP while retaining each protocol’s execution semantics.
  • The conclusion reports 86 source-mapped cases, 18 properties, and 40 previously undocumented findings, with representative validation through implementations, SDK/schema witnesses, and executable PoCs.

APPENDIX

The appendix describes idealized end-to-end workflows for x402, MPP, and AP2, identifying their roles, core transitions, optional paths, and settlement-to-delivery ordering. These abstractions preserve protocol-specific semantics while leaving selected method or wire details abstract.

  • x402: The x402 model uses client or wallet, resource server, facilitator, and blockchain roles, with agent and receipt verifier limited to optional extensions.
  • x402: x402 discovery and signed receipts are optional extensions, while the facilitator–blockchain handoff is represented by Tamarin state facts rather than a prescribed wire encoding.
  • x402: x402’s core path runs from request and authenticated payment terms through exact authorization, facilitator verification, settlement, and bound resource delivery.
  • MPP: MPP abstracts the payment method while modeling a common challenge, credential, settlement, receipt, and resource-delivery workflow.
  • MPP: MPP binds the challenge to resource, amount, recipient, expiration, request digest, and method context, then verifies and consumes the credential before settlement.
  • MPP: After authenticated settlement, MPP returns a receipt and protected resource; method-specific theories refine the backbone with finality, retry, refund, and asynchronous-delivery states.
  • AP2: AP2 separates shopping, authorization, credential issuance, checkout, and payment processing across seven roles, with an optional payment-network path.
  • AP2: AP2’s backbone covers signed checkout and payment mandates, merchant validation, processor context verification, and one signed payment receipt.

D. ACP End-to-End Flow

The ACP flow first establishes and updates authoritative checkout state, then conditionally authenticates the buyer, obtains checkout-bound delegated payment, and creates the order only after payment success. Its idealized model captures this buyer-intent-to-order backbone while separate theories cover additional lifecycle conditions.

  • ACP’s core roles are buyer, agent or client, merchant, payment provider, and conditionally an authentication provider.
  • The authoritative checkout lifecycle creates merchant state containing cart, amount, currency, merchant identity, status, and payment handlers, with update and retrieval operations.
  • Delegated authentication is conditional and is skipped when the authoritative checkout does not require additional payer authentication.
  • The delegated payment allowance is bound to checkout session, merchant, maximum amount, currency, usage mode, and expiration, and the issued token carries the same allowance.
  • After verifying the payment result, the merchant creates the order and returns the completed checkout and signed order for buyer confirmation.

E. Known Issues Mapping

The mapping relates public evidence to the paper’s known and calibration cases, while distinguishing evidence provenance from match strength. ACP examples include replayed intent traces, capability-negotiation confusion, unenforced interventions, unselected marketing consent, and credential crossings across processing boundaries.

  • Evidence mapping: Match strength measures correspondence between public evidence and a formal case, not issue severity, exploitability, proof strength, or deployment reachability.Direct evidence records the same trigger or invariant and security consequence; partial and adjacent indicate narrower or related coverage.
  • Evidence mapping: Table VI maps public evidence to coverage for 46 known or calibration cases using sections, pull requests, RFCs, mitigations, attack subcases, and security rules.The table also defines EVM, SVM, SIWX, and MCP abbreviations.
  • ACP findings: Additional ACP evidence shows marketing consent recorded without being displayed and selected, and authentication or payment tokens crossing LLM, proxy, or logging boundaries.Both findings are reported with direct match strength.
  • ACP findings: ACP evidence records intent traces being echoed or duplicated under idempotent replay.The cited sources are ACP-12 Repository PR 54 and the Intent Traces RFC.
  • ACP findings: ACP evidence identifies confusion between public discovery and session capability negotiation, alongside required interventions that are not enforced before completion.These findings are marked as directly matched to the formal cases.
Loading 2609.00060v1…