Model Checking the Security of the Lightning Network

TL;DR

This work formalizes the Lightning Network protocol in TLA+ and defines a security property ensuring honest users eventually obtain their correct balances. To overcome the enormous state space, the authors perform a two-stage refinement: (i) abstract time using ideas from timed automata, and (ii) separate single-hop from multi-hop protocol analyses, enabling model checking for models with up to $4$ hops and $2$ concurrent payments. They verify the refinements with proofs and TLC simulations, gaining confidence that the current Lightning specification is secure within the modeled scope. The study also discusses limitations (e.g., restricted adversary, omitted features such as fees and routing) and outlines avenues for future work, including complete formal proofs and linking the spec to real implementations. Overall, the approach demonstrates a practical pathway to formally verify complex payment-channel protocols and can inform safer future designs.

Abstract

Payment channel networks are an approach to improve the scalability of blockchain-based cryptocurrencies. The Lightning Network is a payment channel network built for Bitcoin that is already used in practice. Because the Lightning Network is used for transfer of financial value, its security in the presence of adversarial participants should be verified. The Lightning protocol's complexity makes it hard to assess whether the protocol is secure. To enable computer-aided security verification of Lightning, we formalize the protocol in TLA+ and formally specify the security property that honest users are guaranteed to retrieve their correct balance. While model checking provides a fully automated verification of the security property, the state space of the protocol's specification is so large that model checking becomes unfeasible. We make model checking the Lightning Network possible using two refinement steps that we verify using proofs. In a first step, we prove that the model of time used in the protocol can be abstracted using ideas from the research of timed automata. In a second step, we prove that it suffices to model check the protocol for single payment channels and the protocol for multi-hop payments separately. These refinements reduce the state space sufficiently to allow for model checking Lightning with models with payments over up to four hops and two concurrent payments. These results indicate that the current specification of Lightning is secure.

Figures (9)

• Figure 1: Formal definition of the security property as an idealized payment network. The module IdealPaymentNetwork specifies that each user behaves as specified by the module IdealUser (see \ref{['fig-tla-idealized-payment-network-user']}) and that the users' views on which payments have been processed are consistent as specified in the module IdealPayments (see \ref{['fig-tla-idealized-payment-network-payments']}).
• Figure 2: Part of the security property that defines how a user's variables are allowed to change. The action $\mathrm{Deposit}$ specifies how a user deposits funds into the channel. $\mathrm{Pay}$ specifies that payments are either processed or aborted and the channel balance is updated accordingly. $\mathrm{Withdraw}$ specifies that the channel balance is withdrawn to the blockchain. The fairness condition ensures that a user will withdraw if the user's channel balance is positive.
• Figure 3: Part of the security property that defines that the sender of a payment may only see the payment as processed if the receiver of the payment sees the payment as processed.
• Figure 4: Structure of the stepwise refinement to show that the Lightning protocol $(I)$ refines the security property $(V)$. Specification $(I)$ is presented in \ref{['sec-lightning']}, specification $(V)$ in \ref{['sec-security-property']}, and the intermediate specifications in \ref{['sec-proof-sketch']}. The correctness of each step is either proven or model checked. Additionally, we check the refinement steps as well as the whole stepwise refinement using simulation, i.e., non-exhaustive model checking (see \ref{['sec-model-checking-results']}).
• Figure 5: Zones in which bisimilar states are grouped in a scenario a) with two HTLCs with timelocks $t_1$ and $t_2$ and b) with two HTLCs and an unpublished transaction $tx$ with an output that has a relative timelock $r$.

Theorems & Definitions (29)

• Definition 1: informal security
• Definition 2: Bisimilarity
• Definition 3: $\hat{T}_d^x$
• Definition 4: $\hat{\mathcal{T}}^{x}_d$
• Definition 5: $N_{\hat{S}}$
• Definition 6: $N_{S}$
• Definition 7: $ETP^x(s)$
• Definition 8: $AdvanceTime_{\hat{S}}$
• Theorem 9
• Lemma 10