Payout Race

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.

Scalability has long been a struggle for blockchain-based digital currencies (Rizzo, 2016 ) . Payment channel networks (PCN) are one popular solution to this problem. PCNs facilitate participants making payments off-chain, while still maintaining the security properties of the underlying blockchain. The largest PCN in deployment is the Lightning Network (Poon and Dryja, 2016 ) with a peer count of over 49000 49000 49000 49000 and a market cap of over 192M USD 1 1 1 1ml.com/statistics . The Lightning Network (LN) relies on Bitcoin (Nakamoto, 2008 ) as its underlying blockchain.

The Lightning Network operates in three phases: channel establishment, channel operation, and channel closure. In the channel establishment phase, two peers escrow funds between them in a transaction whose output they can only spend with a transaction signed by both peers. In the channel operation phase, the two peers create a new transaction that pays the escrowed funds to the peers. The transaction changes the ratio of how much of the funds goes to each peer and represents the updated channel balance as a result of the payment. The two peers each sign the new transaction with their respective private keys and each send the resulting signature to the other peer, so that both peers have their own signature for the transaction as well as the other peer’s signature. Neither peer publishes this transaction on the blockchain. They store the transaction locally. The transaction serves as protection for each peer. At any time, they can submit the transaction to the blockchain network and retrieve their funds. This funds-retrieval process is called channel closure—the third phase. This protocol was designed by Poon and Dryja ( 2016 ) and later standardized in the form of a specification documents called the Basis of Lightning Technology (BOLT) (BOLT: Basis of Lightning Technology, Lightning Network Specifications ) .

As a result of its growing popularity, the Lightning Network has been subject to numerous attacks in the literature such as the Flood & Loot attack (Harris and Zohar, 2020 ) , griefing attacks (Weintraub et al., 2021 ; Rohrer et al., 2019 ; Pérez-Sola et al., 2020 ; int, ; Mizrahi and Zohar, 2021 ) , the Wormhole attack (Malavolta et al., 2019 ) , which allows intermediaries to steal the fees of others, as well as various privacy attacks, which allow parties to infer sensitive information user identities (Kumble et al., 2021 ; Kumar Sharma et al., 2023 ; Rohrer and Tschorsch, 2020 ; Nisslmueller et al., 2020 ; Tikhomirov et al., 2020 ; Kappos et al., 2021 ) or the amount of funds users own (Herrera-Joancomartí et al., 2019 ; Biryukov et al., 2021 ; Nisslmueller et al., 2020 ; Kappos et al., 2021 ) .

The Lightning Network’s use as a financial medium of exchange underscores the importance of its security, and makes finding any latent security issues a top priority. Most prior attempts to find vulnerabilities in the Lightning Network have done so via manual analysis by domain experts—a difficult and time-consuming process. Only a few works have focused on ensuring the absence of vulnerabilities. Rain et al. ( 2023 ) created a game-theoretic model of the LN, but their model is based on the original 2016 Lightning paper by Poon and Dryja ( 2016 ) and does not reflect the significant changes to the protocol developed since then. Additionally, they model only the channel closure and overlay routing, which —while valuable — are not the phases in which most network communication occurs. Likewise, Kiayias and Litos ( 2020 ) built a theoretical model of the cryptography of the LN based on the BOLTs. This, however, only works under assumptions of idealized functionality and thus does not reflect incorrect behavior that can result under more realistic network and operational conditions. Meanwhile, specific implementations of the Lightning Network such as lnd ( lightningnetwork/lnd: Lightning Network Daemon, ) , CoreLightning ( cor, ) , and Eclair ( ecl, ) are subject to unit tests and code reviews to find and prevent mistakes in said implementations.

One approach for getting assurance the correctness of systems is using formal methods. Unlike testing, formal methods can help disambiguate system specifications and can expose flaws in system requirements, often not captured through testing. They also provide mathematical proofs the system behavior. Formal methods have been shown to be successful for uncovering security flaws in many network protocols including TCP (von Hippel et al., 2020 ; Bishop et al., 2019 ) , TLS (Bhargavan et al., 2017 ; Delignat-Lavaud et al., 2017 ; Cremers et al., 2017 ) , Bluetooth (Arai and Kaneko, 2014 ; Chang and Shmatikov, 2007 ; Nguyen and Leneutre, 2014 ; Phan and Mingard, 2012 ; Wu et al., 2022 ) , and 5G (Basin et al., 2018 ) , and have also seen similar success in cryptographic protocols such as Signal (Kobeissi et al., 2017 ; Cremers et al., 2020 ) , Noise (Girol et al., 2020 ; Kobeissi et al., 2019 ) , Needham-Schroeder (Maggi and Sisto, 2002 ; Lowe, 1995 , 1996 ) , and Diffie-Hellman (Cremers and Jackson, 2019 ) .

The use of formal methods in the blockchain space has been limited, however. A number of works have explored the correctness of smart contracts—in the same vein as program analysis (Amani et al., 2018 ; Annenkov et al., 2020 ; Sun and Yu, 2020 ; Grishchenko et al., 2018 ; Bai et al., 2018 ; Osterland and Rose, 2020 ; Almakhour et al., 2023 ; Nehaï et al., 2018 ; Mavridou et al., 2019 ; Nam and Kil, 2022 ) , one paper explored the correctness of one of Bitcoin’s core protocols (Modesti et al., 2021 ) , and another modeled byzantine fault tolerance in the Red Belly blockchain (Crain et al., 2021 ; Tholoniat and Gramoli, 2022 ) . However, none of these works, nor any others to our knowledge, have sufficiently addressed concerns the correctness of the LN and its associated protocols.

To our knowledge, only one work has applied formal methods to the Lightning Network (Grundmann and Hartenstein, 2023 ) . However, this work abstracts away several important details, which may be the reason why it does not find any vulnerabilities. First, they only model a single payment at a time, which overlooks the complexities of concurrency. Second, they do not model any error conditions, which are important because they represent ways in which the protocol could exit unexpectedly without executing necessary clean up actions. Finally, they define only a single security property, which is too abstract to model any unexpected behavior within the protocol—even if no funds are lost. Additionally, the work is not peer reviewed and the only public artifacts are a short two-page paper (Grundmann, 2021 ) and an extended progress report (Grundmann and Hartenstein, 2023 ) , thus hindering the development of a cumulative literature.

In this work, we build a formal model of single-hop transactions in the Lightning Network payment protocol. We model this protocol as a finite state machine (FSM), as well as provide five security-critical properties that are necessary to protect users’ funds and their accessibility thereof. These properties capture not only the overall successful completion of payments, but also numerous error states not modeled in work. We also define properties that capture the correct intermediate operation of the protocol, thus ensuring that there are no states in which a peer’s view of the transaction outcome is uncertain. The model and the properties were informed by the official Lightning Network BOLTs. We then formally verified this model using the Spin model checker to explore all protocol executions and confirm if any such executions violate our security properties. We find that two of the five properties can be violated. The first violation is a reproduction of the previously published congestion attack (Mizrahi and Zohar, 2021 ) . The second violation lead us to discover a novel attack against the system in which an in-flight payment can end up in an ambiguous state allowing either party to claim the funds—possibly against the expectations of the other peer on the channel (i.e., the counterparty). We call this a Payout Race attack, and we reproduced this attack in a local testbed environment. We mitigations and impact of the attack, as well as limitations of the mitigations techniques due to message timing in distributed systems.

The vulnerability of a financial network is a sensitive matter. While developing stronger defenses to this attack is out of the scope of this work, we have alerted the LN’s security point of our findings and the risks. No perfect defense is possible at this time without a massive redesign of the protocol. However, the LN developers are considering clarifications to the specification documents to inform protocol implementers of various risk factors to be aware of. One popular LN client, lnd , has implemented features in an attempt to limit exposure to this attack. While these mitigations are not a panacea, they do increase the attack difficulty by narrowing the vulnerable time window and might make good candidates for standardization. Though they are all limited by both lack of developer awareness as well as unrealistic uptime expectations. We highlight these efforts and their drawbacks in detail in Section 5 .

Our contributions are the following

We formally model single-hop transactions in the Lightning Network payment protocol as a finite state machine as well as define five security properties. We open source our model and properties for the benefit of the Lightning Network and security communities 2 2 2 .

We show that two of the properties can be violated, thus reproducing a prior attack and leading us to discover the new Payout Race attack.

We show that our novel Payout Race attack is a credible threat by reproducing it in a testbed environment consisting of lnd clients. We confirm that lnd is following the BOLT specifications via manual code inspection.

Payment channel networks (PCN) are a type of financial payment system designed to increase throughput and privacy of blockchain transactions—both of which are salient issues among digital currencies, including Bitcoin. The Lightning Network (LN) is a PCN implementation that uses Bitcoin as its underlying blockchain (Poon and Dryja, 2016 ) .

As the Lightning Network relies on the operation of Bitcoin, it is important to understand the mechanics of Bitcoin transactions. Bitcoin follows the unspent transaction output (UTXO) model for storing and transferring its eponymous digital currency. In the UTXO model, tokens are not fungible. Technically speaking, a user does not spend bitcoins (BTC) directly; a user spends the output of a previously mined transaction—however many BTC that entails. A transaction can have multiple inputs and multiple outputs. We define an output as θ := ( a ⁢ m ⁢ o ⁢ u ⁢ n ⁢ t , ϕ ) assign 𝜃 𝑎 𝑚 𝑜 𝑢 𝑛 𝑡 italic-ϕ \theta:=(amount,\phi) italic_θ := ( italic_a italic_m italic_o italic_u italic_n italic_t , italic_ϕ ) , where a ⁢ m ⁢ o ⁢ u ⁢ n ⁢ t 𝑎 𝑚 𝑜 𝑢 𝑛 𝑡 amount italic_a italic_m italic_o italic_u italic_n italic_t is the value (in BTC for LN), and ϕ italic-ϕ \phi italic_ϕ is some condition that must be satisfied to spend that output. For the case of Bitcoin, we define the condition ϕ italic-ϕ \phi italic_ϕ as a function that accepts some input, and must evaluate to t ⁢ r ⁢ u ⁢ e 𝑡 𝑟 𝑢 𝑒 true italic_t italic_r italic_u italic_e . One important condition for our work is transaction maturity , which is defined as the Bitcoin block number of a future block. It can be specified in relative or absolute terms, and it demarcates a point in time before which a transaction is invalid. A transaction will not be included in a block by an honest miner if it is not yet mature.

We define an input of a transaction as τ := ( r ⁢ e ⁢ f ⁢ ( θ ) , a ⁢ r ⁢ g ⁢ s ) assign 𝜏 𝑟 𝑒 𝑓 𝜃 𝑎 𝑟 𝑔 𝑠 \tau:=(ref(\theta),args) italic_τ := ( italic_r italic_e italic_f ( italic_θ ) , italic_a italic_r italic_g italic_s ) . That is, an input includes a reference to an output along with a vector a ⁢ r ⁢ g ⁢ s 𝑎 𝑟 𝑔 𝑠 args italic_a italic_r italic_g italic_s of input arguments that must satisfy the output condition θ . ϕ formulae-sequence 𝜃 italic-ϕ \theta.\phi italic_θ . italic_ϕ .

Payment channel networks (PCNs) consist of a network of interlinked payment channels . A payment channel is a blockchain-backed financial agreement between two or more parties, which allows them to make verifiable payments to each other without requiring that all of the transactions are published on the blockchain. In the Lightning Network, a channel must have exactly two parties. The party connected to a peer via a payment channel is called the counterparty . This terminology is symmetric and simply indicates whose perspective we are taking at the moment.

A payment channel in LN is established by one of the channel parties escrowing funds in a blockchain transaction that contains an output condition ϕ c ⁢ l ⁢ o ⁢ s ⁢ e subscript italic-ϕ 𝑐 𝑙 𝑜 𝑠 𝑒 \phi_{close} italic_ϕ start_POSTSUBSCRIPT italic_c italic_l italic_o italic_s italic_e end_POSTSUBSCRIPT requiring 2-of-2 signatures to release the funds back to their rightful owner. This is called a funding transaction . As part of the channel establishment process, both parties cooperate to form a signed blockchain transaction, which they broadcast to the Bitcoin network. The channel is considered funded when the funding transaction has been added to the ledger and had some configurable number of blocks mined on top of it.

The two parties then cooperate to form a closing transaction . This is a transaction that includes an input τ c ⁢ l ⁢ o ⁢ s ⁢ e subscript 𝜏 𝑐 𝑙 𝑜 𝑠 𝑒 \tau_{close} italic_τ start_POSTSUBSCRIPT italic_c italic_l italic_o italic_s italic_e end_POSTSUBSCRIPT that contains both parties’ signatures in the arguments; these are both needed to satisfy ϕ c ⁢ l ⁢ o ⁢ s ⁢ e subscript italic-ϕ 𝑐 𝑙 𝑜 𝑠 𝑒 \phi_{close} italic_ϕ start_POSTSUBSCRIPT italic_c italic_l italic_o italic_s italic_e end_POSTSUBSCRIPT . Creating this closing transaction is done as part of channel establishment, but they do not immediately send it to the blockchain network for processing. Instead, both parties store the transaction locally. At any time, either party can submit the closing transaction to the blockchain to release the escrowed funds. The closing transaction can also be updated as discussed .

When the local party wants to make a payment to the counterparty, they send the counterparty a commitment —a signed blockchain transaction that spends the funding transaction output and pays out the channel balance in a potentially different ratio than was initially agreed upon. In the Lightning Network, this message is called \seqsplit COMMITMENT_SIGNED ( Table 1 , row 2). An astute reader will notice that the closing transaction from the paragraph also spent the funding transaction output. That is because this commitment—and any that follow—are replacements for the initial closing transaction. The ability to spend from the funding transaction outputs is precisely what makes it a commitment, because the counterparty can close the channel with said commitment and receive the dictated amount. Both parties can continue sending each other updated commitments for new channel balances—arbitrarily many times—until the channel is closed. Each of the commitments transmitted between the peers is a valid blockchain transaction, which means that as the parties make payments to each other, they are collecting a series of valid transactions.

The protocol necessitates that old commitments be rendered unspendable, but enforcing this is non-trivial. There are a number of proposed solutions to this problem (Gudgeon et al., 2020 ) . The solution used in LN is called replace-by-revocation (RbR). In RbR, every commitment includes a conditional penalty payout that can be triggered by providing a commitment-specific revocation key . After receiving a new commitment, the local party sends the counterparty a revocation key for the commitment. In the Lightning Network, this message is called \seqsplit REVOKE_AND_ACK ( Table 1 , row 3). If either peer submits a transaction to the blockchain that they had previously revoked, then the counterparty has recourse by submitting a new penalty transaction that includes the acquired revocation key. This revocation functionality is built into the ϕ italic-ϕ \phi italic_ϕ conditions of each output in the commitment. The penalty transaction allows the penalizing party to spend both the payout that would normally have gone to them plus the payout that would have gone to the counterparty, thus allowing them to pay the full amount of the channel to themselves. This mechanism is supposed to disincentivize any attempts at duplicity from either peer.

A closing transaction must include a signature from both parties, thus each commitment message includes the signature of the sender. This means a party does not update its view of the channel balance until they receive a new commitment signature from the counterparty. In practice, this means that both parties must send a commitment of the new channel balance and both parties must revoke the balance ( Figure 1 ).

To prevent a race between the two parties to spend the outputs of a blockchain-published commitment, a timeout measured in blocks is enforced as part of the output conditions ϕ italic-ϕ \phi italic_ϕ for the transaction submitter. So while the non-submitting party with a revocation key can spend the commitment output immediately, the transaction-submitting party must wait T 𝑇 T italic_T blocks before they can spend the commitment transaction outputs. This delay is designed to give the non-transaction submitter time to publish a penalty transaction to the blockchain.

A natural limitation of the payment channel construct is that it requires a party to escrow funds for each channel it establishes. Thus the number of diverse parties whom one can pay is limited by the liquidity of each party. A payment channel network addresses this limitation by allowing individual payments to traverse multiple, sequentially linked payment channels. The payment channels thus form a peer-to-peer network where any peer in the network can pay any other peer as long as there is a path in the network graph between them and each channel on that path has enough liquidity to support the payment in question.

A single payment that traverses multiple payment channels consists of independent transactions on each channel. These component transactions must remain collectively atomic—either all of them complete successfully, or none of them do. One mechanism for ensuring this atomicity is the HTLC (Poon and Dryja, 2016 ) .

An HTLC payment is a three-step process. In the first step, the payee U n subscript 𝑈 𝑛 U_{n} italic_U start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT sends the payer U 0 subscript 𝑈 0 U_{0} italic_U start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT an invoice that includes the hash H ⁢ ( p ) 𝐻 𝑝 H(p) italic_H ( italic_p ) of a random number p 𝑝 p italic_p and a payment amount v 𝑣 v italic_v . In the step, each peer starting with U 0 subscript 𝑈 0 U_{0} italic_U start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT , sends a new HTLC request (called \seqsplit UPDATE_ADD_HTLC , Table 1 , row 1) and a commitment for v 𝑣 v italic_v to the peer along the payment path. The commitments, which are Bitcoin transactions signed by each sender, each contain an outputs with condition ϕ italic-ϕ \phi italic_ϕ that can only be satisfied if the submitter can also provide a preimage p 𝑝 p italic_p that hashes to H ⁢ ( p ) 𝐻 𝑝 H(p) italic_H ( italic_p ) . In the final phase, the payment recipient U n subscript 𝑈 𝑛 U_{n} italic_U start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT releases the preimage p 𝑝 p italic_p to its counterparty U n − 1 subscript 𝑈 𝑛 1 U_{n-1} italic_U start_POSTSUBSCRIPT italic_n - 1 end_POSTSUBSCRIPT along the final channel in the payment. Since the final hop’s transaction is complete, peer U n − 1 subscript 𝑈 𝑛 1 U_{n-1} italic_U start_POSTSUBSCRIPT italic_n - 1 end_POSTSUBSCRIPT can pass the preimage to peer U n − 2 subscript 𝑈 𝑛 2 U_{n-2} italic_U start_POSTSUBSCRIPT italic_n - 2 end_POSTSUBSCRIPT , who passes to U n − 3 subscript 𝑈 𝑛 3 U_{n-3} italic_U start_POSTSUBSCRIPT italic_n - 3 end_POSTSUBSCRIPT , etc., until the initial payer U 0 subscript 𝑈 0 U_{0} italic_U start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT has received the preimage.

At this point, the payment is considered functionally complete as all parties along the payment path can redeem their updated channel funds by submitting their latest commitment to the blockchain. The Lightning Network protocol does, in fact, dictate an additional exchange of commitments and revocation on each channel. This exchange exists for two reasons. First, it reduces the complexity of the redeem scripts ϕ italic-ϕ \phi italic_ϕ , thus reducing the transaction size—an important concern for the ever-growing Bitcoin blockchain (Rizzo, 2016 ) . Second, it provides a quicker spending path for unilaterally closed channels, which becomes possible because both parties will have assurance that the other party has received the commitment for the new amount. See the third and fourth messages in Figure 1 .

In this paper, we create a formal model of the popular PCN, the Lightning Network. Specifically, we model Lightning’s payment protocol as defined in the public specification (i.e. Basis of Lightning Technology, BOLTs (BOLT: Basis of Lightning Technology, Lightning Network Specifications ) ).

We opt for model checking because it guarantees a through all possible executions, and its ability to report violating traces. In contrast, fuzzing is useful for efficiently exploring large state spaces, but it notably does not offer any guarantees of finding violations if they exist. Additionally, while fuzzing can find vulnerabilities in implementations, it is not well-suited to English-language specifications.

Theorem provers such as ACL2 (Kaufmann and Moore, 2022 ) , Coq (coq, 2023 ) , and Alloy (Jackson, 2012 ) are also not suitable for our use case. Like fuzzers, theorem provers require an implementation. This implementation must be written in the language of the prover—a significant effort for the modeler. Furthermore, while a theorem prover can verify similar properties as a model checker, and in some cases more properties, this comes at a cost. The ability to model an interactive Turing machine means that some properties cannot be verified without human guidance. On the other hand, model checking can be fully automated.

Model checkers are designed for exploring transition systems such as finite state machines. We opt to use the Spin model checker, a state-of-the-art model checker designed for verifying concurrent programs (Holzmann, 1997 ) . Model checkers like Tamarin (Meier et al., 2013 ) and ProVerif ( Blanchet et al. , 2016 ) are designed to check cryptographic semantics and security protocols. For example, they can model cryptographic games that capture definitions of security such as IND-CPA. The attacks that we found in this work ( Section 5 ) cannot be defended against with cryptography, and thus would not have been found by checking the cryptographic semantics. Spin , on the other hand, is useful for modeling network protocol semantics. As this work focuses on network protocol semantics, we selected Spin , and ultimately, this allows us to model the network communication elements of the LN protocol without the cost of verifying the cryptographic elements. Spin also supports modelling Büchi automata, which are infinite executions of protocols. This is critical for our model since there is no limit to the number of payments the parties can make on a single payment channel, which naturally leads to the existence of infinite executions. For writing properties, Spin supports verification of LTL properties as well as basic assertions and trace assertions (see Section 4 ). These properties are useful for expressing logical requirements of a system that change over time—precisely the case for the Lightning Network payment payment protocol.

In this work, we consider only the channel operation phase of the LN protocol, ignoring channel opening and closing. This is because LN channels spend most of their time in channel operation, and this is the phase in which intermediate- to long-lived channels will send most of their messages. A channel only needs to be opened and closed once, but once open, many payments can be made across it. Our modeling of only part of the protocol is not an artifact of our methodology nor is it a reflection on computational restrictions for model checking the rest of the LN protocol. It simply reflects the degree of manual work required to build a formal model, and is aligned with other works that model subsets of protocols (Arai and Kaneko, 2014 ; Chang and Shmatikov, 2007 ; Nguyen and Leneutre, 2014 ; Phan and Mingard, 2012 ; Modesti et al., 2021 ; Basin et al., 2018 ) .

We restrict our model to payments over a single channel. We consider an adversary with full access to one of the peers on that channel, including their cryptographic keys. The adversary can use the keys to encrypt, decrypt, sign or send arbitrary messages, but cannot break the underlying cryptographic primitives. Any attempt to forge a hash or signature will be detected. While the LN uses encryption for all communication, we do not model this explicitly as we are not considering confidentiality or privacy properties. We consider this attacker model in lieu of the more conservative Dolev-Yao attacker (Dolev and Yao, 1983 ) , because the LN specifies that reliable communication channels must be used (bol, 2023a ) , and the cryptographic elements of the protocol render manipulation by a network adversary ineffective.

We do not consider partitions to the underlying blockchain network that could disrupt the consensus protocol, as that would leave the system vulnerable to much more powerful attacks. However, we do allow that individual LN peers could become partitioned from the Lightning Network and might be prevented from submitting transactions to the blockchain.

To model the Lightning Network, we built an event-driven finite state machine (FSM) of the LN protocol’s payment flow stage. We consider two types of events that initiate transitions: timeouts and receiving messages. In response to an event, the FSM can either send a message, or update any state variables. We present our state machine in Figure 2 . We based our rigorous model on the published LN specification—the BOLTs (BOLT: Basis of Lightning Technology, Lightning Network Specifications ) . There are eleven BOLTs in the spec, but our work focuses on BOLTs two and three, which describe the channel operation behavior for peers that have already established a channel. Textual specifications lack rigor because natural language is ambiguous. Additionally, such specifications are often incomplete. When the textual specification in the BOLTs did not provide enough information or was ambiguous, we consulted the reference implementation ( lnd ( lightningnetwork/lnd: Lightning Network Daemon, ) ) or the protocol developers directly. We also examined execution traces from our model and the Lighting Network implementation. As discussed in Section 5 , the fact that the attacks we found with our model works on the real system implementation demonstrates the usefulness and fidelity of our model. Further details our model are available in Appendix B .

We model two LN peers that are directly connected via a single payment channel. These two peers are modeled as independent processes within Spin . Our model is written in Spin ’s modeling language Promela . We begin executing an LN peer process using the Promela run . The two processes are ensured to start atomically by using Promela ’s atomic keyword. Atomicity at this stage ensures that, at least at the start, both processes are initialized and running. Since we are modeling the payment flow, both peers must already have been running (to setup the channel) and likewise must not have closed the channel yet. The starting state of both processes is FUNDED . Aside from internal bookkeeping data, each peer tracks two state variables: the number of HTLCs opened by the local party and the number opened by the counterparty.

As our goal is to model payments between two peers, we must also model the network communication between those peers. We model network communication via the Promela concept of channels (not to be confused with payment channels). In Promela , processes communicate by writing and reading from shared channels, which are queue-like data structures. Writing to a channel enqueues a message, and reading from a channel dequeues a message. Since we are using these channels to model network communication between distributed processes, we call a write to a channel a “send” event, and a read from a channel a “receive” event. We model seven message types as detailed in Table 1 . These are all the possible messages that can be sent during payment except for a WARNING message, which we combine with the ERROR message as it can be used in all the same situations—the difference being that it carries slightly different information that might be of diagnostic use to the user.

Network communication in the LN is bidirectional. We model bidirectional communication as a pair of channels. Each peer sends to one channel and receives from the other with each peer only sending to the channel that the other peer receives from. Concretely, peer P A subscript 𝑃 𝐴 P_{A} italic_P start_POSTSUBSCRIPT italic_A end_POSTSUBSCRIPT sends to channel C A subscript 𝐶 𝐴 C_{A} italic_C start_POSTSUBSCRIPT italic_A end_POSTSUBSCRIPT and receives from channel C B subscript 𝐶 𝐵 C_{B} italic_C start_POSTSUBSCRIPT italic_B end_POSTSUBSCRIPT , while peer P B subscript 𝑃 𝐵 P_{B} italic_P start_POSTSUBSCRIPT italic_B end_POSTSUBSCRIPT sends to channel C B subscript 𝐶 𝐵 C_{B} italic_C start_POSTSUBSCRIPT italic_B end_POSTSUBSCRIPT and receives from channel C A subscript 𝐶 𝐴 C_{A} italic_C start_POSTSUBSCRIPT italic_A end_POSTSUBSCRIPT . In practice, a pair of LN peers will communicate over a single TCP connection, however, it is convenient for us to model communication as two unidirectional channels. Splitting the channels up as such allows us to avoid modeling unrealistic network contention between the peers, such as one peer not being able to send a message because the other peer has already sent a message—two facts which are causally independent and would not cause issues over a TCP connection.

A Promela channel can be either buffered or unbuffered. A process that sends to an unbuffered channel, a so-called rendezvous channel , will block until another peer receives a message from the channel—logically, it is a queue of length zero. Rendezvous channels are useful for modeling lock-step synchrony, because a process cannot continue its execution until its message is read. However, the LN runs over the public internet where lock-step synchrony is not practical.

We opt to create buffered channels. In Promela , a channel can include a fixed-size buffer, which indicates how many messages it can hold without causing the sender to block (i.e., a queue of length n 𝑛 n italic_n , where n > 0 𝑛 0 n>0 italic_n > 0 ). This models a bounded form of asynchrony, because the sender is able to continue execution before receiving confirmation that the peer has received the message. To this end, we create channels with a buffer size of one. This is sufficient to allow Spin to check a large number of otherwise unreachable states. However, the state space complexity that the model checker explores grows exponentially with the channel size, so for practical constraints we keep the value to one. It is possible that there are states the protocol cannot reach unless there are more messages in flight, however, we believe the likelihood of this is small because the nature of this protocol is to try to maintain some degree of synchronization. A party cannot get too far ahead of its counterparty, because it frequently needs information from the counterparty to proceed.

A single channel cannot support more than 483 483 483 483 in-flight HTLCs. According to BOLT #8, the maximum transaction size in Lightning is 65 65 65 65 kb (bol, 2023b ) . This maximum size is set to be less than the maximum standard Bitcoin transaction size 3 3 3 This is more of a common practice than a hard rule. It is legal for larger transactions to be included in blocks, but many miners will not relay them. .

Each commitment transaction sent between two peers must contain an output θ 𝜃 \theta italic_θ for each HTLC between those two peers. If not, then there could be disagreement the ratio of the payout from the funding transaction. Given the effective maximum transaction size, the sizes of the required arguments of the transaction input τ . a ⁢ r ⁢ g ⁢ s formulae-sequence 𝜏 𝑎 𝑟 𝑔 𝑠 \tau.args italic_τ . italic_a italic_r italic_g italic_s , and the script conditions ϕ italic-ϕ \phi italic_ϕ for each output θ 𝜃 \theta italic_θ , the maximum number of HTLCs concurrently in flight must be less than or equal to 483 483 483 483 . In the protocol code and documentation, this is referred to as \seqsplit max_accepted_htlcs .

In our model, we set \seqsplit max_accepted_htlcs to be ten. However, we do not believe that this constraint negatively impacts the fidelity of our results. In fact, a value of two for \seqsplit max_accepted_htlcs is sufficient to visit all system states for two peers, beyond that, new HTLCs only increment a counter. While an increased counter is technically a new state, these new states do not add any conceptually interesting executions and thus are not worth the resulting state space explosion of using a \seqsplit max_accepted_htlcs of 483. Our value of ten is enough to give confidence that no new interesting executions appear beyond a value of two \seqsplit max_accepted_htlcs , but still small enough to execute quickly.

We define the correctness of the Lightning Network payment protocol in terms of certain properties it must satisfy. Some of these properties, such as deadlock avoidance, are common among network protocols. Others, however, are specific to the LN payment protocol. These properties were either derived directly or were inferred from guarantees made in the BOLTs (BOLT: Basis of Lightning Technology, Lightning Network Specifications ) . In this section, we these properties in depth.

Model checkers can often verify if it is possible for a protocol to deadlock or livelock. Deadlock occurs when a run ends in a state in which no further steps can be taken but is not a legal end state. Livelock , on the other hand, is a type of non-progress cycle where execution can continue indefinitely without reaching a valid end state from which no further steps are possible.

To enable Spin to check for both deadlock and livelock, we must add meta-labels to the Promela model. Meta-labels are simply code-level labels that are prefixed with expected identifiers which confer additional meaning to those states.

The Spin model checker allows us to indicate which states are valid end states by prefixing a label with “end” in the Promela model. Any execution that terminates at an end label is considered accepting . Our only labeled end states are FUNDED and FAIL_CHANNEL . Likewise, Promela allows us to define progress states, which indicate that any infinite execution that includes the progress state infinitely many times is Büchi-accepting. We denote progress states by prefixing a label with “progress.” Our only progress state is FUNDED .

Beyond deadlock and livelock, we define five more properties for our model. In the properties below, we define P 𝑃 P italic_P to be the set of peers. We indicate that a peer is sending message m 𝑚 m italic_m to another peer by writing ! m !m ! italic_m , and receiving message m 𝑚 m italic_m by writing ? ⁢ m ? 𝑚 ?m ? italic_m . If any message is legal, we write *. If a set of messages M 𝑀 M italic_M is accepted except for a particular message m 𝑚 m italic_m , we write M / m 𝑀 𝑚 M/m italic_M / italic_m . We have modeled some of the properties graphically as FSMs where applicable.

Our properties are either modeled as trace assertions which allow us to specify sequences of events that all accepting runs must always match, or linear temporal logic (LTL), which allow us to specify sequences of states that all accepting runs must match. We provide more details and background on types of properties and model checking in general in Appendix A .

A peer p 𝑝 p italic_p should never send a \seqsplit REVOKE_AND_ACK before receiving a \seqsplit COMMITMENT_SIGNED ( Figure 3 ).

We model this property as a trace assertion, which we implement by claiming that no trace of events should exist where a peer sends a \seqsplit REVOKE_AND_ACK and then immediately receives a \seqsplit COMMITMENT_SIGNED .

A peer should always be able to unilaterally close a channel by submitting a commitment transaction to the blockchain. However, if the local party revokes a commitment before receiving a new one, then they lose their ability to close without the possibility of penalty. This is because commitments that the local party revokes can be contested by the counterparty providing the revocation key in τ . a ⁢ r ⁢ g ⁢ s formulae-sequence 𝜏 𝑎 𝑟 𝑔 𝑠 \tau.args italic_τ . italic_a italic_r italic_g italic_s to the spending script ϕ italic-ϕ \phi italic_ϕ . The penalty allows the counterparty to spend all the UTXOs θ 𝜃 \theta italic_θ of the channel, accounting for the entire value of the channel.

Therefore, a peer should avoid putting itself in a position where the only commitment transactions it can submit to the blockchain can be contested (because they have all been revoked). Note that a peer can only do damage to itself by prematurely sending a revocation. A peer could also find itself in a similar position if it loses access to its private key.

A peer must not send or receive an \seqsplit UPDATE_FULFILL_HTLC until it has sent a \seqsplit REVOKE_AND_ACK ( Figure 4 ).

A peer that does not revoke commitments retains the ability to close the channel with an old channel balance—a balance that does not include later payments. This is a safety violation. The counterparty would not be able to contest the commitment submitted to the blockchain because it does not have the revocation key that would have been included in the never-received revocation message.

An HTLC should not be fulfillable if there is more than one channel balance possible for a peer. Such a situation would create ambiguity between the two channel peers how much of the channel balance each of them controls. We model this property as a trace assertion.

If a peer receives a \seqsplit COMMITMENT_SIGNED , its message must be a \seqsplit REVOKE_AND_ACK ( Figure 5 ).

Like 2 , failure to send a revocation can leave the channel in an ambiguous state where one peer has a full channel timeout period to decide which of the two channel states it wants to commit to. A revocation should force the peer to choose a single state.

This property, again a trace assertion, is derived from the BOLTs explicit requirement that “a receiving node [of a \seqsplit COMMITMENT_SIGNED message] MUST respond with a \seqsplit REVOKE_AND_ACK message.” While 2 precludes the possibility of a payment completing successfully without sending the requisite revocation, 3 limits the possibilities further by saying that the immediate message after a \seqsplit COMMITMENT_SIGNED must be a \seqsplit REVOKE_AND_ACK . Though the text does not directly state that a \seqsplit REVOKE_AND_ACK must be the immediate message, we infer this to be the intent in the BOLT as this particular line in the BOLT captures the requirements of a successful payment—where neither peer is at risk of losing funds. The only other message besides \seqsplit REVOKE_AND_ACK that could make semantic sense towards completing a payment securely, would be another \seqsplit COMMITMENT_SIGNED , however, this just delays the problem because the counterparty (having already sent a commitment) cannot legally send another.

A violation of this property would mean that even though the payment was not successful, one peer could still spend the HTLC after an arbitrary delay (chosen during channel creation).

A channel cannot have \seqsplit max_accepted_htlcs open. For a peer with l 𝑙 l italic_l locally opened HTLCs and r 𝑟 r italic_r counterparty-opened HTLCs, we can say using the LTL always (written as □ □ \square □ ).

Going above the \seqsplit max_accepted_htlcs limit is unsupported behavior because it means that commitments and penalty transactions could become too large to be mined ( Section 3.3 ); such an action should result in channel failure according to the BOLTs. However, even having \seqsplit max_accepted_htlcs HTLCs open means that the channel cannot accept more HTLCs, thus blocking all the funds on the channel from use.

An accepting run should always ( □ □ \square □ ) eventually ( ⋄ ⋄ \diamond ⋄ ) terminate with the state s 𝑠 s italic_s in FUNDED or FAIL_CHANNEL , i.e.,

All payments should either complete successfully (end up in FUNDED ) or follow a proper error path (end up in FAIL_CHANNEL ). Typically, an error leads to one or both of parties to force-close the channel, i.e., they close the channel without mutual agreement to do so. Repeatedly passing through FUNDED is allowed as this would constitute a Büchi acceptance cycle.

Our model is implemented in 300 lines of code. We model all seven message types that are used in channel operation (see Table 1 ), as well as all eight states shown in Figure 2 .

All runs were executed on a 2021 Lenovo X1 Carbon ThinkPad with an 11th Gen Intel(R) Core(TM) i7-1165G7 processor clocked at 2.80 2.80 2.80 2.80 GHz and 32 32 32 32 GB RAM. We use Spin version 6.5.2—the latest available at the time of our experiments.

Spin took approximately 0.1 seconds to verify each of the five properties and explored between 478 states (property 4) and 609502 609502 609502 609502 states (property 5). When checking for livelock and deadlock, Spin explored 288139 288139 288139 288139 states, and the highest memory usage in any of the runs peaked at 175 MB. Our verification with Spin did not report any deadlocks or livelocks. However, of the five properties we defined ( Section 4 ), we found that two of them can be violated in accepting runs. Each of these violations can result in an attack, one of the attacks is known in the literature, the other is novel to the best of our knowledge. We the property violations and attack mechanisms in detail below.

Our system correctly captured Mizrahi and Zohar’s congestion attack (Mizrahi and Zohar, 2021 ) . This is the direct implication of the Lightning Network protocol violating 4 , which states that a channel should never have \seqsplit max_accepted_htlcs HTLCs open.

In this attack, a malicious peer sends new \seqsplit UPDATE_ADD_HTLC s until hitting the \seqsplit max_accepted_htlcs HTLC limit. This action is similar to a griefing attack. A griefing attack occurs when an honest user is unable to route a payment over a channel because that channel cannot accept additional HTLCs. This is usually because the full amount of funds on the channel are already allocated to prior in-flight payments. However, in this case, the cause is that the number of HTLCs has hit the mandated hard limit. Griefing has been studied extensively in works (Pérez-Sola et al., 2020 ; Mizrahi and Zohar, 2021 ; Miller et al., 2019 ; Egger et al., 2019 ; Aumayr et al., 2022 ) .

What makes this property ( 4 ) interesting is that peers are explicitly allowed to open \seqsplit max_accepted_htlcs HTLCs (BOLT: Basis of Lightning Technology, Lightning Network Specifications ) . Whatever the limit is set to, the protocol will naturally permit that many HTLCs, so, in fact, it is expected that the model violates this property. Nonetheless, this violation serves as additional confirmation that our model is accurate. For a discussion on mitigating this attack, we refer the reader to Mizrahi and Zohar ( 2021 ) .

Our verification of the Lightning Network payment protocol led us to what we believe is a novel attack against the payment protocol. Spin did not uncover the attack in its entirety, but the full attack is only a slight extension to the property-violating trace. We describe the attack mechanism and implications below.

There are, in fact, an infinite number of accepting runs that violate 3 —a result of the payment protocol being an infinite Büchi automaton. However, the shortest violating trace is straightforward as is shown in Figure 6 in a payment between two LN peers, Alice and Bob. While it is impossible to enumerate all violating traces, we suspect that all such violations a common cause.

The shortest trace in which this violation occurs happens after one peer, Alice, adds a new HTLC and then immediately sends a commitment. The channel counterparty’s message must be a \seqsplit REVOKE_AND_ACK according to the BOLTs, however, the BOLTs also explicitly state that

“From the point of waiting for CHANNEL_READY [a message sent during channel establishment] onward, either node MAY send an \seqsplit ERROR and fail the channel if it does not receive a required response from the other node after a reasonable timeout.”

This is, in fact, an ambiguity in the specification, because a peer cannot always send a \seqsplit REVOKE_AND_ACK if it also always allowed to send an \seqsplit ERROR and fail the channel.

As discussed in Section 2.2 , during a Lightning Network payment, each peer must successively commit to new states—this is the core process in sending payments off-chain. In order to make sure that at all times each peer is able to claim its channel funds on the blockchain, each peer must always maintain at least one valid \seqsplit COMMITMENT_SIGNED message. The implication of this is that at some points during protocol execution, one or both peers may have two or more legal commitments that they could redeem on the blockchain.

Having two legal channel states can lead to ambiguity in how much the channel should payout to each party, if the payment protocol does not reach its prescribed conclusion. In most cases and in successful payments, this is not a problem, because after receiving a new commitment, a peer revokes its commitment with a \seqsplit REVOKE_AND_ACK . The revocation thus limits the peer again to only a single commitment transaction that it can safely (i.e., without fear of penalty) submit to the blockchain.

The violation of 3 showed that the protocol can terminate in an undesirable state. This observation led us to consider what would happen if there were a network partition after Alice sent message \Circled [fill color=black,inner color=white]b in Figure 6 . In general, a peer cannot be certain that its counterparty received the commitment until it receives an acknowledgment in the form of a \seqsplit REVOKE_AND_ACK message. The implications of this are critical, which becomes clear when we consider how this could play out in a point-of-sale situation.

Consider the scenario where Alice is at a brick-and-mortar store trying to purchase product 𝒫 𝒫 \mathcal{P} caligraphic_P via transaction 𝒯 ⁢ 𝒳 𝒯 𝒳 \mathcal{TX} caligraphic_T caligraphic_X from Bob. Prior to the payment, Alice’s most up-to-date commitment C ⁢ 2 B 𝐶 subscript 2 𝐵 C2_{B} italic_C 2 start_POSTSUBSCRIPT italic_B end_POSTSUBSCRIPT and Bob’s most up-to-date commitment C ⁢ 2 A 𝐶 subscript 2 𝐴 C2_{A} italic_C 2 start_POSTSUBSCRIPT italic_A end_POSTSUBSCRIPT agree on the payout amounts available to both Alice and Bob—these are encoded in the commitments’ respective UTXOs. Both C ⁢ 2 B 𝐶 subscript 2 𝐵 C2_{B} italic_C 2 start_POSTSUBSCRIPT italic_B end_POSTSUBSCRIPT and C ⁢ 2 A 𝐶 subscript 2 𝐴 C2_{A} italic_C 2 start_POSTSUBSCRIPT italic_A end_POSTSUBSCRIPT can accept the same UTXO input τ 𝜏 \tau italic_τ , if they are force-closing a channel. In this case, τ 𝜏 \tau italic_τ is equal to the output of the channel funding transaction ( t ⁢ x f ⁢ u ⁢ n ⁢ d . θ formulae-sequence 𝑡 subscript 𝑥 𝑓 𝑢 𝑛 𝑑 𝜃 tx_{fund}.\theta italic_t italic_x start_POSTSUBSCRIPT italic_f italic_u italic_n italic_d end_POS...