本文提出 CheckMate 框架，用于全自动化的博弈论安全分析，特别关注区块链技术。CheckMate 将协议建模为博弈，并分析其博弈论安全性，即激励兼容性和拜占庭容错性。该框架要么通过提供防御策略证明协议是安全的，要么给出所有可能的攻击向量。对于不安全的协议，CheckMate 还能在存在的情况下给出使协议变得安全的最弱前置条件。CheckMate 实现了博弈论安全在一阶线性实数算术中的可靠且完备编码，从而将安全分析归约为可满足性求解。此外，CheckMate 还自动化了算术项上高效的分情况处理。实验表明，CheckMate 具有良好的可扩展性，能够分析包含数万亿策略的博弈，这些博弈对比特币闪电网络的阶段进行了建模。该研究的核心贡献在于将博弈论安全推理转化为自动化的求解问题，为区块链协议的安全验证提供了一种新的形式化方法。适合对形式化验证、区块链安全、博弈论应用感兴趣的研究者和安全工程师阅读。

闪电网络是比特币二层支付网络的重要基础设施，其通道两端通常依赖单一在线私钥进行签名，这构成显著的单点故障风险。尽管阈值签名已广泛用于保护链上比特币资产，但至今无法在闪电通道中实际部署。其根本原因在于：将某一通道参与方阈值化，需要在现有两方 MuSig2 多签名协议内部嵌套一个阈值签名方案，同时不能改变 MuSig2 原有的随机数交换流程或消息交互顺序。本文解决了这一难题：首先形式化定义了一种新的密码学原语——嵌套阈值多签名，该原语允许在多签名协议中使其中一方以阈值群组的形式参与；随后基于此原语提出了 Iceberg 方案，这是首个支持嵌套阈值 MuSig2 签名的构造。Iceberg 允许闪电通道的一端以 t-of-n 阈值群组身份运行，同时对外仍呈现为标准 MuSig2 参与方，因此无需修改比特币协议、闪电网络协议或对端节点，即可单方面地在现有闪电网络上部署阈值托管。作者证明了 Iceberg 的安全性，将其原型集成到生产级闪电节点中并完成了性能基准测试。实验结果表明：在容忍一个成员被攻破的阈值群组配置下，通道支付吞吐量仍能达到未修改端点的 93% 以上，仅引入适度开销。该工作为闪电网络通道密钥管理提供了实用的阈值化方案，显著降低单点故障风险，同时保持与现有网络的完全兼容性。适合对密码学应用、闪电网络安全性或密钥管理方案感兴趣的开发者与研究人员阅读。

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

本文提出Blitz，第一个无需两阶段提交就能实现安全的多跳支付方案。在闪电网络等支付通道网络中，多跳支付需要保证原子性：要么所有中间节点都收到资金，要么所有节点都不收到。现有方案依赖两阶段提交（2PC），但2PC在异步网络中可能因中间节点离线或恶意行为导致锁定资金被无限期锁定，且需要复杂的数据结构如HTLC。Blitz通过引入新的密码学原语“条件数字签名”和“可验证秘密重分配”，实现了无需两阶段提交的原子交换。具体地，发送方生成一系列条件签名，中间节点只有在前一跳成功转移资金后才能解锁下一跳，从而避免资金锁定风险。Blitz还支持离线接收方，并提供了对现有闪电网络协议的向后兼容性。实验表明，Blitz在通信轮次和计算开销上均优于基于2PC的方案，通信开销减少约50%。论文还证明了Blitz在通用可组合安全模型下的安全性。该工作对支付通道网络的扩展性和用户体验有重要改进。

比特币闪电网络（LN）作为一种低成本、隐蔽的通信通道，可能被攻击者利用来构建僵尸网络，现有研究如LNBot和D-LNBot只是概念验证，且仅通过模拟评估，缺乏对现实拓扑形成、传播复杂性和抵御拆除能力的深入理解。本文提出LNTest，这是第一个用于评估基于LN的僵尸网络的可重用测试平台。LNTest基于Core Lightning节点构建，使用Docker容器化，并运行在共享的Bitcoin Core regtest链上。它支持三种覆盖拓扑模式：确定性链、自主对等发现和用户提供图，从而能够针对不同的僵尸网络结构进行受控实验。通过LNTest，作者报告了三个主要发现：第一，D-LNBot的自主形成协议不会产生其设计中的均匀链，而是产生一个聚类链，其中团块通过桥接节点相连，移除桥接节点会导致网络碎片化；第二，命令传播规模与僵尸网络大小呈线性关系（Θ(n)），而不是先前声称的O(m log n)，且更高的邻居连通性无助于传播；第三，覆盖拓扑决定了拆除策略的有效性：均匀度链抵抗定向移除但易受随机故障影响，无标度拓扑表现出相反的模式，而自主形成的聚类链在两种攻击下都很脆弱，因此是最易受攻击的。LNTest作为开源发布，附带可重现所有实验的脚本，以支持基于LN的僵尸网络防御的可重复研究。

该论文提出了名为 Horcrux 的新型多跳支付协议，旨在解决支付通道网络（如闪电网络）中因通道耗尽导致支付失败的问题。传统多跳支付存在路径中间节点通道余额被单向消耗殆尽的风险，称为“通道耗尽攻击”，严重影响网络可靠性和流动性效率。Horcrux 通过“合成、分割、转移和存活”四步机制实现通用且增强的多跳支付：首先将支付金额拆分为多个原子部分，通过不同路径并利用中间节点的流动性“合成”支付；若路径上某通道余额不足，则自动执行“分割”操作，将支付拆分成更小的子支付，并“转移”到其他可用路径；同时，系统通过动态调整支付顺序和预留机制“存活”于低流动性环境。该方法不依赖智能合约或中心化协调，完全基于密码学承诺和哈希时间锁定合约（HTLC）的扩展。实验基于真实闪电网络拓扑数据，模拟了不同网络负载和攻击场景下的支付成功率。结果表明，与现有多跳支付方案（如 Atomic Multi-Path Payments, AMP 和 Multipath Payments）相比，Horcrux 在支付成功率上提升约 30%，特别是在高网络拥堵或通道余额分布不均时效果显著；同时，平均支付延迟仅增加不到 10%，额外通信开销可忽略。论文还证明了 Horcrux 对通道耗尽攻击的抵抗力，并给出了形式化安全证明。该工作适用于所有基于 HTLC 的支付通道网络，具有较好的通用性和实用性。