论文用 Tamarin 形式化分析 x402、MPP、ACP、AP2 四个智能体支付协议

智能体支付把用户意图、委托授权、凭证使用、结算和履约拆到多个参与方与阶段，现有规范没有给出可机器检验的跨阶段安全关系。

• 场景：作者称 AI 智能体已代用户购买商品、完成结账并为 API、数据和数字服务付款。x402 在最近 30 天报告超过 7500 万笔交易。与授权和结账耦合更紧的传统支付不同，用户可能在商户或条款尚未确定时就授权任务，后续每一步局部有效，整笔交易仍可能与该授权不一致。
• 现有工作不足：作者称已有研究从协议逻辑、实现行为、运行时攻击和部署安全分析了 x402 与 AP2，更广的工作整理了智能体支付与商务威胁，但没有在异构协议上给出共同的、机器检验的规范级分析。
• 核心问题：哪些安全关系必须贯穿智能体支付工作流，当前协议是否保持这些关系。作者列出三点困难：相关关系分散在规范性正文、schema、示例和参考实现中，绑定与状态约束可能隐式或欠指定；各协议的角色、授权制品、结算机制、信任假设和状态机不同；许多违反只在重试、并发会话、可复用凭证和异步支付或履约的有状态组合中出现。
• 本文做法：用 Tamarin 对 x402、MPP、ACP、AP2 做规范驱动、反例引导的形式化，在共同验证边界内保留协议自身语义，把独立验证过的关系汇总为 18 条跨完整性、支付与服务的安全性质，并对保留的违反构造最小加强的对照模型后重验。
• 威胁模型：
  • 对手：符号 Dolev–Yao 对手控制不可信通信信道，可拦截、修改、抑制、重排和重放消息，发起并发会话，并复用已获得的凭证或授权制品。
  • 智能体：不信任 agent 保持用户意图的交易上下文；它可以选择非意图服务、改参数、重复请求或以非意图方式调用可用凭证。内部原因（如提示注入或推理错误）被抽象掉，只问协议在 agent 发出协议上合法、但可能偏离原意图的动作时是否仍安全。
  • 信任：标准密码原语被假定安全，未妥协方保护长期密钥。钱包或可信授权组件只对其显式认证的交易条款被信任；未以密码学或其他方式显式绑定的上下文不假定受保护。provider、facilitator、支付处理方、registry 和结算系统只在协议分配给它们的已认证陈述或状态转移上被信任。每个协议模型另写其规范所要求的额外妥协、信道或终局性假设。
  • 受害系统：用户把权限委托给 agent，由商户或服务提供方、凭证提供方、facilitator 或支付处理方以及结算轨道共同完成授权、验证、结算与服务交付。

作者把相关工作放在智能体支付协议本身、已有安全分析，以及 Tamarin 这一验证工具上。

• 智能体支付协议
  • x402 与 MPP——把支付接入 HTTP 交互；x402 用 HTTP 402 返回支付要求，客户端重试时携带签名支付载荷，由服务器或可选 facilitator 验证并结算。
  • ACP——协调 agent 发起的结账，商户保持权威结账状态，委托支付 token 按金额、币种、商户、结账会话和过期约束支付使用。
  • AP2——用签名的 Checkout 与 Payment Mandate 编码用户意图、授权约束和已授权交易，并密码学绑定结账、限定范围的支付凭证和签名支付回执。
• 已有安全分析
  • 对 x402、AP2 的细致研究——从协议逻辑、实现行为、运行时攻击和部署安全分析这两个协议。作者称这些工作暴露了重要弱点，但没有给出跨异构协议的共同、机器检验的规范级分析。
  • 更广的威胁整理——把威胁组织到智能体支付与商务系统上。作者同样称其未提供上述跨协议规范级分析。
  • 传统支付——授权与结账耦合更紧。作者用这一点对照智能体支付把授权、支付、结算和履约在参与方与时间上拆开。
• 形式化工具
  • Tamarin——把密码协议建成多重集重写系统，在无界并发会话下做符号验证；对手为 Dolev–Yao，安全性质写成迹上的公式，失败时可给出反例迹。
• 基线与校准来源：已知或校准案例的公开证据，x402 包括此前的协议逻辑分析、具体攻击以及 facilitator 与结算安全分析，AP2 另包括一篇分析；四个协议还审阅官方规范、安全指南、仓库 issue 与 pull request 以及 RFC。作者以此要求证据侧模型复现已记录行为，对照参考模型仍可执行并验证相应约束。论文未把某一套外部工具当作攻击基线，验证对象是钉住修订上的规范与仓库证据。

作者把本文定位为：在保留各协议语义的前提下，用反例引导的 Tamarin 分析回答跨工作流需要哪些安全关系、当前协议是否保持它们，而不是预先假定一套完整性质分类。

整体是 specification-driven、counterexample-guided 的 Tamarin 分析：先在共同角色与生命周期边界里提出源锚定的验证问题，再为每个协议单独抽出可执行语义，用反例归因缺失关系，最后与最小加强的对照模型比较并跨协议归并。

问题设定与验证边界

• 共同角色：user、agent、wallet、provider、facilitator、ledger、registry、observer。wallet 持有或行使支付权限；provider 可以是商户、资源服务器、工具、API 或模型提供方；facilitator 覆盖验证或支付处理；registry 支持发现或市场；observer 能接触支付相关制品但不直接参与交易。同一实现可兼任多角色，职责仍分开，以免从软件共置推断信任。
• 生命周期：意图形成与服务发现、授权、交易发起、服务执行或计量、支付验证与结算、服务交付或结果返回、失败恢复。这些是分析点，协议可以合并、重排或省略。
• 四个域：Integrity（身份、条款、授权与协议语义是否跨角色和阶段一致绑定）、Payment（委托支付是否只产生预期经济效果并留在授权范围与预算内）、Service（所选服务是否在执行、交付、失败与恢复中保持一致）。Table I 给出各域的关注点、主要角色、生命周期跨度和引导问题。不在范围内的是：一般模型质量、商业或监管合规，以及底层密码原语或结算轨道的安全，除非它们直接改变协议级支付语义。

四阶段工作流

1. 定义源锚定性质：用钉住的规范性正文、schema、官方示例和相关仓库制品实例化候选关系，并在跑 Tamarin 之前固定。一条常见对应性质为 φ_P,k ≡ ∀ γ, i. Effect_P,k(γ)@i ⇒ ∃ j. Requirements_P,k(γ)@j ∧ j < i。含义是：协议 P、相关章节 k 下，每个相关效果都要有更早的匹配条件；γ 是参与方、支付条款、资源、会话或凭证等交易上下文。其他案例表达单次使用、守恒、生命周期或不泄露。
2. 建立证据模型：只编码评该性质所需的角色、消息、状态转移和信任假设，保留缺失或可选检查，不为了让性质成立而加条件。在解释全称结果前，用 exists-trace 引理或聚焦见证证明相关支付或服务效果可达；若预期流不可达，先按源证据改模型。
3. 验证并归因：Tamarin 要么证明该性质，要么给出反例迹。人工把迹归为建模错误、显式环境假设、规范所允许的行为、仓库中观察到的行为，或故意削弱的负对照。只有源支持的行为保留为协议发现。反例若暗示另一关系，须回到第 1 步单独验证，不能同时当动机和证据。
4. 对照参考模型：保留相同角色、交易上下文和安全效果，只改所考察的 guard、绑定或状态转移。规范已要求该条件则为 normative reference；没有强制条件则为 patched reference。两侧都必须可执行：证据侧要能到达违反行为，参考侧仍要到达预期协议效果并满足同一性质。

从规范到状态机

• 翻译：把钉住修订上的官方工作流重构成端到端执行，区分强制、推荐、可选和省略行为。Tamarin 规则只保留回答该问题所需的转移；额外约束只出现在对照参考模型里。端到端流在附录 A 至 D。
• 运行示例：x402 的 Cardano Finality-before-Delivery，走 facilitator 提交分支。facilitator 提交交易，Cardano 返回哈希与状态，facilitator 转发，资源服务器授权客户端访问。正文警告内存池或近期区块中的交易可能回滚，但响应 schema 仍允许 status=mempool；confirmed 被推荐但非强制。模型因此同时保留内存池状态上的提前交付和确认后的正常交付。状态机写作 M_Cardano=⟨ Actors, Data, States, Transitions⟩，Actors 为 facilitator F、区块链 B、资源服务器 RS、客户端 C，Data 为交易标识 tx 与状态 s（m 为 mempool，c 为 confirmed）。
• 编码：后续要用的状态做成事实：演化中的支付状态是线性事实，可复用的配置或信任状态是持久事实。每个操作是一条多重集重写规则，动作用 action fact 记下执行者、操作和共享交易上下文。存在网络边界时，公开通信用对手控制的 In/Out。同一 tx 贯穿上链或确认、facilitator 状态、资源服务器交付和回滚，使对应引理不能用一笔交易的确认去证明另一笔的交付。

对照验证与 18 条性质

• 终局性引理：每笔资源交付是否都先有同一 tx 的区块链确认。规范侧证伪该全称性质，并用见证表明存在先按 mempool 交付、随后同一交易回滚的迹。因规范不强制确认，参考模型标为 patched：mempool 状态进入拒绝而不产生可交付状态，确认后的交付路径保持不变。可执行性引理证明新的 mempool 拒绝事件可达，且确认后交付仍可达。
• 归并：人工把表达同一安全关系的案例引理归成共享族，只抽象协议专有名称，保留做决定与依赖该决定的参与方、必须绑定的支付或服务上下文，以及所需事件顺序。86 个聚焦案例各有一个主族；次级映射记录同一迹的交叉后果。四个理想化端到端模型演练强制核心流；协议原生的对照模型组检查局部边界。某族只在钉住证据含相关角色、阶段和状态关系时才实例化。形成或修订一族后重扫四个来源，直到不再出现新的源锚定案例或新关系。Table II 列出 P1–P18：完整性 P1、P2、P7、P9、P12、P18；支付 P3、P4、P8、P11；服务 P5、P6、P10、P13–P17。
• 保证边界：证明意味着该模型所有迹满足引理，证伪意味着存在一条违反迹。作者称这是对所编码模型的可靠符号结果，不声称实现、模型或性质完备；Tamarin 不能证明从正文、schema 和代码的翻译是忠实的，源映射和反例归因需要人工审查。

实验设置

• 对象：四个协议 x402、MPP、AP2、ACP 的 Tamarin 模型，共 11,949 行代码、529 条 lemma。其中 269 条 exists-trace 引理用于可执行性或指定见证，101 条证据侧 all-traces 引理被预期反例证伪，159 条 all-traces 引理（含对应的规范或加强性质）被证明。聚合验证脚本跑完所有活跃理论文件并接受每个预期结果；没有 lemma 留下未解决的证明状态。证伪在这里是机器检验证据，表示所建基线允许被考察的行为。
• 案例：86 个 source-mapped 验证案例，映射到 Table II 的 18 条性质。一个案例可出现在多行，因为其引理实例化了多条性质；圈号标识把证据侧反例归因并保留为新发现的那条性质。Table III 含 40 个这样的发现。无圈号只表示该案例–性质对没有被归因为新发现，可以是同一案例的另一性质维度，或已知/校准案例。
• 已知/校准判定：相关行为或安全关系在作者报告截止前已有公开证据。x402 的证据包括此前协议逻辑分析、具体攻击以及 facilitator 与结算安全分析；AP2 另包括一篇分析。四个协议还审阅官方规范、安全指南、仓库 issue、pull request 和 RFC。附录 E 的 Table VI 汇总 46 个案例及支持证据。
• 实现侧：新的 x402 发现在三个实现上评估；十个代表性发现通过实现 PoC、SDK/schema 级见证和源对齐的可执行迹验证，跨越五个安全性质。作者称若干问题仍在调查或缓解中，因此不报告不必要的可利用细节，只报告协议机制、反例和受控验证。
• 成功判定：证据侧要到达违反性质的行为；对照侧（normative 或 patched）仍要到达预期效果并证明同一关系。两侧除所研究的那个决定外保持同一案例上下文。论文未报告统计显著性检验，也未把 LLM 当作评审模型。

主结果

Table III 把 86 个案例映射到 P1–P18，并标出 40 个新发现；正文给出按协议的分解。

协议	新的形式一致性发现	出处
x402	13	Sec. V-C
MPP	12	Sec. V-C
AP2	10	Sec. V-C
ACP	5	Sec. V-C
合计	40（另复现 46 个已知或校准案例）	摘要、Sec. V-A

• 作者的解读：40 个此前未记录的问题覆盖 17 个 Integrity、16 个 Payment 和 7 个 Service 案例，涉及缺失的跨角色绑定、授权与解析歧义、重复效果、结算与交付状态，以及具体的支付制品泄露。作者称局部有效的协议步骤仍可组合成全局不一致的授权、支付或服务结果。
• 范围：作者称该范围限于所分析的快照和所建模的信任边界；这个计数不代表已证实的漏洞。正文在此处截断为 “does not represent demonstrated vulnerabilitie”，后文未在所给文本中给出完整句子。
• 修复：对每个保留的违反，作者隔离缺失的协议关系，构造最小加强的参考模型并重验预期性质。参考侧对应性质在 Table III 所列每个案例中得到验证。

已知或校准案例

• 测了什么：附录 E Table VI 将 46 个案例标为已知或校准，并给出证据来源、问题摘要、对应性质和匹配强度（Direct 或 Partial）。
• AP2 与 ACP 中可见的条目：AP2-07，复发与预算检查缺少验证方侧的原子状态（P3、P8，Direct）；AP2-11，token 释放可以省略 cnf/sd_hash 的 mandate 链绑定（P1、P11、P18，Partial）；AP2-13，确定性结账哈希可以暴露结账内容（P11、P16，Direct）；AP2-14，SDK 评估器不强制复发频率（P3、P8，Direct）；AP2-15，允许的支付工具按 ID 匹配但不按类型匹配（P1、P2、P9，Direct）。
• ACP：ACP-01，必需的 Delegate Payment 可用普通支付数据绕过（P1、P2、P11，Direct）；ACP-02，委托 token 在交易时未重新绑定到完整额度（P1、P2、P7、P11、P17，Partial）；ACP-03，完成操作的幂等性与支付及订单副作用不原子（P3、P4、P6、P13，Direct）；ACP-04，发现/feed 条款在未接受权威结账时被使用（P4、P10、P14、P15，Direct）；ACP-05，渲染卖方提供的原始 HTML 允许标记注入（P9、P14，Direct）；ACP-06，完成操作可以省略所需的认证结果（P4、P7、P14、P18，Direct）；ACP-07，估计的购物车总额被当作最终结账授权（P4、P8、P10、P14，Direct）；ACP-08，归因被回显或冲突会阻断结账（P3、P4、P16，Direct）；ACP-09，营销同意在未展示和选择的情况下被记录（P7、P14，Direct）；ACP-10，认证或支付 token 越过 LLM、代理或日志边界（P9、P11、P16、P18，Direct）；ACP-12，幂等重放下意图迹被回显或复制（P3、P6、P16，Direct）；ACP-13，公开发现与会话能力协商被混淆（P9、P10、P12、P16、P18，Direct）；ACP-16，完成前未强制所需干预（P4、P10、P14、P15，Direct）。x402 与 MPP 的 Table VI 行在所给文本中未完整出现，故不逐条列出。作者称这些案例用于校准：证据侧必须复现已记录行为，对照参考仍可执行并验证相应安全约束。

Cardano 终局性案例

• 测了什么：x402 的 Cardano exact scheme 中，资源交付是否必须先于同一 tx 的区块链确认。规范侧 φ_finality 被证伪；见证 W_spec 表明存在资源在时刻 i 按 mempool 状态交付、同一交易在更晚的 j 回滚的迹。
• 修补后：patched 参考禁止用 mempool 状态启用交付。作者报告 Tamarin 同时证明 φ_finality 与 N_patched：每条可达交付都有同一交易的先前确认，且没有交付可以使用 mempool 状态；确认后的交付仍可达。作者称该比较针对符号理论，不是已部署实现。
• 归属：该案例归入 P5（Settlement and Finality Soundness）。作者称 schema 允许 mempool，正文只是警告可能回滚并推荐确认，因此该迹是规范所允许的行为。

其他消融与分析

• 模型规模：11,949 行、529 条 lemma；269 条 exists-trace，101 条证据侧 all-traces 被证伪，159 条 all-traces 被证明（Sec. V-A）。
• 新发现的域分布：17 个 Integrity、16 个 Payment、7 个 Service（Sec. V-C）。按协议：x402 13、MPP 12、AP2 10、ACP 5。
• 性质覆盖方式：一族并不作为一条泛型引理在每个协议上断言；只在钉住证据含相关角色、阶段和状态关系时实例化（Sec. IV-D）。
• x402 实现侧：三个实现上评估新发现；十个代表性发现、五个安全性质，验证手段为实现 PoC、SDK/schema 级见证和源对齐可执行迹（摘要与贡献列表）。论文未报告各实现的名称、各 PoC 的成功率或查询次数。
• 工作流终止条件：重扫不再产生新的源锚定案例或新语义关系后停止；作者称这是保留案例在验证边界内的系统覆盖，不是穷尽上游或部署行为，也不是穷尽所有可能的安全性质（Sec. IV-E）。
• 负对照：故意削弱的负对照用于校准已有强制要求；建模错误退回第 2 步，不保留为协议发现（Sec. III-C）。论文未单列负对照的条数。

作者指出的局限与后续方向

• 模型相对：Sec. IV-E 写明，证明排除的是所建模型中的每条违反迹，证伪提供的是一条违反的模型迹；这些保证保持为 model-relative。要得出关于引理所表示的模型性质的结论，比较两侧都需要所述效果可达。
• 证明搜索不必终止：同一节写明，对任意协议证明搜索不必终止，因此只报告已完成的结果，并让脚本拒绝警告或缺失结果。
• 翻译忠实性：同一节写明，Tamarin 不能证明从正文、schema 和代码的翻译是忠实的，源映射和反例归因因此需要人工审查。
• 覆盖不是穷尽：同一节写明，不动点式重扫建立的是验证边界内保留案例的系统覆盖，不是模型穷尽每一项上游或已部署行为，也不是 P1–P18 穷尽所有可能的安全性质。作者因此声称的是所编码模型上的可靠符号结果，而不是实现、模型或性质完备。
• 快照与信任边界：Sec. V-C 写明，40 个问题的范围限于所分析的快照和所建模的信任边界。作者并称该计数不代表已证实的漏洞（句末在所给文本中未写完）。
• 负责任披露：引言中的 Responsible disclosure 写明，若干问题仍在调查或缓解中，因而不报告不必要的可利用细节。这是披露做法，不是实验局限；后续是否并入上游，论文未写成已完成。

实验覆盖范围

• 协议与案例：Sec. V-A 对 x402、MPP、AP2、ACP 建立 Tamarin 模型，86 个 source-mapped 验证案例、529 条 lemma，聚合脚本接受全部预期结果，没有 lemma 留下未解决证明状态。
• 已知与新发现：46 个为已知或校准案例，证据映射在附录 E Table VI；40 个为此前未记录的形式一致性发现，按协议为 x402 13、MPP 12、AP2 10、ACP 5，并按域分为 17 个 Integrity、16 个 Payment、7 个 Service。
• 性质实例化：Table II 的 18 族只在钉住来源包含相应角色、生命周期阶段和状态关系时实例化；某案例可映射到多条性质，圈号只标被归因为新发现的那一对。
• 实现级检查：新的 x402 发现在三个实现上评估，十个代表性发现跨五个安全性质，手段为实现 PoC、SDK/schema 级见证和源对齐可执行迹。论文未报告这三个实现的名称、各 PoC 的定量成功率，以及 MPP、AP2、ACP 是否做了同样的实现级验证。
• 对照修复：每个保留的违反都有只改所考察 guard、绑定或状态转移的对照参考，且参考侧性质在所列案例中被验证；Cardano 案例的比较对象是符号理论。论文未报告证明耗时或重复次数。

Jiang 等把 x402、MPP、ACP、AP2 放进同一套 Tamarin 验证边界，检查委托授权与其后的经济效果、服务效果是否跨参与方、状态和阶段保持一致。

智能体可在商户和条款未定前获得授权，授权、支付、结算和履约由不同参与方异步完成。作者认为现有分析没有给出跨这些异构协议的、机器检验的规范级安全关系。

方法是规范驱动、反例引导：八个抽象角色和七段生命周期只用来定位该问什么，每个协议的规则仍从钉住的正文、schema、示例和仓库抽出。验证问题在每次 Tamarin 运行前固定。失败则归因；源所允许的缺口被隔离成一条缺失关系，再做成只改该决定的 normative 或 patched 对照模型，两侧都要可执行。独立验证后的关系归成 Table II 的 P1–P18，重扫直到不再出现新案例。运行示例是 x402 Cardano：schema 允许 mempool 状态交付，而该状态之后可以回滚；修补后的模型要求交付前有同一 tx 的确认，同时保留确认后的正常交付。

模型共 11,949 行、529 条 lemma。86 个验证案例中，46 个复现已知或校准行为，40 个是此前未记录的形式一致性发现：x402 13、MPP 12、AP2 10、ACP 5，域上为 17 个完整性、16 个支付、7 个服务。101 条证据侧全称引理被预期反例证伪，159 条全称引理（含对照性质）被证明。新的 x402 发现在三个实现上评估，其中十个、跨五个安全性质，由实现 PoC、SDK/schema 见证和源对齐可执行迹支持。

作者的结论是：局部有效的协议步骤仍可组成与委托授权不一致的支付或服务结果，因此委托授权必须与其后的经济和服务效果在参与方、状态和协议阶段上保持一致。作者同时把这些结论限定为所编码模型上的符号结果，不声称实现或性质完备，并称 40 这个计数限于所分析快照与所建信任边界，不代表已证实的漏洞。