{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:10:05Z","timestamp":1755843005890,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":42,"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":"ANR","award":["ANR-22-PECY-0006"],"award-info":[{"award-number":["ANR-22-PECY-0006"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3690193","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"2814-2828","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Foundations for Cryptographic Reductions in CCSA Logics"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-3619-1232","authenticated-orcid":false,"given":"David","family":"Baelde","sequence":"first","affiliation":[{"name":"Univ Rennes, CNRS, IRISA, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5891-154X","authenticated-orcid":false,"given":"Adrien","family":"Koutsos","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2574-2256","authenticated-orcid":false,"given":"Justine","family":"Sauvage","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,12,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2013. CVE-2014-0160 aka. the Heartbleed bug. Available from MITRE. http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2014-0160"},{"key":"e_1_3_2_1_2_1","volume-title":"Th\u00e9o Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters.","author":"Abate Carmine","year":"2021","unstructured":"Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Th\u00e9o Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters. 2021. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. In CSF. IEEE, 1--15."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813707"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2012.08.007"},{"key":"e_1_3_2_1_5_1","volume-title":"An Interactive Prover for Protocol Verification in the Computational Model. In 42nd IEEE Symposium on Security and Privacy, SP 2021","author":"Baelde David","year":"2021","unstructured":"David Baelde, St\u00e9phanie Delaune, Charlie Jacomme, Adrien Koutsos, and Sol\u00e8ne Moreau. 2021. An Interactive Prover for Protocol Verification in the Computational Model. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24--27 May 2021. IEEE, 537--554."},{"volume-title":"Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant","author":"Baelde David","key":"e_1_3_2_1_6_1","unstructured":"David Baelde, St\u00e9phanie Delaune, Adrien Koutsos, and Sol\u00e8ne Moreau. 2022. Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant. In CSF. IEEE, 289--304."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF61375.2024.00046"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175781"},{"key":"e_1_3_2_1_9_1","volume-title":"Foundations for Cryptographic Reductions in CCSA Logics. (March","author":"Baelde David","year":"2024","unstructured":"David Baelde, Adrien Koutsos, and Justine Sauvage. 2024. Foundations for Cryptographic Reductions in CCSA Logics. (March 2024). https:\/\/hal.science\/hal-04511718 long version."},{"volume-title":"ESORICS (2) (Lecture Notes in Computer Science","author":"Bana Gergei","key":"e_1_3_2_1_10_1","unstructured":"Gergei Bana, Rohit Chadha, and Ajay Kumar Eeralla. 2018. Formal Analysis of Vote Privacy Using Computationally Complete Symbolic Attacker. In ESORICS (2) (Lecture Notes in Computer Science, Vol. 11099). Springer, 350--372."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660276"},{"key":"e_1_3_2_1_12_1","volume-title":"SoK: Computer-Aided Cryptography. In 2021 IEEE Symposium on Security and Privacy (SP). 777--795","author":"Barbosa Manuel","year":"2021","unstructured":"Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In 2021 IEEE Symposium on Security and Privacy (SP). 777--795."},{"key":"e_1_3_2_1_13_1","volume-title":"Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Yassine Lakhnech, Benedikt Schmidt, and Santiago Zanella B\u00e9guelin.","author":"Barthe Gilles","year":"2013","unstructured":"Gilles Barthe, Juan Manuel Crespo, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Yassine Lakhnech, Benedikt Schmidt, and Santiago Zanella B\u00e9guelin. 2013. Fully automated analysis of padding-based encryption in the computational model. In CCS. ACM, 1247--1260."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-ifs.2015.0429"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF61375.2024.00019"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77649"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.006"},{"volume-title":"Formal Computational Unlinkability Proofs of RFID Protocols","author":"Comon Hubert","key":"e_1_3_2_1_23_1","unstructured":"Hubert Comon and Adrien Koutsos. 2017. Formal Computational Unlinkability Proofs of RFID Protocols. In CSF. IEEE Computer Society, 100--114."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_6"},{"volume-title":"Constraint Solving and Insecurity Decision in Presence of Exclusive or","author":"Comon-Lundh Hubert","key":"e_1_3_2_1_25_1","unstructured":"Hubert Comon-Lundh and Vitaly Shmatikov. 2003. Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or. In LICS. IEEE Computer Society, 271."},{"volume-title":"A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols","author":"Cremers Cas","key":"e_1_3_2_1_26_1","unstructured":"Cas Cremers, Caroline Fontaine, and Charlie Jacomme. 2022. A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols. In SP. IEEE, 125--141."},{"key":"e_1_3_2_1_27_1","unstructured":"The Squirrel development team. 2024. The Squirrel Prover repository. https:\/\/github.com\/squirrel-prover\/squirrel-prover\/."},{"key":"e_1_3_2_1_28_1","volume-title":"Reps","author":"Feng Yu","year":"2017","unstructured":"Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. 2017. Component-based synthesis for complex APIs. In POPL. ACM, 599--612."},{"volume-title":"2023 2023 IEEE Symposium on Security and Privacy (SP) (SP). IEEE Computer Society","author":"Gancher J.","key":"e_1_3_2_1_29_1","unstructured":"J. Gancher, S. Gibson, P. Singh, S. Dharanikota, and B. Parno. 2023. OWL: Compositional Verification of Security Protocols via an Information-Flow Type System. In 2023 2023 IEEE Symposium on Security and Privacy (SP) (SP). IEEE Computer Society, Los Alamitos, CA, USA, 1130--1147."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani Susmit Jha Ashish Tiwari and Ramarathnam Venkatesan. 2011. Synthesis of loop-free programs. In PLDI. ACM 62--73.","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_1_31_1","volume-title":"Malozemoff","author":"Hoang Viet Tung","year":"2015","unstructured":"Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff. 2015. Automated Analysis and Synthesis of Authenticated Encryption Schemes. In CCS. ACM, 84--95."},{"key":"e_1_3_2_1_32_1","volume-title":"CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In 2024 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society","author":"Jeanteur Simon","year":"2024","unstructured":"Simon Jeanteur, Laura Kov\u00e1cs, Matteo Maffei, and Michael Rawson. 2024. CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In 2024 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, Los Alamitos, CA, USA, 259--259."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Susmit Jha Sumit Gulwani Sanjit A. Seshia and Ashish Tiwari. 2010. Oracle-guided component-based program synthesis. In ICSE (1). ACM 215--224.","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"volume-title":"EuroS&P","author":"Koutsos Adrien","key":"e_1_3_2_1_35_1","unstructured":"Adrien Koutsos. 2019. The 5G-AKA Authentication Protocol Privacy. In EuroS&P. IEEE, 464--479."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Lowe Gavin","key":"e_1_3_2_1_37_1","unstructured":"Gavin Lowe. 1996. Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 147--166."},{"key":"e_1_3_2_1_38_1","volume-title":"Green","author":"Malozemoff Alex J.","year":"2014","unstructured":"Alex J. Malozemoff, Jonathan Katz, and Matthew D. Green. 2014. Automated Analysis and Synthesis of Block-Cipher Modes of Operation. In CSF. IEEE Computer Society, 140--152."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Daniel Perelman Sumit Gulwani Dan Grossman and Peter Provost. 2014. Test-driven synthesis. In PLDI. ACM 408--418.","DOI":"10.1145\/2594291.2594297"},{"volume-title":"Symposium on. IEEE Computer Society","author":"Rusinowitch M.","key":"e_1_3_2_1_40_1","unstructured":"M. Rusinowitch, R. K\u00fcsters, M. Turuani, and Y. Chevalier. 2003. An NP Decision Procedure for Protocol Insecurity with XOR. In Logic in Computer Science, Symposium on. IEEE Computer Society, Los Alamitos, CA, USA, 261."},{"volume-title":"Computational Security","author":"Scerri Guillaume","key":"e_1_3_2_1_41_1","unstructured":"Guillaume Scerri and Ryan Stanley-Oakes. 2016. Analysis of Key Wrapping APIs: Generic Policies, Computational Security. In CSF. IEEE Computer Society, 281--295."},{"key":"e_1_3_2_1_42_1","unstructured":"Victor Shoup. 2004. Sequences of games: a tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch. (2004) 332."}],"event":{"name":"CCS '24: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Salt Lake City UT USA","acronym":"CCS '24"},"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.3690193","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3690193","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:53:21Z","timestamp":1755842001000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690193"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":42,"alternative-id":["10.1145\/3658644.3690193","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3690193","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"}}]}}