该论文针对AI代理支付协议这一新兴的自主商业交易层进行了系统性的形式化安全分析。研究背景在于，AI代理正被授权代表用户购买商品与服务并执行支付，而与传统支付流程不同，此类协议将用户意图、委托授权、凭据使用、结算和履约分散到多个参与方与多个协议阶段，导致单一消息或单一参与者无法强制执行完整的安全保障。然而，现有协议规范、模式和参考实现中的安全保证大多隐式存在，缺乏系统的形式化验证。论文选择了四种具有代表性的代理支付协议：x402、MPP、ACP和AP2，并在Tamarin验证器中对其建模。作者基于代理支付生命周期的公共抽象，构建了源自源码的模型，捕获各协议的角色、状态、信任假设及生命周期转换。分析并非先验地假定完整的属性分类，而是通过源码支撑的验证问题和反例轨迹，揭示缺失的绑定关系、状态约束和跨阶段对应性，并将结果归纳为18条共享安全原则。在总共86个验证案例中，研究复现了46个已知或校准案例，并识别出40个此前未记录的正式一致性发现。对于每个保留的违规案例，作者隔离出缺失的协议关联，构建最小增强的参考模型，并重新验证目标属性。论文还针对x402的新发现评估了三个实现，并通过实现PoC、SDK/模式级证据和源码对齐的可执行轨迹验证了十项代表性发现，涉及五项安全原则。结果表明，委托授权必须与其在跨参与方、状态和协议阶段所产生的经济与服务效果保持一致。该研究适合对AI代理支付安全、形式化验证、协议分析感兴趣的学者与安全工程师阅读，为相关协议的设计与审计提供了可复用的方法论和具体发现。

本文对闪电网络（Lightning Network）的安全性进行了形式化分析。闪电网络是一种支付通道网络，市值超过1.92亿美元，旨在通过链下快速交易解决比特币的可扩展性问题。目前存在多个闪电网络客户端实现，它们都遵循相同的文本规范（即BOLTs）。此前虽有若干漏洞被手动发现，但尚未有工作系统地分析闪电网络的安全性。本文提出了一个形式化框架，用于分析闪电网络中的支付路由和通道拥堵场景，重点关注“支付竞赛”（Payout Races）和“拥堵通道”（Congested Channels）这两种可能引发安全问题的情形。研究者定义了安全属性，并基于BOLTs规范建立了抽象模型，通过形式化方法验证了在竞争性支付和通道容量受限条件下，协议可能出现的死锁、资金锁定或不当结算等问题。论文还讨论了现有实现与规范之间可能存在的偏差，并指出了潜在的攻击面。该工作的主要贡献包括：首次对闪电网络进行系统性形式化安全分析、识别出若干先前未被发现的设计缺陷，以及为后续改进BOLTs规范和客户端实现提供了理论依据。适合对区块链安全、形式化验证和支付通道网络感兴趣的研究人员阅读。

本文首次对BIP32（比特币改进提案32）钱包系统进行了完整的形式化安全分析，无需任何修改。BIP32自2012年引入以来，已成为最常用的比特币钱包之一，但此前缺乏对其具体安全属性的严格证明。该研究基于Das等人（CCS '19）的近期工作，提出了分层确定性钱包系统（如BIP32）的形式化安全模型，并在此模型下，从BIP32使用的ECDSA签名算法的存在性不可伪造性出发，给出了安全性归约。最后，作者给出了BIP32标准实现所能达到的具体安全参数估计，并展示了通过采用替代密钥派生方法，可以在不增加额外成本的情况下将安全强度提升约20比特（从91比特提升至111比特）。该工作为BIP32钱包的安全性提供了坚实的理论基础，并对密钥管理实践具有重要指导意义。