Security of the Lightning Network: Model Checking a Stepwise Refinement with TLA+

Payment channel networks such as the Lightning Network are an approach to improve the scalability of blockchain-based cryptocurrencies. The complexity of Lightning, the Lightning Network's protocol, 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. Model checking provides a fully automated verification of the security property, however, the state space of the protocol's specification is so large that model checking is unfeasible. We make model checking of Lightning possible using two refinement steps that we verify using proofs. In a first step, we abstract the model of time and in a second step we use compositional reasoning to separately model check a single payment channel and multi-hop payments. These refinements reduce the state space sufficiently to allow for model checking Lightning with small finite models. Our results indicate that the current specification of Lightning is secure.