Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network

本文介绍了闪电网络，这是一个市值超过1.92亿美元的支付通道网络，通过快速的离线交易来解决比特币的可扩展性问题。有多个闪电网络客户端实现，所有这些实现都符合BOLTs规范。虽然已经手动发现了几个漏洞，但迄今为止，很少有工作对闪电网络的安全性进行系统分析。 在本文中，我们采用基础方法来分析闪电网络的安全性，并借助形式化方法进行验证。基于BOLTs规范，我们建立了闪电网络单跳支付协议的详细形式化模型，并使用Spin模型检查器进行验证。我们的模型捕捉了支付协议的并发性和错误语义。然后，我们定义了几个安全属性，这些属性捕捉了协议的正确中间操作，确保结果始终对通道双方都是确定的，并使用它们重新发现了一种先前在文献中报道的已知攻击以及一种新的攻击，称为“支付竞赛”。支付竞赛包括一系列特定事件，可以导致协议中的歧义，使无辜用户不知不觉地丢失资金。我们通过在本地测试环境中复现该攻击来确认其实用性。

分析Lightning Network的安全性，并发现已知攻击和一种新的攻击

使用形式化方法建立Lightning Network的单跳支付协议的详细模型，并使用Spin模型检查器进行验证。定义了几个安全属性，用于捕捉协议的正确中间操作，确保结果始终对通道双方确定，并重新发现了一种已知攻击和一种新的攻击。

使用形式化方法分析Lightning Network的安全性，发现一种新的攻击。在本地测试环境中复现了攻击。论文提供了实验设计和使用的数据集。

最近的相关研究并没有使用形式化方法对Lightning Network的安全性进行分析。