A Formal Analysis of Agent Payment Protocols

• URL: http://arxiv.org/abs/2609.00060v1
• Date: Sun, 30 Aug 2026 14:04:15 GMT
• Title: A Formal Analysis of Agent Payment Protocols
• Abstract summary: Agent payment protocols are emerging as a key transaction layer for autonomous commerce.<n>We formalize four representative agent payment protocols: x402, MPP, ACP, and AP2 in Tamarin.<n>We use source-backed verification questions and counterexample traces to expose missing bindings, state constraints, and cross-stage correspondences.
• Score: 21.91506763477032
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Zero-Knowledge Predicate Proofs Between AI Agents: A Measured, Cross-Protocol Gateway and the Source-Integrity Gap [0.0]
  Multi-agent AI platforms move quickly from staging to production, but the way agents establish trust remains rudimentary.<n>We take provable data minimisation between agents from proposal to running system.<n>A 32-bit threshold predicate proves in 6.2 ms and verifies in 1.0 ms with a 608-byte Bulletproofs proof.
  arXiv  Detail & Related papers  (2026-08-30T23:16:17Z)
• AgentProv: Auditing Agentic LLM API Providers via Tool-use Policy Probes [38.37599802008238]
  Commercial LLM APIs advertise a specific foundation model, but the served backbone may be silently substituted, quantized, or wrapped.<n>All existing audits decide backbone identity from the text-output channel.<n>We introduce Agentic Provenance (AgentProv), the first action-based identity audit for agentic LLM APIs.
  arXiv  Detail & Related papers  (2026-08-30T08:22:12Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• Preventing Premature Commitment in Coding Agents with an Evidence-Conditioned Execution Layer [38.62073085926841]
  LLM-based coding agents edit source code or submit patches before examining enough repository evidence to justify the change.<n>We present ECLoop, an execution layer that interposes between the agent and the repository to enforce evidence-conditioned execution.
  arXiv  Detail & Related papers  (2026-07-30T20:16:35Z)
• A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
  This study develops a technical taxonomy to classify and analyze large language models (LLMs) agent communication protocols.<n>The framework guides protocol selection and highlights open research gaps such as privacy and policy enforcement.
  arXiv  Detail & Related papers  (2026-06-17T14:45:20Z)
• Agent Name Service (ANS): A Proof-of-Concept Trust Layer for Secure AI Agent Discovery, Identity, and Governance in Kubernetes [0.0]
  This paper presents an implementation-oriented proof of concept for the Agent Name Service (ANS)<n>ANS is a DNS-inspired trust layer for AI agent discovery and interoperability.<n>We observe sub-10ms response in demonstrated service paths and full success for scripted demo deployment scenarios.
  arXiv  Detail & Related papers  (2026-04-29T01:24:27Z)
• Anumati: Proof of Adherence as a Formal Consent Model for Autonomous Agent Protocols [0.0]
  We propose a versioned, append-only consent model for agent-to-agent communication.<n>The model is instantiated as a non-breaking extension to two widely used agent protocols.
  arXiv  Detail & Related papers  (2026-04-16T10:48:21Z)
• SoK: Security of Autonomous LLM Agents in Agentic Commerce [17.16390433047924]
  This paper develops a unified security framework for autonomous LLM agents in commerce and finance.<n>We organize threats along five dimensions: agent integrity, transaction authorization, inter-agent trust, market manipulation, and regulatory compliance.<n>We propose a layered defense architecture addressing authorization gaps left by current agent-payment protocols.
  arXiv  Detail & Related papers  (2026-04-15T01:55:40Z)
• AgentRFC: Security Design Principles and Conformance Testing for Agent Protocols [2.1352949241716352]
  Agent protocols enable autonomous agents to discover capabilities, delegate tasks, and compose services across trust boundaries.<n>Despite massive deployment, no systematic security framework for these protocols exists.<n>We present three contributions: the Agent Protocol Stack, the Agent-Agnostic Security Model, and AgentConform.
  arXiv  Detail & Related papers  (2026-03-25T00:25:02Z)
• CreditAudit: 2$^\ ext{nd}$ Dimension for LLM Evaluation and Selection [44.251742023911135]
  CreditAudit is a deployment oriented credit audit framework that evaluates models under a family of semantically aligned and non adversarial system prompt templates.<n>We show that models with similar mean ability can exhibit substantially different fluctuation, and stability risk can overturn prioritization decisions in agentic or high failure cost regimes.
  arXiv  Detail & Related papers  (2026-01-23T07:53:25Z)
• SmartSnap: Proactive Evidence Seeking for Self-Verifying Agents [45.71333459905404]
  SmartSnap is a paradigm shift from passive, post-hoc verification to proactive, in-situ self-verification by the agent itself.<n>We introduce the Self-Verifying Agent, a new type of agent designed with dual missions: to complete a task and to prove its accomplishment with curated evidences.<n>Experiments on mobile tasks across model families and scales demonstrate that our SmartSnap paradigm allows training LLM-driven agents in a scalable manner.
  arXiv  Detail & Related papers  (2025-12-26T14:51:39Z)
• Binding Agent ID: Unleashing the Power of AI Agents with accountability and credibility [46.323590135279126]
  BAID (Binding Agent ID) is a comprehensive identity infrastructure establishing verifiable user-code binding.<n>We implement and evaluate a complete prototype system, demonstrating the practical feasibility of blockchain-based identity management and zkVM-based authentication protocol.
  arXiv  Detail & Related papers  (2025-12-19T13:01:54Z)
• A Taxonomy and Methodology for Proof-of-Location Systems [42.222053626544366]
  We propose a taxonomy identifying four core domains of Proof-of-Location (PoL) systems.<n>We then introduce a methodology to map application-specific requirements onto appropriate PoL architectures.<n>Overall, this work offers a structured approach to building secure, scalable, and interoperable PoL systems.
  arXiv  Detail & Related papers  (2025-08-19T19:39:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.