The Lightning Network, a payment channel network with a market cap of over 192M USD, is designed to resolve Bitcoin’s scalability issues through fast off-chain transactions. There are multiple Lightning Network client implementations, all of which conform to the same textual specifications known as BOLTs. Several vulnerabilities have been manually discovered, but to-date there have been few works systematically analyzing the security of the Lightning Network. In this work, we take a foundational approach to analyzing the security of the Lightning Network with the help of formal methods. Based on the BOLTs’ specifications, we build a detailed formal model of the Lightning Network’s single-hop payment protocol and verify it using the Spin model checker. Our model captures both concurrency and error semantics of the payment protocol. We then define several security properties which capture the correct intermediate operation of the protocol, ensuring that the outcome is always certain to both channel peers, and using them we re-discover a known attack previously reported in the literature along with a novel attack, referred to as a Payout Race. A Payout Race consists of a particular sequence of events that can lead to an ambiguity in the protocol in which innocent users can unwittingly lose funds. We confirm the practicality of this attack by reproducing it in a local testbed environment.

@en

Payment channel networks (PCN) enable scalable blockchain transactions without fundamentally changing the underlying distributed ledger algorithm. However, routing a payment via multiple channels in a PCN requires locking collateral for potentially long periods of time. Adversaries can abuse this mechanism to conduct denial-of-service attacks. Previous work focused on source routing, which is unlikely to remain a viable routing approach as these networks grow. In this work, we examine the effectiveness of attacks in PCNs that use routing algorithms based on local knowledge, where compromised intermediate nodes can delay or drop transactions to create denial-of-service. We focus on SpeedyMurmurs as a representative of such protocols. We identify two attacker node selection strategies; one based on the position in the routing tree, and the other on between-ness centrality. Our simulation-driven study shows that while they are both effective, the centrality-based attack approaches near-optimal effectiveness. We also show that the attacks are ineffective in less centralized networks and discuss incentives for the participants in PCNs to create less centralized topologies through the payment channels they establish among themselves.@en