{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:22:24Z","timestamp":1766442144654,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","funder":[{"DOI":"10.13039\/100016964","name":"Werner Siemens-Stiftung","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100016964","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765131","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:33:16Z","timestamp":1763854396000},"page":"2759-2773","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Looping for Good: Cyclic Proofs for Security Protocols"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-7886-4480","authenticated-orcid":false,"given":"Felix","family":"Linker","sequence":"first","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2941-5165","authenticated-orcid":false,"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0322-2293","authenticated-orcid":false,"given":"Cas","family":"Cremers","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzac053"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005088"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813662"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00037"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(3:10)2019"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_2_2_9_1","volume-title":"33rd USENIX Security Symposium. https:\/\/www.usenix.org\/conference\/usenixsecurity24\/presentation\/bhargavan.","author":"Bhargavan Karthikeyan","year":"2024","unstructured":"Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, and Rolfe Schmidt. 2024. Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. In 33rd USENIX Security Symposium. https:\/\/www.usenix.org\/conference\/usenixsecurity24\/presentation\/bhargavan."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833653"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3439724"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","unstructured":"James Brotherston. 2005. Cyclic Proofs for First-Order Logic with Inductive Definitions. In Automated Reasoning with Analytic Tableaux and Related Methods. doi: 10.1007\/11554554_8.","DOI":"10.1007\/11554554_8"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328453"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","unstructured":"James Brotherston Dino Distefano and Rasmus Lerchedahl Petersen. 2011. Automated Cyclic Entailment Proofs in Separation Logic. In Automated Deduction -- CADE-23. doi: 10.1007\/978--3--642--22438--6_12.","DOI":"10.1007\/978--3--642--22438--6_12"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--35182--2_25"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","unstructured":"Alan Bundy. 2001. Chapter 13 - The Automation of Proof by Mathematical Induction. In Handbook of Automated Reasoning. (Jan. 1 2001). doi: 10.1016\/B978-044450813--3\/50015--1.","DOI":"10.1016\/B978-044450813--3\/50015--1"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00032"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP57164.2023.00016"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3423354"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.35"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00001"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.2.255"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","unstructured":"Anupam Das and Damien Pous. 2017. A Cut-Free Cyclic Proof System for Kleene Algebra. In Automated Reasoning with Analytic Tableaux and Related Methods. doi: 10.1007\/978--3--319--66902--1_16.","DOI":"10.1007\/978--3--319--66902--1_16"},{"key":"e_1_3_2_2_29_1","volume-title":"Formal Analysis of Diffie-Hellman Protocols. In 29th USENIX Security Symposium. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/girol.","author":"Girol Guillaume","year":"2020","unstructured":"Guillaume Girol, Lucca Hirschi, Ralf Sasse, Dennis Jackson, Cas Cremers, and David Basin. 2020. A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols. In 29th USENIX Security Symposium. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/girol."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523731"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2021.29"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/3766078.3766336"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16992323"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.3929\/ethz-c-000783356"},{"key":"e_1_3_2_2_37_1","volume-title":"The X3DH Key Agreement Protocol. Revision 1. (Nov. 4","author":"Marlinspike Moxie","year":"2016","unstructured":"Moxie Marlinspike and Trevor Perrin. 2016. The X3DH Key Agreement Protocol. Revision 1. (Nov. 4, 2016). https:\/\/signal.org\/docs\/specifications\/x3dh\/x3dh.pdf."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.3929\/ethz-a-009790675"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","unstructured":"Simon Meier Benedikt Schmidt Cas Cremers and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification (CAV). doi: 10.1007\/978--3--642--39799--8_48.","DOI":"10.1007\/978--3--642--39799--8_48"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3448300.3467823"},{"key":"e_1_3_2_2_41_1","volume-title":"The Double Ratchet Algorithm. Revision 1. (Nov. 20","author":"Perrin Trevor","year":"2016","unstructured":"Trevor Perrin and Moxie Marlinspike. 2016. The Double Ratchet Algorithm. Revision 1. (Nov. 20, 2016). https:\/\/signal.org\/docs\/specifications\/doubleratchet\/doubleratchet.pdf."},{"volume-title":"Wikipedia. (Dec. 24, 2024","year":"2025","key":"e_1_3_2_2_42_1","unstructured":"2024. Proof by infinite descent. In Wikipedia. (Dec. 24, 2024). Retrieved Apr. 8, 2025 from https:\/\/en.wikipedia.org\/w\/index.php?title=Proof_by_infinite_desc ent&oldid=1264957154."},{"key":"e_1_3_2_2_43_1","unstructured":"Jan Rooduijn Dexter Kozen and Alexandra Silva. 2024. A Cyclic Proof System for Guarded Kleene Algebra with Tests. In Automated Reasoning. doi: 10.1007 \/978--3-031--63501--4_14."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018623"},{"key":"e_1_3_2_2_45_1","volume-title":"Formal Verification of Processes. Master's thesis","author":"Sch\u00f6pp Ulrich","year":"2025","unstructured":"Ulrich Sch\u00f6pp. 2001. Formal Verification of Processes. Master's thesis. University of Edinburgh. Retrieved Apr. 8, 2025 from https:\/\/ulrichschoepp.de\/Docs\/msc.pdf."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","unstructured":"Ulrich Sch\u00f6pp and Alex Simpson. 2002. Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes. In Foundations of Software Science and Computation Structures. doi: 10.1007\/3--540--45931--6_26.","DOI":"10.1007\/3--540--45931--6_26"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","unstructured":"Alex Simpson. 2017. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In Foundations of Software Science and Computation Structures. doi: 10.1007\/978--3--662--54458--7_17.","DOI":"10.1007\/978--3--662--54458--7_17"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2003024"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","unstructured":"Christoph Sprenger and Mads Dam. 2003. On the structure of inductive reasoning: circular and tree-shaped proofs in the \u03bc-calculus. In Foundations of Software Science and Computation Structures. doi: 10.1007\/3--540--36576--1_27.","DOI":"10.1007\/3--540--36576--1_27"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.14778\/3523210.3523218"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09532-0"},{"key":"e_1_3_2_2_52_1","volume-title":"TreeSync: Authenticated Group Management for Messaging Layer Security. In 32nd USENIX Security Symposium. (Aug.","author":"Wallez Th\u00e9ophile","year":"2023","unstructured":"Th\u00e9ophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, and Karthikeyan Bhargavan. 2023. TreeSync: Authenticated Group Management for Messaging Layer Security. In 32nd USENIX Security Symposium. (Aug. 2023). https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/wallez."},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/363"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Taipei Taiwan","acronym":"CCS '25"},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:19:49Z","timestamp":1766441989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":53,"alternative-id":["10.1145\/3719027.3765131","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765131","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}