智能体支付协议的形式化分析

中文摘要 AI 辅助

智能体支付协议正成为自主商务的关键交易层，使AI智能体能够代表用户购买商品与服务并执行支付。与传统支付流程不同，它们将用户意图、委托权限、凭证使用、结算及履行分配至多个参与方与阶段，形成了无单一消息或参与方能强制执行的安全依赖。然而，这些保障在不断演变的规范、模式及参考实现中大多仍为隐含状态，缺乏系统的形式化分析。我们在Tamarin中对四种代表性智能体支付协议：x402、MPP、ACP和AP2进行了形式化。通过智能体支付生命周期的通用抽象，我们构建了基于源的模型，以捕捉各协议的角色、状态、信任假设及生命周期转换。我们未采用完整的属性分类，而是使用基于源的验证问题与反例迹线，以揭示缺失的绑定、状态约束及跨阶段对应关系，并将其整合为18项共享安全原则。在86个验证案例中，我们的分析复现了46个已知或校准案例，并识别出40个此前未记录的形式一致性发现。对于每个保留的违规情况，我们隔离缺失的协议关系，构建最小程度强化的参考模型，并重新验证预期属性。我们还在三种实现中评估了新的x402发现，并通过实现原型（PoCs）、SDK/模式级见证及跨五项安全原则的源对齐可执行迹线验证了10个代表性发现。我们的结果表明，委托授权必须在参与方、状态及协议阶段间与其产生的经济与服务效果保持一致。

英文摘要

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.

发表机构

• Southern University of Science and Technology（南方科技大学）
• Indian Institute of Technology（印度理工学院）
• City University of Hong Kong（香港城市大学）

机构由 AI 辅助整理，请以论文原文为准。