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

TL;DR

This paper presents a formal, model-checked analysis of the Lightning Network's single-hop payment protocol. By modeling LN as a finite-state machine and verifying it with the Spin model checker, the authors uncover two security issues: a known congestion attack and a novel Payout Race that can yield ambiguous outcomes and fund loss under network partitions. The work provides a rigorous foundation for security properties, demonstrates practical relevance via a PoC with lnd, and discusses mitigations and limitations inherent to asynchronous two-phase commitments. Overall, the study highlights concrete vulnerabilities in LN's current design, underscores the need for clarified BOLT specifications and robust mitigations, and demonstrates the value of formal methods for validating off-chain payment protocols with real-world impact.

Abstract

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.

Figures (7)

• Figure 1: Each Lightning peer sends a commitment and revocations to its counterparty.
• Figure 2: A finite state machine of the normal payment flow in the Lightning Network. Labels ending in "_T" are timers. Execution starts in FUNDED. Both FAIL_CHANNEL states are equivalent and are duplicated for readability.
• Figure 3: This automaton representing \ref{['prop:p1']} should never generate an accepting run when executed synchronously with the model.
• Figure 4: The execution of an accepting run of the model should never match this automaton representing \ref{['prop:p2a']}. Concretely, a peer should never send a -UPDATE_FULFILL_HTLC directly after receiving a -COMMITMENT_SIGNED ---it should instead send a -REVOKE_AND_ACK before the fulfillment.
• Figure 5: The execution of an accepting run of the model should always match this automaton representing \ref{['prop:p2b']}.