A Formally Verified Lightning Network
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929751535386624 |
|---|---|
| author | Fabiański, Grzegorz Stefański, Rafał Litos, Orfeas Stefanos Thyfronitis |
| author_facet | Fabiański, Grzegorz Stefański, Rafał Litos, Orfeas Stefanos Thyfronitis |
| contents | In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, we provide a machine checkable proof that they are upheld under every scenario, all in an integrated fashion. We build our system using the Why3 platform. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_07200 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formally Verified Lightning Network Fabiański, Grzegorz Stefański, Rafał Litos, Orfeas Stefanos Thyfronitis Cryptography and Security Logic in Computer Science In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, we provide a machine checkable proof that they are upheld under every scenario, all in an integrated fashion. We build our system using the Why3 platform. |
| title | A Formally Verified Lightning Network |
| topic | Cryptography and Security Logic in Computer Science |
| url | https://arxiv.org/abs/2503.07200 |