{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:31:00Z","timestamp":1767983460844,"version":"3.49.0"},"publisher-location":"Cham","reference-count":65,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-10794-7_16","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:06Z","timestamp":1763188986000},"page":"313-335","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Security of\u00a0the\u00a0Lightning Network: Model Checking a\u00a0Stepwise Refinement with\u00a0TLA+"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1352-0625","authenticated-orcid":false,"given":"Matthias","family":"Grundmann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3441-3180","authenticated-orcid":false,"given":"Hannes","family":"Hartenstein","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507\u2013535 (1995). https:\/\/doi.org\/10.1145\/203095.201069","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-48654-1_16","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R Alur","year":"1994","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162\u2013177. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/978-3-540-48654-1_16"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032042"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, \u0141.: Modeling bitcoin contracts by timed automata. In: Legay, A., Bozga, M. (eds.) Formal Modeling and Analysis of Timed Systems, pp. 7\u201322. Springer International Publishing, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10512-3_2","DOI":"10.1007\/978-3-319-10512-3_2"},{"key":"16_CR5","unstructured":"Barbaravi\u010dius, V.: Year-over-Year Data Shows Rising Lightning Network Adoption|CoinGate (2024). https:\/\/coingate.com\/blog\/post\/lightning-network-year-over-year-data"},{"issue":"3","key":"16_CR6","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MSEC.2022.3154689","volume":"20","author":"D Basin","year":"2022","unstructured":"Basin, D., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real-world, cryptographic protocols. IEEE Secur. Priv. 20(3), 24\u201332 (2022). https:\/\/doi.org\/10.1109\/MSEC.2022.3154689","journal-title":"IEEE Secur. Priv."},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Biryukov, A., Naumenko, G., Tikhomirov, S.: Analysis and\u00a0probing of\u00a0parallel channels in\u00a0the\u00a0lightning network. In: Eyal, I., Garay, J. (eds.) Financial Cryptography and Data Security, pp. 337\u2013357. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-18283-9_16","DOI":"10.1007\/978-3-031-18283-9_16"},{"issue":"1\u20132","key":"16_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/3300000004","volume":"1","author":"B Blanchet","year":"2016","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations Trends Priv. Secur. 1(1\u20132), 1\u2013135 (2016). https:\/\/doi.org\/10.1561\/3300000004","journal-title":"Foundations Trends Priv. Secur."},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"14","DOI":"10.4204\/EPTCS.373.2","volume":"373","author":"B Blanchet","year":"2022","unstructured":"Blanchet, B.: The security protocol verifier ProVerif and its horn clause resolution algorithm. Electron. Proc. Theoret. Comput. Sci. 373, 14\u201322 (2022). https:\/\/doi.org\/10.4204\/EPTCS.373.2","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"key":"16_CR10","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd Your Herd of Provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, p.\u00a053 (2011). https:\/\/inria.hal.science\/view\/index\/identifiant\/hal-00790310"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"B\u00f6gli, R., Lerena, L., Tsigkanos, C., Kehrer, T.: A Systematic literature review on\u00a0a\u00a0decade of\u00a0industrial TLA+\u00a0practice. In: Kosmatov, N., Kov\u00e1cs, L. (eds.) Integrated Formal Methods, pp. 24\u201334. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-76554-4_2","DOI":"10.1007\/978-3-031-76554-4_2"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de\u00a0Roever, W.P., Langmaack, H., Pnueli, A. (eds.) Compositionality: The Significant Difference, pp. 103\u2013129. Springer, Berlin, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49213-5_5","DOI":"10.1007\/3-540-49213-5_5"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda \u2013 a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, pp. 73\u201378. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_6","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Boyd, C., Gj\u00f8steen, K., Wu, S.: A blockchain model in tamarin and formal analysis of hash time lock contract. In: DROPS-IDN\/v2\/document\/10.4230\/OASIcs.FMBC.2020.5. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/OASIcs.FMBC.2020.5","DOI":"10.4230\/OASIcs.FMBC.2020.5"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0055357","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 298\u2013302. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055357"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Brugger, L.S., Kov\u00e1cs, L., Petkovic\u00a0Komel, A., Rain, S., Rawson, M.: CheckMate: automated game-theoretic security reasoning. In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, pp. 1407\u20131421. CCS \u201923, Association for Computing Machinery, New York, NY, USA (Nov 2023). https:\/\/doi.org\/10.1145\/3576915.3623183","DOI":"10.1145\/3576915.3623183"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: Proceedings 42nd IEEE Symposium on Foundations of Computer Science, pp. 136\u2013145 (2001). https:\/\/doi.org\/10.1109\/SFCS.2001.959888","DOI":"10.1109\/SFCS.2001.959888"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Cirstea, H., Kuppe, M.A., Loillier, B., Merz, S.: Validating traces of\u00a0distributed programs against TLA+ specifications. In: Madeira, A., Knapp, A. (eds.) Software Engineering and Formal Methods, pp. 126\u2013143. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-77382-2_8","DOI":"10.1007\/978-3-031-77382-2_8"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp. 353\u2013362 (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39190","DOI":"10.1109\/LICS.1989.39190"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"van Dam, G., Kadir, R.A., Nohuddin, P.N.E., Zaman, H.B.: Improvements of the balance discovery attack on lightning network payment channels. In: H\u00f6lbl, M., Rannenberg, K., Welzer, T. (eds.) ICT Systems Security and Privacy Protection, pp. 313\u2013323. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58201-2_21","DOI":"10.1007\/978-3-030-58201-2_21"},{"key":"16_CR21","unstructured":"Fabia\u0144ski, G., Stefa\u0144ski, R., Thyfronitis\u00a0Litos, O.S.: A Formally Verified Lightning Network (2025). https:\/\/fc25.ifca.ai\/preproceedings\/63.pdf"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Grundmann, M., Hartenstein, H.: Model Checking the Security of the Lightning Network (2025). https:\/\/doi.org\/10.48550\/arXiv.2505.15568","DOI":"10.48550\/arXiv.2505.15568"},{"key":"16_CR23","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17206471","author":"M Grundmann","year":"2025","unstructured":"Grundmann, M., Hartenstein, H.: TLA+ specification of lightning, security property, and refinement mappings. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.17206471","journal-title":"Zenodo"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Harris, J., Zohar, A.: Flood & loot: a systemic attack on the lightning network. In: Proceedings of the 2nd ACM Conference on Advances in Financial Technologies, pp. 202\u2013213. AFT \u201920, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3419614.3423248","DOI":"10.1145\/3419614.3423248"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Herrera-Joancomart\u00ed, J., Navarro-Arribas, G., Ranchal-Pedrosa, A., P\u00e9rez-Sol\u00e0, C., Garcia-Alfaro, J.: On the difficulty of hiding the balance of lightning network channels. In: Proceedings of the 2019 ACM Asia Conference on Computer and Communications Security, pp. 602\u2013612. Asia CCS \u201919, Association for Computing Machinery, Auckland, New Zealand (2019). https:\/\/doi.org\/10.1145\/3321705.3329812","DOI":"10.1145\/3321705.3329812"},{"key":"16_CR26","unstructured":"Howard, H., Kuppe, M.A., Ashton, E., Chamayou, A., Crooks, N.: Smart casual verification of the confidential consortium framework. In: Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation, pp. 259\u2013276. USENIX Association, Philadelphia, PA, USA (2025)"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H., Starove\u0161ki, V.: Secrecy and Authenticity Properties of the Lightning Network Protocol, pp. 119\u2013130 (2020). https:\/\/www.scitepress.org\/Link.aspx?doi=10.5220\/0008974801190130","DOI":"10.5220\/0008974801190130"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"H\u00fcttel, H., Starove\u0161ki, V.: Key agreement in the lightning network protocol. In: Furnell, S., Mori, P., Weippl, E., Camp, O. (eds.) Information Systems Security and Privacy, pp. 139\u2013155. Communications in Computer and Information Science, Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94900-6_7","DOI":"10.1007\/978-3-030-94900-6_7"},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Kappos, G., et al.: An empirical analysis of privacy in the lightning network. In: Borisov, N., Diaz, C. (eds.) Financial Cryptography and Data Security, pp. 167\u2013186. Springer, Berlin, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-662-64322-8_8","DOI":"10.1007\/978-3-662-64322-8_8"},{"key":"16_CR30","unstructured":"Kiayias, A., Thyfronitis\u00a0Litos, O.S.: A Composable Security Treatment of the Lightning Network (2019). https:\/\/eprint.iacr.org\/2019\/778"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Kiayias, A., Thyfronitis\u00a0Litos, O.S.: A composable security treatment of the lightning network. In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF), pp. 334\u2013349 (2020). https:\/\/doi.org\/10.1109\/CSF49147.2020.00031","DOI":"10.1109\/CSF49147.2020.00031"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Kumble, S.P., Epema, D., Roos, S.: How lightning\u2019s routing diminishes its anonymity. In: Proceedings of the 16th International Conference on Availability, Reliability and Security, pp. 1\u201310. ARES \u201921, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3465481.3465761","DOI":"10.1145\/3465481.3465761"},{"issue":"3","key":"16_CR33","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994). https:\/\/doi.org\/10.1145\/177492.177726","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR34","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc, USA (2002)"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) Correct Hardware Design and Verification Methods. pp. 162\u2013175. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560548_14","DOI":"10.1007\/11560548_14"},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Int. J. Softw. Tools Technolo. Transfer 1(1-2), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Lu, Z., Han, R., Yu, J.: General congestion attack on HTLC-based payment channel networks. In: DROPS-IDN\/v2\/document\/10.4230\/OASIcs.Tokenomics.2021.2. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/OASIcs.Tokenomics.2021.2","DOI":"10.4230\/OASIcs.Tokenomics.2021.2"},{"key":"16_CR38","doi-asserted-by":"publisher","unstructured":"Malavolta, G., Moreno-Sanchez, P., Schneidewind, C., Kate, A., Maffei, M.: Anonymous multi-hop locks for blockchain scalability and interoperability. In: Proceedings 2019 Network and Distributed System Security Symposium. Internet Society, San Diego, CA (2019). https:\/\/doi.org\/10.14722\/ndss.2019.23330","DOI":"10.14722\/ndss.2019.23330"},{"key":"16_CR39","doi-asserted-by":"publisher","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 696\u2013701. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Merz, S.: Formal specification and verification. In: Concurrency: the Works of Leslie Lamport, pp. 103\u2013129. Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3335772.3335780","DOI":"10.1145\/3335772.3335780"},{"key":"16_CR41","unstructured":"Microsoft Research \u2013 Inria Joint Centre: TLA+ Proof System (2025). https:\/\/proofs.tlapl.us\/doc\/web\/content\/Home.html"},{"key":"16_CR42","doi-asserted-by":"publisher","unstructured":"Mizrahi, A., Zohar, A.: Congestion attacks in payment channel networks. In: Borisov, N., Diaz, C. (eds.) Financial Cryptography and Data Security, pp. 170\u2013188. Springer, Berlin, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-662-64331-0_9","DOI":"10.1007\/978-3-662-64331-0_9"},{"key":"16_CR43","doi-asserted-by":"publisher","unstructured":"Nadahalli, T., Khabbazian, M., Wattenhofer, R.: Timelocked bribing. In: Borisov, N., Diaz, C. (eds.) Financial Cryptography and Data Security, pp. 53\u201372. Springer, Berlin, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-662-64322-8_3","DOI":"10.1007\/978-3-662-64322-8_3"},{"key":"16_CR44","unstructured":"Nakamoto, S.: Bitcoin: A Peer-to-Peer Electronic Cash System. Tech. rep. (2008)"},{"key":"16_CR45","doi-asserted-by":"publisher","unstructured":"Ndolo, C., Tschorsch, F.: On the\u00a0(Not So) surprising impact of\u00a0multi-path payments on\u00a0performance and privacy in\u00a0the\u00a0lightning network. In: Katsikas, S., et al. (eds.) Computer Security. ESORICS 2023 International Workshops, pp. 411\u2013427. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-54204-6_25","DOI":"10.1007\/978-3-031-54204-6_25"},{"key":"16_CR46","doi-asserted-by":"publisher","unstructured":"P\u00e9rez-Sol\u00e0, C., Ranchal-Pedrosa, A., Herrera-Joancomart\u00ed, J., Navarro-Arribas, G., Garcia-Alfaro, J.: LockDown: balance availability attack against lightning network channels. In: Bonneau, J., Heninger, N. (eds.) Financial Cryptography and Data Security, pp. 245\u2013263. Lecture Notes in Computer Science, Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51280-4_14","DOI":"10.1007\/978-3-030-51280-4_14"},{"key":"16_CR47","unstructured":"Poon, J., Dryja, T.: The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. Tech. rep. (2016)"},{"key":"16_CR48","doi-asserted-by":"publisher","unstructured":"Rain, S., Avarikioti, G., Kov\u00e1cs, L., Maffei, M.: Towards a game-theoretic security analysis of off-chain protocols. In: 2023 IEEE 36th Computer Security Foundations Symposium (CSF), pp. 107\u2013122 (2023). https:\/\/doi.org\/10.1109\/CSF57540.2023.00003","DOI":"10.1109\/CSF57540.2023.00003"},{"key":"16_CR49","doi-asserted-by":"crossref","unstructured":"Riard, A., Naumenko, G.: Time-Dilation Attacks on the Lightning Network. arXiv:2006.01418 [cs] (2020). http:\/\/arxiv.org\/abs\/2006.01418","DOI":"10.21428\/58320208.6ac6960a"},{"key":"16_CR50","doi-asserted-by":"publisher","unstructured":"Rohrer, E., Malliaris, J., Tschorsch, F.: Discharged payment channels: quantifying the lightning network\u2019s resilience to topology-based attacks. In: 2019 IEEE European Symposium on Security and Privacy Workshops (EuroS PW), pp. 347\u2013356 (2019). https:\/\/doi.org\/10.1109\/EuroSPW.2019.00045","DOI":"10.1109\/EuroSPW.2019.00045"},{"key":"16_CR51","doi-asserted-by":"publisher","unstructured":"Rohrer, E., Tschorsch, F.: Counting down thunder: timing attacks on privacy in payment channel networks. In: Proceedings of the 2nd ACM Conference on Advances in Financial Technologies, pp. 214\u2013227. AFT \u201920, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3419614.3423262","DOI":"10.1145\/3419614.3423262"},{"key":"16_CR52","doi-asserted-by":"publisher","unstructured":"Romiti, M., et al.: Cross-layer deanonymization methods in the lightning protocol. In: Borisov, N., Diaz, C. (eds.) Financial Cryptography and Data Security, pp. 187\u2013204. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-662-64322-8_9","DOI":"10.1007\/978-3-662-64322-8_9"},{"key":"16_CR53","unstructured":"Russell, R.: Full Disclosure: CVE-2019-12998 \/ CVE-2019-12999 \/ CVE-2019-13000 (2019). https:\/\/lists.linuxfoundation.org\/pipermail\/lightning-dev\/2019-September\/002174.html"},{"key":"16_CR54","doi-asserted-by":"publisher","unstructured":"Setzer, A.: Modelling Bitcoin in Agda (2018). https:\/\/doi.org\/10.48550\/arXiv.1804.06398","DOI":"10.48550\/arXiv.1804.06398"},{"key":"16_CR55","doi-asserted-by":"publisher","unstructured":"Sguanci, C., Sidiropoulos, A.: Mass exit attacks on the lightning network. In: 2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), pp.\u00a01\u20133 (2023). https:\/\/doi.org\/10.1109\/ICBC56567.2023.10174926","DOI":"10.1109\/ICBC56567.2023.10174926"},{"key":"16_CR56","unstructured":"The Tamarin Team: Tamarin-Prover Manual (2024). https:\/\/tamarin-prover.com\/manual\/master\/tex\/tamarin-manual.pdf"},{"key":"16_CR57","doi-asserted-by":"publisher","unstructured":"Tikhomirov, S., Moreno-Sanchez, P., Maffei, M.: A quantitative analysis of security, anonymity and scalability for the lightning network. In: 2020 IEEE European Symposium on Security and Privacy Workshops (EuroS &PW), pp. 387\u2013396 (2020). https:\/\/doi.org\/10.1109\/EuroSPW51379.2020.00059","DOI":"10.1109\/EuroSPW51379.2020.00059"},{"key":"16_CR58","doi-asserted-by":"publisher","unstructured":"Tochner, S., Zohar, A., Schmid, S.: Route hijacking and DoS in off-chain networks. In: Proceedings of the 2nd ACM Conference on Advances in Financial Technologies, pp. 228\u2013240. AFT \u201920, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3419614.3423253","DOI":"10.1145\/3419614.3423253"},{"issue":"1","key":"16_CR59","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1023\/A:1008734703554","volume":"18","author":"S Tripakis","year":"2001","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods Syst. Design 18(1), 25\u201368 (2001). https:\/\/doi.org\/10.1023\/A:1008734703554","journal-title":"Formal Methods Syst. Design"},{"key":"16_CR60","unstructured":"Various: Core Lightning, htlc_state.h (2018). https:\/\/github.com\/ElementsProject\/lightning\/blob\/master\/common\/htlc_state.h"},{"key":"16_CR61","unstructured":"Various: BOLT 2: Peer Protocol for Channel Management (2024). https:\/\/github.com\/lightning\/bolts\/blob\/master\/02-peer-protocol.md"},{"key":"16_CR62","unstructured":"Various: BOLT: Basis of Lightning Technology (Lightning Network In-Progress Specifications) (2024). https:\/\/github.com\/lightning\/bolts"},{"key":"16_CR63","unstructured":"Various: Apalache | The Symbolic Model Checker for TLA+ (2025). https:\/\/apalache-mc.org\/"},{"key":"16_CR64","unstructured":"Various: TLA+ Toolbox (2025). https:\/\/github.com\/tlaplus\/tlaplus"},{"key":"16_CR65","doi-asserted-by":"publisher","unstructured":"Weintraub, B., Kumble, S.P., Nita-Rotaru, C., Roos, S.: Payout races and congested channels: a formal analysis of security in the lightning network. In: Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, pp. 2562\u20132576. CCS \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3658644.3670315","DOI":"10.1145\/3658644.3670315"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:58:56Z","timestamp":1767967136000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}