Pith. sign in

REVIEW 4 major objections 5 minor 89 references

Model Checking the Security of the Lightning Network

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper argues that a TLA+ model of Lightning, checked up to four hops and two concurrent payments, satisfies the security property that honest users retrieve their correct balance.

desk verdict A serious TLA+ formalization and a feasible bounded verification pipeline, but the multi-channel security claim leans on a manual proof that deserves referee scrutiny. read the letter →

arxiv 2505.15568 v1 pith:7VT4SWNN submitted 2025-05-21 cs.CR cs.LO

Matthias Grundmann , Hannes Hartenstein This is my paper · ORCID
classification cs.CRcs.LO MSC 68Q6068M12
keywords LightningNetworkpaymentchannelsformalverificationmodelcheckingTLA+refinementmappingHTLCrevocationmechanism
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to answer a concrete question: can an honest user of the Lightning Network be sure of getting their correct balance out of a payment channel, even when other participants are malicious? To make this answerable by machine, the authors write the protocol in TLA+, specify an 'ideal payment network' that captures the security property, and then connect the two by a chain of five specifications linked by refinement mappings. The chain makes model checking feasible: a time-abstraction step groups equivalent clock states into zones, and a channel-abstraction step lets single-channel and multi-hop behavior be checked separately. With these reductions, the explicit-state model checker fully explores models with payments over up to four hops and two concurrent payments, and simulation covers larger scenarios and the manual proof steps. The paper's conclusion is that the current Lightning specification is secure, meaning that it implements the idealized payment network, within the modeled adversary powers and checked bounds.

What carries the argument

Two linked abstractions carry the argument. The first is a generalized time-skip theorem for explicit real-time specifications: if time is modeled by clocks that only matter through the order in which timelocks become reachable, an original specification implements an optimized one where time jumps directly to the next 'newly possible' point, so states that differ only by clock values inside the same zone are not distinguished. The second is an idealized-channel abstraction: each payment channel is replaced by a specification that updates HTLC states in single idealized steps, and a proof using reordering rules adapted from distributed-systems verification shows that interleaved protocol steps can be rearranged and collapsed into those idealized steps. Around these sit the security property itself, a TLA+ module defining that honest users can deposit, pay, and finally withdraw with a balance that only changes consistently with processed payments, and a refinement mapping that identifies the values in the protocol state with the balances in that ideal network.

What would settle it

A concrete disproof would be a reachable state in any fully explored model in which an honest user's final blockchain balance is less than their correct channel balance; the paper reports no such state. On the live protocol, an attack falling inside the modeled adversary class, such as a malicious channel peer who, without message forging or collusion, causes an honest monitoring user to end with less than their balance, would also falsify the transfer of the result.

Watch

Extended reading notes

Core claim

The paper's central claim is that the TLA+ formalization of the Lightning Network protocol is a refinement of a formally specified 'ideal payment network,' and therefore satisfies the security property that every honest user is finally able to retrieve at least their correct balance on the blockchain. The argument proceeds through a chain of five specifications (I through V) connected by refinement mappings. Two reductions make state-space exploration feasible: first, time, modeled as blockchain height with absolute and relative timelocks, is abstracted to zone representatives by a generalized time-skip theorem adapted from timed-automata bisimulation; second, the multi-channel protocol is shown to refine a specification of idealized channels, so that single-channel protocol correctness and multi-hop payment correctness can be model checked separately. The explicit-state model checker fully explores models with payments over up to four hops and two concurrent payments, and simulation is used for larger models and to check the manual proof steps. On this basis the paper concludes that the current Lightning specification is secure for the modeled adversarial capabilities and the checked bounds.

Load-bearing premise

The conclusion stands or falls with whether the TLA+ model faithfully captures the real Lightning protocol, including the paper's restrictions that adversarial users cannot coordinate or send arbitrary messages and that transactions are confirmed without delay or reorganization.

Editorial extensions

If this is right

  • Under the modeled assumptions, an honest user can rely on the channel protocol alone to retrieve at least their correct balance on-chain, even if the counterparty is malicious and tries to publish an outdated commitment transaction.
  • The security property gives an operational rule: a seller may treat an incoming payment as processed once the corresponding incoming HTLC is fulfilled, without needing to wait for the fulfilled HTLC to be removed from the channel.
  • The model can serve as a conformance reference: execution traces from Lightning implementations can be checked against the TLA+ specification.
  • Proposed protocol modifications can be tested quickly; the paper demonstrates that model checking detects a flawed simplification that would remove HTLC second-stage transactions.
  • The same refinement machinery, especially the time-skip abstraction, can be applied to analyze dual-funded channels and other timed payment protocols.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next step would be to machine-check the three manual refinement proofs, since those are the only steps not verified by exhaustive model checking; until then the security claim rests partly on hand proofs.
  • If the result transfers to practice, it suggests that, within the modeled environment, external watchtowers are not needed for balance correctness, only the honest user's own protocol-following behavior and blockchain monitoring.
  • The 'ideal payment network' formulation could be reused as a security definition for other payment channel networks, because it is stated purely in terms of user balances, payment views, and honest withdrawal.
  • Relaxing the excluded adversary abilities, such as allowing adversarial users to exchange information or send arbitrary messages, would be the most direct stress test of the result; the paper leaves this for future work.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper presents a TLA+ formalization of the Lightning Network protocol, a TLA+ specification of a security property (honest users finally retrieve at least their correct balance), and a stepwise-refinement argument intended to show that the protocol specification implements the security specification. The verification combines manual proofs for time abstraction (refinements 1 and 3) and for the channel-to-idealized-channel abstraction (refinement 2), with model checking of two refinement steps: the single-channel refinement 2a and the final idealized-channel-to-security-property refinement 4. Model checking is performed with TLC on finite instances with up to four users, four hops, and two concurrent payments; larger instances and the manual proofs are additionally checked by simulation. The paper concludes that the modeled Lightning specification is an implementation of an idealized payment network and therefore fulfills the modeled security property.

Significance. If the claims are accepted, the paper makes a valuable contribution: it provides a substantial, public TLA+ formalization of Lightning that follows the official BOLT specification closely, defines a user-level security property independently of the protocol, and demonstrates a refinement architecture that makes finite model checking feasible. The explicit encoding of revocation, HTLC state transitions, on-chain punishment, and time bounds is a useful artifact for the community, and the reported automated discovery of subtle flaws in a prior formalization illustrates the value of the approach. The paper is also appropriately transparent in several places, stating that the manual refinement proofs are not machine checked and that the adversary model and blockchain model are simplified. However, the central claim as phrased in Section VI-C and the abstract goes beyond what is actually verified, because the decisive multi-channel transfer rests on a manual environment-mocking proof and because model checking covers only small finite instances.

major comments (4)
  1. [Section VI-C and Section VII] The sentence 'we conclude from the refinement steps described above that specification I implements specification V' is stronger than the verification performed. Refinements 1, 2, and 3 are manual proofs, and only refinements 2a and 4 are model checked, on finite instances with up to four users and two concurrent payments, as reported in Tables I and II. The finite bounds matter: Section VIII explicitly acknowledges that attacks requiring more than four users would not be discovered. The conclusion should be scoped, for example as 'the modeled instances and the stated assumptions give evidence that the modeled specification is secure', or the unqualified implication should be replaced by a clearly stated conditional theorem listing all assumptions and all manually proved steps.
  2. [Section VI-B and Section F2] The multi-channel security conclusion depends on the manual proof that the environment-mocking module in specification IIa captures all possible steps that other channels can perform. Model checking of refinement 2a validates the mocked single-channel system only; its transfer to the full multi-channel network relies entirely on the soundness of that unverified proof and on the adapted IronFleet reordering rules for shared variables. This is load-bearing because a real user participating in two channels can observe and react to intermediate HTLC states in one channel while updating another, and the paper does not machine-check that the mocking module covers those interleavings. Please either provide a machine-checked proof of the mocking lemma, or explicitly mark the multi-channel refinement 2 as a manually verified step and correspondingly weaken the headline claim.
  3. [Section IV, Section VI-C, and Section VIII] The security statement is conditional on several protocol simplifications that are security-relevant: the adversary cannot send messages with arbitrary content, adversarial users cannot exchange information, transactions are assumed to be included in the next block without reorganizations, channels are single-funded, and fees are omitted. These assumptions are listed in Sections IV and VIII, but the paper's central conclusion in Section VI-C and the abstract does not carry them. Since an attacker in the real Lightning network can plausibly control multiple nodes and exploit transaction delays, the unqualified phrase 'the current specification of Lightning is secure' is not warranted. The paper should state the verified theorem explicitly with each modeling assumption as a precondition, so that the gap between the verified model and the real protocol is visible to the reader.
  4. [Section VII] The model-checking results are finite and limited to selected scenarios, and the paper acknowledges that larger scenarios are checked only by simulation. This is a reasonable engineering choice, but it means the paper does not establish security for the unbounded Lightning protocol. In particular, the model C5 with two concurrent payments takes about a month and is near the limit of the method; no argument is given that the set of checked models is representative for all attacks on the real protocol. The paper should either justify why the checked configurations cover the security-relevant behaviors or explicitly describe the result as evidence rather than a proof of security for the general protocol.
minor comments (5)
  1. [Section I] The sentence 'We describe Lightning in more detail and give an introduction to TLA + in Section II' contains a duplicated 'in'; please correct this typo.
  2. [Abstract and Section IX] The abstract says 'results indicate that the current specification of Lightning is secure', while Section IX says the formalization 'can serve as a starting point for future work towards a formally verified reference implementation'. These two statements are in tension; please align the wording with the actual scope of the verification.
  3. [Section IV and Section B2] The paper states that the TLA+ formalization is available on GitHub but does not provide a version or commit hash. For reproducibility of the reported model-checking results, please cite a specific release or commit and describe the exact TLA+ tools and parameters used.
  4. [Section VII] The simulation-based verification is described only qualitatively. Please report the number of simulation runs, the seed and configuration, and which larger scenarios were covered, so that the evidence from simulation can be assessed.
  5. [Tables I and II] The model names C1 to C5 and the entries in Table II are described in the text, but a direct mapping between each table row and the corresponding TLA+ model instance would make the artifact easier to reproduce.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the ideal security property is defined independently of the protocol model, and the refinement chain is a genuine verification argument.

full rationale

The central claim is that the TLA+ protocol specification (I) implements an independently specified idealized secure payment network (V). Specification V is not derived from the Lightning protocol; it is defined in Figures 1-3 as a minimal ideal system with Deposit, Pay, and Withdraw actions and a consistency condition between sender and receiver views. The protocol specification I follows the official BOLT specification and models the actual message exchange, revocation, commitment transactions, and on-chain closing. The intermediate specifications are verified either by explicit-state model checking (refinements 2a and 4) or by structured proofs (refinements 1, 2, 3). The fact that refinement mapping 4 is 'straightforward because all variables of specification V are also variables of specification IV' is a standard refinement setup: sharing external variables does not by itself make every IV behavior a V behavior; TLC still checks that each IV step is a legal V step. The unverified manual proofs and the environment-mocking proof are proof obligations whose failure would weaken the result, but they are not circular inputs. There are no relevant self-citations and no fitted parameters are renamed as predictions. The acknowledged limitations (adversary cannot send arbitrary messages, no fee modeling, bounded small models) are scope restrictions and correctness risks, not circularity.

Assumptions & free parameters 3 free parameters · 8 assumptions · 0 invented entities

The central claim rests on the faithfulness of the TLA+ model to the real Lightning protocol and on the correctness of two refinement proofs. The ledger lists the protocol simplifications and adversary restrictions that the security result inherits. No numerical fits to data are used, but the model checking instances introduce finite bounds, and the manual proofs introduce an additional unverified component.

free parameters (3)
  • Grace period constant G = 3 (default)
    Number of blocks after an HTLC timeout during which the HTLC can still be fulfilled; suggested by BOLT, chosen by hand, not fitted to data. It affects the state space and is part of the protocol model.
  • TO_SELF_DELAY = constant, value not fixed in text
    Channel parameter for how long a counterparty's output must be locked; a modeling constant, not fitted to data.
  • Finite model instance bounds = per model (Tables I and II)
    TLC requires finite ranges for balances, amounts, timelocks, and payment counts. The security property is demonstrated only for these finite instances, not for arbitrary values or unbounded numbers of payments.
assumptions (8)
  • domain assumption Perfect cryptography: the adversary cannot forge signatures, invert hash functions, or guess preimages and payment secrets; the hash function is modeled as identity with names distinguishing hashes from preimages.
    Standard symbolic cryptography assumption, stated in Section IV and applied throughout the formalization in Section B3.
  • domain assumption Transactions published on the blockchain are included in the next block; there are no blockchain reorganizations and no transaction inclusion delays.
    Stated in Section IV ('each transaction to be published is included in the next block being created'); Section VIII-B lists reorgs and delays as future work.
  • domain assumption Messages between channel parties are delivered reliably and in order, but can be arbitrarily delayed; global invoice messages can be delivered in arbitrary order.
    Stated in Section IV: messages are delivered reliably and in order but can be arbitrarily delayed.
  • ad hoc to paper The adversary may omit sending messages or publishing transactions and may publish certain transactions other than specified, but may not send messages with arbitrary content, and adversarial users do not exchange information.
    Section IV and Section VIII-B: these restrictions are made to keep the state space manageable; they weaken the adversary model compared to the real protocol and are acknowledged limitations.
  • domain assumption Only single-funded channels are modeled; fees, key rotation, onion routing, route finding, channel reopening, new parties joining, and dual funding are out of scope.
    Sections II-A and VIII-B: features left out because they are considered not required for the modeled security property.
  • ad hoc to paper Liveness assumptions for dishonest users: dishonest users participate in channel opening, publish spendable outputs after the counterparty terminates, and in one specific situation time out an HTLC output on-chain.
    Section B17: these exceptions simplify termination and the definition of idealized channels; the authors argue they do not practically strengthen the adversary, but they are extra assumptions beyond the protocol spec.
  • domain assumption The small finite models checked (up to 4 hops, 2 concurrent payments, 3 to 4 users) are representative of all relevant protocol behaviors.
    Section VII: the authors state they 'only check a small selection of models that we deem representative'; Section VIII-A notes attacks with more than four users would not be discovered.
  • ad hoc to paper The manual refinement proofs for abstractions 1, 2, and 3 are correct.
    Section VI: only refinements 2a and 4 are model checked; the proofs are structured but not machine checked with TLAPS, and the larger steps are only simulated.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Model Checking the Security of the Lightning Network." pith.science (2026). https://pith.science/paper/7VT4SWNN

@misc{pith2026250515568,
  author       = {Pith},
  title        = {Pith review of: Model Checking the Security of the Lightning Network},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7VT4SWNN}},
  note         = {Machine review of arXiv:2505.15568}
}
read the original 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

Figures reproduced from arXiv: 2505.15568 by the authors.

Figure 1
Figure 1. Formal definition of the security property as an idealized payment [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 3
Figure 3. Part of the security property that defines that the sender of a payment [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 2
Figure 2. Part of the security property that defines how a user’s variables are [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: Structure of the stepwise refinement to show that the Lightning protocol [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: Zones in which bisimilar states are grouped in a scenario a) with two [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: Overview of the IronFleet methodology. The upper half shows the [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: In the protocol specification pII q, steps for opening and updating two channels might be interleaved (left column). The refinement mapping 2 from specification pII q to pIII q abstracts such interleaved steps to idealized steps (right column). Thereby, the specificati…
Figure 8
Figure 8. Figure 8: Flow chart of HTLC states. The actions with the prefix H! are actions [PITH_FULL_IMAGE:figures/full_fig_p021_8.png]
Figure 9
Figure 9. Figure 9: Derivation of keys in Lightning. Each box shows a key or piece [PITH_FULL_IMAGE:figures/full_fig_p022_9.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

89 extracted references · 77 canonical work pages

  1. [1]

    The Bitcoin Lightning Network: Scalable Off- Chain Instant Payments,

    J. Poon and T. Dryja, “The Bitcoin Lightning Network: Scalable Off- Chain Instant Payments,” Tech. Rep., 2016

    2016

  2. [2]

    Bitcoin: A Peer-to-Peer Electronic Cash System,

    S. Nakamoto, “Bitcoin: A Peer-to-Peer Electronic Cash System,” Tech. Rep., 2008

    2008

  3. [3]

    Year-over-Year Data Shows Rising Lightning Network Adoption|CoinGate,

    V . Barbaravi ˇcius, “Year-over-Year Data Shows Rising Lightning Network Adoption|CoinGate,” Aug. 2024. [Online]. Available: https://coingate.com/blog/post/lightning-network-year-over-year-data

    2024

  4. [4]

    (2024) BOLT: Basis of Lightning Technology (Lightning Network In-Progress Specifications)

    Various. (2024) BOLT: Basis of Lightning Technology (Lightning Network In-Progress Specifications). [Online]. Available: https://github. com/lightning/bolts

    2024

  5. [5]

    The temporal logic of actions,

    L. Lamport, “The temporal logic of actions,”ACM Transactions on Programming Languages and Systems, vol. 16, no. 3, pp. 872–923, May 1994

    1994

  6. [6]

    USA: Addison-Wesley Longman Publishing Co., Inc., 2002

    ——,Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. USA: Addison-Wesley Longman Publishing Co., Inc., 2002

    2002

  7. [7]

    (2025) TLA+ Toolbox

    Various. (2025) TLA+ Toolbox. [Online]. Available: https://github.com/ tlaplus/tlaplus

    2025

  8. [8]

    (2025) Apalache — The Symbolic Model Checker for TLA+

    ——. (2025) Apalache — The Symbolic Model Checker for TLA+. [Online]. Available: https://apalache-mc.org/

    2025

Show all 89 references
  1. [9]

    (2025) TLA+ Proof System

    Microsoft Research – Inria Joint Centre. (2025) TLA+ Proof System. [Online]. Available: https://proofs.tlapl.us/doc/web/content/Home.html

    2025

  2. [10]

    Automata for modeling real-time systems,

    R. Alur and D. Dill, “Automata for modeling real-time systems,” in Automata, Languages and Programming, M. S. Paterson, Ed. Berlin, Heidelberg: Springer, 1990, pp. 322–335

    1990

  3. [11]

    Formal specification and verification,

    S. Merz, “Formal specification and verification,” inConcurrency: the Works of Leslie Lamport. New York, NY , USA: Association for Computing Machinery, Oct. 2019, pp. 103–129. [Online]. Available: https://doi.org/10.1145/3335772.3335780

    2019

  4. [12]

    A Systematic Liter- ature Review on a Decade of Industrial TLA+ Practice,

    R. B ¨ogli, L. Lerena, C. Tsigkanos, and T. Kehrer, “A Systematic Liter- ature Review on a Decade of Industrial TLA+ Practice,” inIntegrated Formal Methods, N. Kosmatov and L. Kov ´acs, Eds. Cham: Springer Nature Switzerland, 2025, pp. 24–34

    2025

  5. [13]

    The existence of refinement mappings,

    M. Abadi and L. Lamport, “The existence of refinement mappings,” Theoretical Computer Science, vol. 82, no. 2, pp. 253–284, May 1991

    1991

  6. [14]

    Kronos: A model-checking tool for real-time systems,

    M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine, “Kronos: A model-checking tool for real-time systems,” inFormal Techniques in Real-Time and Fault-Tolerant Systems, A. P. Ravn and H. Rischel, Eds. Berlin, Heidelberg: Springer, 1998, pp. 298–302

    1998

  7. [15]

    Uppaal in a nutshell,

    K. G. Larsen, P. Pettersson, and W. Yi, “Uppaal in a nutshell,”Inter- national Journal on Software Tools for Technology Transfer, vol. 1, no. 1-2, pp. 134–152, Dec. 1997

    1997

  8. [16]

    Real-Time Model Checking Is Really Simple,

    L. Lamport, “Real-Time Model Checking Is Really Simple,” inCorrect Hardware Design and Verification Methods, ser. Lecture Notes in Computer Science, D. Borrione and W. Paul, Eds. Berlin, Heidelberg: Springer, 2005, pp. 162–175

    2005

  9. [17]

    Modeling Bitcoin Contracts by Timed Automata,

    M. Andrychowicz, S. Dziembowski, D. Malinowski, and Ł. Mazurek, “Modeling Bitcoin Contracts by Timed Automata,” inFormal Modeling and Analysis of Timed Systems, A. Legay and M. Bozga, Eds. Cham: Springer International Publishing, 2014, pp. 7–22

    2014

  10. [18]

    Modelling Bitcoin in Agda,

    A. Setzer, “Modelling Bitcoin in Agda,” Apr. 2018, arXiv:1804.06398 [cs]

    2018 arXiv

  11. [19]

    A Brief Overview of Agda – A Functional Language with Dependent Types,

    A. Bove, P. Dybjer, and U. Norell, “A Brief Overview of Agda – A Functional Language with Dependent Types,” inTheorem Proving in Higher Order Logics, S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, Eds. Berlin, Heidelberg: Springer, 2009, pp. 73–78

    2009

  12. [20]

    A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract,

    C. Boyd, K. Gjøsteen, and S. Wu, “A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract,” inDROPS- IDN/v2/document/10.4230/OASIcs.FMBC.2020.5. Schloss Dagstuhl – Leibniz-Zentrum f ¨ur Informatik, 2020

    2020 doi

  13. [21]

    Secrecy and Authenticity Properties of the Lightning Network Protocol,

    H. H ¨uttel and V . Starove ˇski, “Secrecy and Authenticity Properties of the Lightning Network Protocol,” Feb. 2020, pp. 119–130. [Online]. Available: https://www.scitepress.org/Link.aspx?doi=10.5220/ 0008974801190130

    2020

  14. [22]

    Key Agreement in the Lightning Network Protocol,

    ——, “Key Agreement in the Lightning Network Protocol,” inInforma- tion Systems Security and Privacy, ser. Communications in Computer and Information Science, S. Furnell, P. Mori, E. Weippl, and O. Camp, Eds. Cham: Springer International Publishing, 2022, pp. 139–155

    2022

  15. [23]

    Towards a Game- Theoretic Security Analysis of Off-Chain Protocols,

    S. Rain, G. Avarikioti, L. Kov ´acs, and M. Maffei, “Towards a Game- Theoretic Security Analysis of Off-Chain Protocols,” in2023 IEEE 36th Computer Security Foundations Symposium (CSF), Jul. 2023, pp. 107– 122, iSSN: 2374-8303

    2023

  16. [24]

    CheckMate: Automated Game-Theoretic Security Reasoning,

    L. S. Brugger, L. Kov ´acs, A. P. Komel, S. Rain, and M. Rawson, “CheckMate: Automated Game-Theoretic Security Reasoning,” Sep. 2023, number: 10853 Publisher: EasyChair. [Online]. Available: https://easychair.org/publications/preprint/2G4t

    2023

  17. [25]

    A Composable Security Treatment of the Lightning Network,

    A. Kiayias and O. S. Thyfronitis Litos, “A Composable Security Treatment of the Lightning Network,” in2020 IEEE 33rd Computer Security Foundations Symposium (CSF), Jun. 2020, pp. 334–349, iSSN: 2374-8303

    2020

  18. [26]

    Universally composable security: a new paradigm for cryptographic protocols,

    R. Canetti, “Universally composable security: a new paradigm for cryptographic protocols,” inProceedings 42nd IEEE Symposium on Foundations of Computer Science, Oct. 2001, pp. 136–145, iSSN: 1552- 5244

    2001

  19. [27]

    Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network,

    B. Weintraub, S. P. Kumble, C. Nita-Rotaru, and S. Roos, “Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network,” inProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, ser. CCS ’24. New York, NY , USA:...

    2024

  20. [28]

    A Formally Verified Lightning Network,

    G. Fabia ´nski, R. Stefa ´nski, and O. S. T. Litos, “A Formally Verified Lightning Network,” Apr. 2025. [Online]. Available: https: //fc25.ifca.ai/preproceedings/63.pdf

    2025

  21. [29]

    A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract,

    C. Boyd, K. Gjøsteen, and S. Wu, “A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract,” 2020

    2020

  22. [30]

    Modeling Urgency in Timed Sys- tems,

    S. Bornot, J. Sifakis, and S. Tripakis, “Modeling Urgency in Timed Sys- tems,” inCompositionality: The Significant Difference, W.-P. de Roever, H. Langmaack, and A. Pnueli, Eds. Berlin, Heidelberg: Springer, 1998, pp. 103–129

    1998

  23. [31]

    Baier and J.-P

    C. Baier and J.-P. Katoen,Principles of model checking. MIT Press, Apr. 2008

    2008

  24. [32]

    The Observational Power of Clocks,

    R. Alur, C. Courcoubetis, and T. A. Henzinger, “The Observational Power of Clocks,” inCONCUR ’94: Concurrency Theory, B. Jonsson and J. Parrow, Eds. Berlin, Heidelberg: Springer, 1994, pp. 162–177

    1994

  25. [33]

    Analysis of Timed Systems Using Time- Abstracting Bisimulations,

    S. Tripakis and S. Yovine, “Analysis of Timed Systems Using Time- Abstracting Bisimulations,”Formal Methods in System Design, vol. 18, no. 1, pp. 25–68, Jan. 2001

    2001

  26. [34]

    IronFleet: proving practical distributed systems correct,

    C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill, “IronFleet: proving practical distributed systems correct,” inProceedings of the 25th Symposium on Operating Systems Principles, ser. SOSP ’15. New York, NY , USA: Association ...

    2015

  27. [35]

    IronFleet: proving safety and liveness of practical distributed systems,

    ——, “IronFleet: proving safety and liveness of practical distributed systems,”Commun. ACM, vol. 60, no. 7, pp. 83–92, Jun. 2017

    2017

  28. [36]

    Dafny: An Automatic Program Verifier for Functional Correctness,

    K. R. M. Leino, “Dafny: An Automatic Program Verifier for Functional Correctness,” inLogic for Programming, Artificial Intelligence, and Reasoning, E. M. Clarke and A. V oronkov, Eds. Berlin, Heidelberg: Springer, 2010, pp. 348–370

    2010

  29. [37]

    Smart Casual Verification of the Confidential Consortium Framework,

    H. Howard, M. A. Kuppe, E. Ashton, A. Chamayou, and N. Crooks, “Smart Casual Verification of the Confidential Consortium Framework,” Oct. 2024, arXiv:2406.17455 [cs]

    2024 arXiv

  30. [38]

    The TAMARIN Prover for the Symbolic Analysis of Security Protocols,

    S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The TAMARIN Prover for the Symbolic Analysis of Security Protocols,” inComputer Aided Verification, N. Sharygina and H. Veith, Eds. Berlin, Heidelberg: Springer, 2013, pp. 696–701

    2013

  31. [39]

    Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif,

    B. Blanchet, “Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif,”Foundations and Trends in Privacy and Security, vol. 1, no. 1-2, pp. 1–135, Oct. 2016

    2016

  32. [40]

    Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols,

    D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols,”IEEE Security & Privacy, vol. 20, no. 3, pp. 24–32, May 2022. 15

    2022

  33. [41]

    T. T. Team,Tamarin-Prover Manual, 2024. [Online]. Available: https://tamarin-prover.com/manual/master/tex/tamarin-manual.pdf

    2024

  34. [42]

    The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm,

    B. Blanchet, “The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm,”Electronic Proceedings in Theoretical Computer Science, vol. 373, pp. 14–22, Nov. 2022, arXiv:2211.12227 [cs]

    2022 arXiv

  35. [43]

    (2024) BOLT 2: Peer Protocol for Channel Management

    Various. (2024) BOLT 2: Peer Protocol for Channel Management. [Online]. Available: https://github.com/lightning/bolts/blob/master/ 02-peer-protocol.md

    2024

  36. [44]

    LockDown: Balance Availability Attack Against Lightning Network Channels,

    C. P ´erez-Sol`a, A. Ranchal-Pedrosa, J. Herrera-Joancomart´ı, G. Navarro- Arribas, and J. Garcia-Alfaro, “LockDown: Balance Availability Attack Against Lightning Network Channels,” inFinancial Cryptography and Data Security, ser. Lecture Notes in Computer Science, J. Bonneau ...

    2020

  37. [45]

    Congestion Attacks in Payment Channel Networks,

    A. Mizrahi and A. Zohar, “Congestion Attacks in Payment Channel Networks,” inFinancial Cryptography and Data Security, N. Borisov and C. Diaz, Eds. Berlin, Heidelberg: Springer, 2021, pp. 170–188

    2021

  38. [46]

    Discharged Payment Chan- nels: Quantifying the Lightning Network’s Resilience to Topology-Based Attacks,

    E. Rohrer, J. Malliaris, and F. Tschorsch, “Discharged Payment Chan- nels: Quantifying the Lightning Network’s Resilience to Topology-Based Attacks,” in2019 IEEE European Symposium on Security and Privacy Workshops (EuroS PW), Jun. 2019, pp. 347–356, iSSN: null

    2019

  39. [47]

    General Congestion Attack on HTLC-Based Payment Channel Networks,

    Z. Lu, R. Han, and J. Yu, “General Congestion Attack on HTLC-Based Payment Channel Networks,” inDROPS- IDN/v2/document/10.4230/OASIcs.Tokenomics.2021.2. Schloss Dagstuhl – Leibniz-Zentrum f ¨ur Informatik, 2022

    2021 doi

  40. [48]

    Route Hijacking and DoS in Off-Chain Networks,

    S. Tochner, A. Zohar, and S. Schmid, “Route Hijacking and DoS in Off-Chain Networks,” inProceedings of the 2nd ACM Conference on Advances in Financial Technologies, ser. AFT ’20. New York, NY , USA: Association for Computing Machinery, Oct. 2020, pp. 228–240

    2020

  41. [49]

    Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability,

    G. Malavolta, P. Moreno-Sanchez, C. Schneidewind, A. Kate, and M. Maffei, “Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability,” inProceedings 2019 Network and Distributed System Security Symposium. San Diego, CA: Internet Society, 2019

    2019

  42. [50]

    A Quantitative Analysis of Security, Anonymity and Scalability for the Lightning Network,

    S. Tikhomirov, P. Moreno-Sanchez, and M. Maffei, “A Quantitative Analysis of Security, Anonymity and Scalability for the Lightning Network,” in2020 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW), Sep. 2020, pp. 387–396

    2020

  43. [51]

    On the Difficulty of Hiding the Balance of Lightning Network Channels,

    J. Herrera-Joancomart ´ı, G. Navarro-Arribas, A. Ranchal-Pedrosa, C. P ´erez-Sol`a, and J. Garcia-Alfaro, “On the Difficulty of Hiding the Balance of Lightning Network Channels,” inProceedings of the 2019 ACM Asia Conference on Computer and Communications Security, ser. Asia C...

    2019

  44. [52]

    Improvements of the Balance Discovery Attack on Lightning Network Payment Channels,

    G. van Dam, R. A. Kadir, P. N. E. Nohuddin, and H. B. Zaman, “Improvements of the Balance Discovery Attack on Lightning Network Payment Channels,” inICT Systems Security and Privacy Protection, M. H ¨olbl, K. Rannenberg, and T. Welzer, Eds. Cham: Springer International Publish...

    2020

  45. [53]

    Counting Down Thunder: Timing Attacks on Privacy in Payment Channel Networks,

    E. Rohrer and F. Tschorsch, “Counting Down Thunder: Timing Attacks on Privacy in Payment Channel Networks,” inProceedings of the 2nd ACM Conference on Advances in Financial Technologies, ser. AFT ’20. New York, NY , USA: Association for Computing Machinery, Oct. 2020, pp. 214–227

    2020

  46. [54]

    An Empirical Analysis of Privacy in the Lightning Network,

    G. Kappos, H. Yousaf, A. Piotrowska, S. Kanjalkar, S. Delgado-Segura, A. Miller, and S. Meiklejohn, “An Empirical Analysis of Privacy in the Lightning Network,” inFinancial Cryptography and Data Security, N. Borisov and C. Diaz, Eds. Berlin, Heidelberg: Springer, 2021, pp. 167–186

    2021

  47. [55]

    Cross-Layer Deanonymization Methods in the Lightning Protocol,

    M. Romiti, F. Victor, P. Moreno-Sanchez, P. S. Nordholt, B. Hasl- hofer, and M. Maffei, “Cross-Layer Deanonymization Methods in the Lightning Protocol,” inFinancial Cryptography and Data Security, ser. Lecture Notes in Computer Science, N. Borisov and C. Diaz, Eds. Berlin, Hei...

    2021

  48. [56]

    How Lightning’s Routing Diminishes its Anonymity,

    S. P. Kumble, D. Epema, and S. Roos, “How Lightning’s Routing Diminishes its Anonymity,” inProceedings of the 16th International Conference on Availability, Reliability and Security, ser. ARES ’21. New York, NY , USA: Association for Computing Machinery, Aug. 2021, pp. 1–10

    2021

  49. [57]

    Analysis and Probing of Parallel Channels in the Lightning Network,

    A. Biryukov, G. Naumenko, and S. Tikhomirov, “Analysis and Probing of Parallel Channels in the Lightning Network,” inFinancial Cryptog- raphy and Data Security, I. Eyal and J. Garay, Eds. Cham: Springer International Publishing, 2022, pp. 337–357

    2022

  50. [58]

    On the (Not So) Surprising Impact of Multi- Path Payments on Performance And Privacy in the Lightning Network,

    C. Ndolo and F. Tschorsch, “On the (Not So) Surprising Impact of Multi- Path Payments on Performance And Privacy in the Lightning Network,” inComputer Security. ESORICS 2023 International Workshops, S. Kat- sikas, F. Cuppens, N. Cuppens-Boulahia, C. Lambrinoudakis, J. Garcia- ...

    2023

  51. [59]

    Flood & Loot: A Systemic Attack on The Lightning Network,

    J. Harris and A. Zohar, “Flood & Loot: A Systemic Attack on The Lightning Network,” inProceedings of the 2nd ACM Conference on Advances in Financial Technologies, ser. AFT ’20. New York, NY , USA: Association for Computing Machinery, Oct. 2020, pp. 202–213

    2020

  52. [60]

    Time-Dilation Attacks on the Lightning Network,

    A. Riard and G. Naumenko, “Time-Dilation Attacks on the Lightning Network,”arXiv:2006.01418 [cs], Jun. 2020. [Online]. Available: http://arxiv.org/abs/2006.01418

    2006 arXiv

  53. [61]

    Timelocked Brib- ing,

    T. Nadahalli, M. Khabbazian, and R. Wattenhofer, “Timelocked Brib- ing,” inFinancial Cryptography and Data Security, N. Borisov and C. Diaz, Eds. Berlin, Heidelberg: Springer, 2021, pp. 53–72

    2021

  54. [62]

    Mass Exit Attacks on the Lightning Network,

    C. Sguanci and A. Sidiropoulos, “Mass Exit Attacks on the Lightning Network,” in2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), May 2023, pp. 1–3, iSSN: 2832-8906

    2023

  55. [63]

    R. Russell. (2019) Full Disclosure: CVE-2019-12998 / CVE-2019-12999 / CVE-2019-13000. [Online]. Available: https://lists.linuxfoundation. org/pipermail/lightning-dev/2019-September/002174.html

    2019

  56. [64]

    Validating Traces of Distributed Programs Against TLA+ Specifications,

    H. Cirstea, M. A. Kuppe, B. Loillier, and S. Merz, “Validating Traces of Distributed Programs Against TLA+ Specifications,” inSoftware Engineering and Formal Methods, A. Madeira and A. Knapp, Eds. Cham: Springer Nature Switzerland, 2025, pp. 126–143

    2025

  57. [65]

    A Composable Security Treatment of the Lightning Network,

    A. Kiayias and O. S. Thyfronitis Litos, “A Composable Security Treatment of the Lightning Network,” 2019, report Number: 778. [Online]. Available: https://eprint.iacr.org/2019/778

    2019

  58. [66]

    How to write a 21st century proof,

    L. Lamport, “How to write a 21st century proof,”Journal of Fixed Point Theory and Applications, vol. 11, no. 1, pp. 43–63, Mar. 2012. APPENDIX A. On the Formalization of [25] While working on the formalization of Lightning in TLA +, we found the following two flaws in the form...

    2012

  59. [67]

    If a user wants to receive a payment, the user creates an invoice and sends it to the user who wants to send the payment

    Multi-Hop Payments:This section explains how Light- ning implements multi-hop payments. If a user wants to receive a payment, the user creates an invoice and sends it to the user who wants to send the payment. The invoice (see Table III) contains a payment hash for which the r...

  60. [68]

    The formalization describes all possible actions how a user of the payment channel initiates transactions or reacts to messages or events

    Formalization Overview:We formalize Lightning in TLA+. The formalization describes all possible actions how a user of the payment channel initiates transactions or reacts to messages or events. In its structure, the formalization of the protocol specification follows the infor...

  61. [69]

    Formalization of Multi-Hop Payments:The actions of a user as described in Section B1 are specified as actions of the HTLCUser module. The actions in the HTLCUser module are the actions of one specific userufor a specific channelcand are parameterized by the id of channelc, the...

  62. [70]

    To reduce the risk of being tracked by third parties, each user in Lightning has a set of private and public keys of which each key is used for one specific purpose

    Keys and Funding-, Commitment- and HTLC- Transactions:In this section, we present the keys that are used in Lightning and what they are used for. To reduce the risk of being tracked by third parties, each user in Lightning has a set of private and public keys of which each key...

  63. [71]

    Here, we explain these keys as they are used in Lightning

    Keys and Key Derivation:Lightning makes use of mul- tiple keys to build transactions. Here, we explain these keys as they are used in Lightning. For the formalization, we use a simplified model that we will present below. Each user has the following set of keys according to th...

  64. [72]

    What is left are the revocation public keys that are derived from the revocation basepoint of one user and theotheruser’s per commitment point

    Formalization of Keys:To keep the specification simple, we model the funding pubkey and the various keys that are derived from a basepoint of a user and the user’s per commit- ment point as the same key pair. What is left are the revocation public keys that are derived from th...

  65. [73]

    The commitment transaction has one input that references the funding transaction’s output

    Transactions:The funding transaction contains an out- put whose amount equals the capacity of the payment channel and which can be spent using signatures for both users’ funding pubkey. The commitment transaction has one input that references the funding transaction’s output. ...

  66. [74]

    An output of a transaction is a record that contains an id, an amount, and a set of conditions of which one needs to be fulfilled to spend the output

    Formalization of Transactions:The formalization of transactions follows the UTXO (unspent transaction output) model of Bitcoin: A transaction is a record that contains a set of inputs, a set of outputs and additional data like the transaction’s id, and an optional absolute tim...

  67. [75]

    The open channel message contains several fields for the parameterization of the channel that we ignore for the TLA + formalization (see Table IX)

    Opening a Payment Channel:To open a payment chan- nel, the funder of the payment channel sends an open channel message to the user to whom the channel should be opened. The open channel message contains several fields for the parameterization of the channel that we ignore for ...

  68. [76]

    As in the module HTLCUser, the actions of the module PaymentChannelUser are parameterized for a specific useruand a payment channel cof useru

    Formalization of Opening a Payment Channel:The module PaymentChannelUser contains the actions to open, update, and close a payment channel. As in the module HTLCUser, the actions of the module PaymentChannelUser are parameterized for a specific useruand a payment channel cof u...

  69. [77]

    Updating a Payment Channel:After a user has sent at least one ‘update add htlc’ message (see Table XIV) to inform the other user about an HTLC, the user sends a ‘commitment - signed’ message. The ‘commitment signed’ message contains a signature for the new commitment transacti...

  70. [78]

    The actions find HTLCs to be updated by the states of the HTLCs and update the states of the HTLCs according to Fig

    Formalization of Updating a Payment Channel:When the useruis in state ‘rev-keys-exchanged’, the action ‘Send- SignedCommitment’ can be enabled if there is at least one HTLC to add or remove and the action ‘ReceiveSignedCom- mitment’ can be enabled if there is a ‘commitment sig...

  71. [79]

    Closing a Payment Channel:There are two ways to close a payment channel: The simplest way is to close the channel by publishing the latest commitment transaction on the blockchain. Both parties can also create a dedicated closing transaction that cannot be revoked and, thus, d...

  72. [80]

    This can either be done honestly modeled by the action ‘CloseChannel’ or dishonestly modeled by the action ‘Cheat’

    Formalization of Closing a Payment Channel:In the formalization, a payment channel can only be closed by pub- lishing a commitment transaction on the blockchain. This can either be done honestly modeled by the action ‘CloseChannel’ or dishonestly modeled by the action ‘Cheat’....

  73. [81]

    A message is sent by an action that specifies that the channel’s message queue is extended by the message that is sent

    Formalization of Messages:The exchange of messages in a channel is modeled by letting the users write messages to a message queue per channel from which each user can read the user’s first message. A message is sent by an action that specifies that the channel’s message queue ...

  74. [82]

    The values used in Lightning for timelocks are numbers that indicate a specific height of the Bitcoin blockchain

    Formalization of Time Flow:HTLCs as well as com- mitment transactions use timelocks to enforce that certain actions cannot be done before a certain point in time. The values used in Lightning for timelocks are numbers that indicate a specific height of the Bitcoin blockchain. ...

  75. [83]

    Therefore, to model honest behavior of user B, we need to model that user B performs an action before the variable LedgerTime reaches the value 10

    However, if the value of the variable LedgerTime was increased to 10 before user B fulfills the HTLC, user B would not have followed the protocol which requires user B to fulfill the HTLC before the HTLC’s timeout. Therefore, to model honest behavior of user B, we need to mode...

  76. [84]

    For example, a user must respond to a ‘commitment signed’ message with a ‘revoke and ack’ message

    Liveness of Users:The Lightning protocol requires that honest users perform certain steps if they can. For example, a user must respond to a ‘commitment signed’ message with a ‘revoke and ack’ message. In the TLA + specification, we model these requirements using a weak fairne...

  77. [85]

    The specificationSpec S must be an explicit-time real-time spec- ification with a set of clocksXand anAdvanceTime S action

    Real-Time SpecificationSpec S :The real-time specifica- tionSpec S to be optimized is defined asSpec S “Init S ^ ˝rNextSsvS ^Liveness S with the set of variablesv S . The specificationSpec S must be an explicit-time real-time spec- ification with a set of clocksXand anAdvanceT...

  78. [86]

    Thus, the only difference between specificationsSand ˆSis how time is advanced by theAdvanceTimeactions

    Optimized Specification ˆS:We define the optimized specification ˆSwith the variablesv ˆS “v S as:Spec ˆS “ Init ˆS ^˝rNext ˆSsvarsˆS ^Liveness ˆS withInit ˆS “Init S and Next ˆS “AdvanceTime ˆS _NextI ˆS andNextI ˆS “NextI S andLiveness ˆS “Liveness S . Thus, the only differe...

  79. [87]

    Extended Real-Time SpecificationSpec S 1:Because the proof that specificationSpec S implements specificationSpec ˆS needs auxiliary variables for defining how a clock is mapped to specificationSpec S , we define an extended specification SpecS 1 that wraps specificationSpec S ...

  80. [88]

    Proof of Theorem 9:In the proof, we use the following notation: Fis formula F in which each clockxPXis replaced by the variablemappedClock x . Formally, this can be expressed using the notationFWITHv 1Ðe 1,v 2Ðe 2 to describe the expressionFwhere variablev 1 is substituted by ...

  81. [89]

    Because the setrelETP LedgerTimepsqcontains the HTLC’s timelock`G`1for every HTLC that can be fulfilled, this condition is fulfilled. x2y12.@sPΣ :@nPETP LedgerTimepsq:apnq “ SendHTLCFailñnPrelETP LedgerTimepsq The action SendHTLCFail depends on LedgerTime to fail an HTLC that ...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.