{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T11:02:25Z","timestamp":1775473345509,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":91,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,12,2]],"date-time":"2024-12-02T00:00:00Z","timestamp":1733097600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Sciecne Foundation","award":["1801546"],"award-info":[{"award-number":["1801546"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3670315","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"2562-2576","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9527-5888","authenticated-orcid":false,"given":"Ben","family":"Weintraub","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3132-365X","authenticated-orcid":false,"given":"Satwik Prabhu","family":"Kumble","sequence":"additional","affiliation":[{"name":"TU Delft, Delft, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9649-6789","authenticated-orcid":false,"given":"Cristina","family":"Nita-Rotaru","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8168-8983","authenticated-orcid":false,"given":"Stefanie","family":"Roos","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern-Landau, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,12,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"URL https:\/\/github.com\/ElementsProject\/lightning."},{"key":"e_1_3_2_1_2_1","unstructured":"URL https:\/\/github.com\/ACINQ\/eclair."},{"key":"e_1_3_2_1_3_1","unstructured":"Connector risk mitigations | interledger. URL https:\/\/interledger.org\/rfcs\/0018-connector-risk-mitigations\/draft-3.html."},{"key":"e_1_3_2_1_4_1","volume-title":"May","author":"Bolt","year":"2023","unstructured":"Bolt #2: Peer protocol, May 2023. URL https:\/\/github.com\/lightning\/bolts\/blob\/ b38156b9510c0562cf50f8758a64602cc0315c19\/02-peer-protocol.md. [Online; accessed 20. May. 2023]."},{"key":"e_1_3_2_1_5_1","volume-title":"May","author":"Bolt","year":"2023","unstructured":"Bolt #8: Encrypted and authenticated transport, May 2023. URL https:\/\/github.com\/lightning\/bolts\/blob\/master\/08-transport.md#lightningmessage- specification. [Online; accessed 20. May. 2023]."},{"key":"e_1_3_2_1_6_1","unstructured":"Sep 2023. URL https:\/\/github.com\/coq\/coq."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jksuci.2022.08.029"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_3_2_1_9_1","volume-title":"Jul","author":"Andresen Gavin","year":"2013","unstructured":"Gavin Andresen and Mike Hearn. Bip 70: Payment protocol, Jul 2013. URL https:\/\/bips.dev\/70\/."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373829"},{"key":"e_1_3_2_1_11_1","first-page":"1","volume-title":"Proceedings of the International Conference on Security and Management (SAM)","author":"Arai Kenichi","unstructured":"Kenichi Arai and Toshinobu Kaneko. Formal verification of improved numeric comparison protocol for secure simple paring in bluetooth using proverif. In Proceedings of the International Conference on Security and Management (SAM), page 1. The Steering Committee of The World Congress in Computer Science, 2014."},{"key":"e_1_3_2_1_12_1","first-page":"4043","volume-title":"USENIX Security Symposium","author":"Aumayr Lukas","year":"2021","unstructured":"Lukas Aumayr, Pedro Moreno-Sanchez, Aniket Kate, and Matteo Maffei. Blitz: Secure multi-hop payments without two-phase commits. In USENIX Security Symposium, pages 4043--4060. USENIX Association, 2021."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560556"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185089.3185138"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_2_1_17_1","volume-title":"Paper 2021\/384","author":"Biryukov Alex","year":"2021","unstructured":"Alex Biryukov, Gleb Naumenko, and Sergei Tikhomirov. Analysis and probing of parallel channels in the lightning network. Cryptology ePrint Archive, Paper 2021\/384, 2021. URL https:\/\/eprint.iacr.org\/2021\/384. https:\/\/eprint.iacr.org\/2021\/ 384."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243650"},{"key":"e_1_3_2_1_19_1","volume-title":"Modeling and verifying security protocols with the applied pi calculus and proverif. Foundations and Trends\u00ae in Privacy and Security, 1(1--2): 1--135","author":"Bruno Blanchet","year":"2016","unstructured":"Bruno Blanchet et al. Modeling and verifying security protocols with the applied pi calculus and proverif. Foundations and Trends\u00ae in Privacy and Security, 1(1--2): 1--135, 2016."},{"key":"e_1_3_2_1_20_1","volume-title":"May","author":"BOLT","year":"2023","unstructured":"BOLT: Basis of Lightning Technology (Lightning Network Specifications). Bolt: Basis of lightning technology (lightning network specifications), May 2023. URL https:\/\/github.com\/lightning\/bolts."},{"key":"e_1_3_2_1_21_1","unstructured":"Lea Salome Brugger. Automating proofs of game-theoretic security properties of off-chain protocols. MS Thesis 2022."},{"key":"e_1_3_2_1_22_1","unstructured":"Jonas Bushart and Christian Rossow. Resolfuzz: Differential fuzzing of dns resolvers."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70936-7_4"},{"key":"e_1_3_2_1_24_1","first-page":"45","article-title":"Formal analysis of authentication in bluetooth device pairing","author":"Chang Richard","year":"2007","unstructured":"Richard Chang and Vitaly Shmatikov. Formal analysis of authentication in bluetooth device pairing. Fcs-arspa07, 45, 2007.","journal-title":"Fcs-arspa07"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00087"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00013"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3423354"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00040"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_32_1","volume-title":"Unlinkable outsourced channel monitoring. Talk transcript) https:\/\/diyhpl. us\/wiki\/transcripts\/scalingbitcoin\/milan\/unlinkableoutsourced- channel-monitoring","author":"Dryja Thaddeus","year":"2016","unstructured":"Thaddeus Dryja. Unlinkable outsourced channel monitoring. Talk transcript) https:\/\/diyhpl. us\/wiki\/transcripts\/scalingbitcoin\/milan\/unlinkableoutsourced- channel-monitoring, 2016."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243856"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3345666"},{"key":"e_1_3_2_1_35_1","first-page":"1857","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Girol Guillaume","year":"2020","unstructured":"Guillaume Girol, Lucca Hirschi, Ralf Sasse, Dennis Jackson, Cas Cremers, and David Basin. A spectral analysis of noise: A comprehensive, automated, formal analysis of {Diffie-Hellman} protocols. In 29th USENIX Security Symposium (USENIX Security 20), pages 1857--1874, 2020."},{"key":"e_1_3_2_1_36_1","unstructured":"Ilya Grishchenko Matteo Maffei and Clara Schneidewind. Ethertrust: Sound static analysis of ethereum bytecode. Technische Universit\u00e4t Wien Tech. Rep pages 1--41 2018."},{"key":"e_1_3_2_1_37_1","volume-title":"Verifying Payment Channels with TLA","author":"Grundmann Matthias","year":"2021","unstructured":"Matthias Grundmann. Verifying Payment Channels with TLA. 2021. URL https:\/\/www.youtube.com\/watch?v=wecVT_4QDcU."},{"key":"e_1_3_2_1_38_1","volume-title":"July","author":"Grundmann Matthias","year":"2023","unstructured":"Matthias Grundmann and Hannes Hartenstein. Towards a formal verification of the lightning network with tla. (arXiv:2307.02342), July 2023. URL http: \/\/arxiv.org\/abs\/2307.02342. arXiv:2307.02342 [cs]."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--51280--4_12"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419614.3423248"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3321705.3329812"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_43_1","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson. Software Abstractions: logic, language, and analysis. MIT press, 2012."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3232755.3232769"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3232755.3232769"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-64322-8_8"},{"key":"e_1_3_2_1_48_1","volume-title":"Acl2 version 8.5","author":"Kaufmann Matt","year":"2022","unstructured":"Matt Kaufmann and J. Strother Moore. Acl2 version 8.5, 2022. URL https: \/\/www.cs.utexas.edu\/users\/moore\/acl2\/."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147.2020.00031"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2019.00034"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00017"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2023.23241"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3465481.3465761"},{"key":"e_1_3_2_1_55_1","unstructured":"lightningnetwork\/lnd: Lightning Network Daemon. lightningnetwork\/lnd: Lightning network daemon. URL https:\/\/github.com\/lightningnetwork\/lnd."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3183495"},{"key":"e_1_3_2_1_57_1","volume-title":"An attack on the needham-schroeder public-key authentication protocol. Information processing letters, 56(3)","author":"Lowe Gavin","year":"1995","unstructured":"Gavin Lowe. An attack on the needham-schroeder public-key authentication protocol. Information processing letters, 56(3), 1995."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61042-1_43"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46017-9_14"},{"key":"e_1_3_2_1_60_1","first-page":"455","volume-title":"CCS","author":"Malavolta Giulio","year":"2017","unstructured":"Giulio Malavolta, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei, and Srivatsan Ravi. Concurrency and privacy with payment-channel networks. In CCS, pages 455--471. ACM, 2017."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23330"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318041.3355461"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--32101--7_30"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","unstructured":"Ayelet Mizrahi and Aviv Zohar. Congestion Attacks in Payment Channel Networks volume 12675 of Lecture Notes in Computer Science page 170--188. Springer Berlin Heidelberg Berlin Heidelberg 2021. ISBN 978--3--662--64330--3. doi: 10.1007\/978--3--662--64331-0_9. URL https:\/\/link.springer.com\/10.1007\/978--3--662--64331-0_9.","DOI":"10.1007\/978--3--662--64331-0_9"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2021.102279"},{"key":"e_1_3_2_1_68_1","volume-title":"Bitcoin: A peer-to-peer electronic cash system. Decentralized business review","author":"Nakamoto Satoshi","year":"2008","unstructured":"Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system. Decentralized business review, 2008."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3143145"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/NCA.2014.50"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5220\/0009429200070014"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101129"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51280-4_14"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11277-010-0215-1"},{"key":"e_1_3_2_1_76_1","volume-title":"The bitcoin lightning network: Scalable offchain instant payments","author":"Poon Joseph","year":"2016","unstructured":"Joseph Poon and Thaddeus Dryja. The bitcoin lightning network: Scalable offchain instant payments, 2016."},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00003"},{"key":"e_1_3_2_1_78_1","volume-title":"Jan","author":"Rizzo Pete","year":"2016","unstructured":"Pete Rizzo. Making sense of bitcoin's divisive block size debate, Jan 2016. URL https:\/\/www.coindesk.com\/markets\/2016\/01\/19\/making-sense-of-bitcoinsdivisive- block-size-debate\/."},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419614.3423262"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSPW.2019.00045"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.3390\/electronics9020255"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-07535-3_12"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSPW51379.2020.00059"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00018"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54549-9_9"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2023.24775"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSPW54576.2021.00046"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3517745.3561448"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833777"},{"key":"e_1_3_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2022.101584"}],"event":{"name":"CCS '24: ACM SIGSAC Conference on Computer and Communications Security","location":"Salt Lake City UT USA","acronym":"CCS '24","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3670315","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3670315","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:17:19Z","timestamp":1755843439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3670315"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":91,"alternative-id":["10.1145\/3658644.3670315","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3670315","relation":{},"subject":[],"published":{"date-parts":[[2024,12,2]]},"assertion":[{"value":"2024-12-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}