KIT | KIT-Bibliothek | Impressum | Datenschutz

Towards a Formal Verification of the Lightning Network with TLA+

Grundmann, Matthias ORCID iD icon 1; Hartenstein, Hannes 1
1 Institut für Informationssicherheit und Verlässlichkeit (KASTEL), Karlsruher Institut für Technologie (KIT)


Payment channel networks are an approach to improve the scalability of blockchain-based cryptocurrencies. Because payment channel networks are used for transfer of financial value, their security in the presence of adversarial participants should be verified formally. We formalize the protocol of the Lightning Network, a payment channel network built for Bitcoin, and show that the protocol fulfills the expected security properties. As the state space of a specification consisting of multiple participants is too large for model checking, we formalize intermediate specifications and use a chain of refinements to validate the security properties where each refinement is justified either by model checking or by a pen-and-paper proof.

Volltext §
DOI: 10.5445/IR/1000160211
Veröffentlicht am 06.07.2023
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 2023
Sprache Englisch
Identifikator KITopen-ID: 1000160211
HGF-Programm 46.23.01 (POF IV, LK 01) Methods for Engineering Secure Systems
Weitere HGF-Programme 46.23.03 (POF IV, LK 01) Engineering Security for Mobility Systems
Umfang 11 S.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page