KIT | KIT-Bibliothek | Impressum | Datenschutz

Verifying Payment Channels 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)

Abstract (englisch):

A payment channel protocol does not only have to provide the payment functionality, it also has to fulfill security guarantees such as ensuring that an honest party receives their correct balance. For complexity reasons, it is typically difficult to assess the security of such a protocol or to find counterexamples in insecure protocols. In this poster, we present an approach to specify functional as well as security properties for a payment channel protocol in TLA+ and show that a Lightning Network-style protocol fulfills the required properties. In case a counterexample is found, we provide protocol developers with a graphical and intuitive output. We present the challenges we faced and our approach to meeting these challenges.

Postprint §
DOI: 10.5445/IR/1000146770
Veröffentlicht am 31.05.2022
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 05.05.2022
Sprache Englisch
Identifikator ISBN: 978-1-6654-9538-7
KITopen-ID: 1000146770
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
Erschienen in IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2nd –5th May 2022, Virtual Conference
Veranstaltung IEEE International Conference on Blockchain and Cryptocurrency (ICBC 2022), Online, 02.05.2022 – 05.05.2022
Verlag Institute of Electrical and Electronics Engineers (IEEE)
Seiten 1-3
Nachgewiesen in Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page