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

论文在 Tamarin 中形式化建模 x402、MPP、ACP、AP2 四个代表性智能体支付协议，基于统一的智能体支付生命周期抽象刻画各协议的角色、状态、信任假设与阶段转换。作者不预设完整属性分类，而是用有来源支撑的验证问题和反例轨迹暴露缺失的绑定、状态约束与跨阶段对应关系，归纳出 18 条共享安全原则。在 86 个验证用例中，分析复现了 46 个已知或校准用例，并识别出 40 项此前未记录的形式化一致性问题。对每个保留的违规，作者定位缺失的协议关系，构造最小强化的参考模型并重新验证目标属性。