{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:01:03Z","timestamp":1750309263183,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,1]],"date-time":"2024-04-01T00:00:00Z","timestamp":1711929600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2024,4]]},"abstract":"<jats:p>\n            Security protocols are widely used today to secure transactions that take place over public channels like the Internet. Common uses include the secure transfer of sensitive information such as credit card numbers, or user authentication on a system. Because of their presence in many widely used applications (\n            <jats:italic>e.g.<\/jats:italic>\n            electronic commerce, government-issued ID), developing methods and tools to verify security protocols has become an important research challenge. Such tools help increase our trust in protocols, and hence on the applications that rely on them.\n          <\/jats:p>","DOI":"10.1145\/3665453.3665461","type":"journal-article","created":{"date-parts":[[2024,5,16]],"date-time":"2024-05-16T17:55:27Z","timestamp":1715882127000},"page":"62-83","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["The Squirrel Prover and its Logic"],"prefix":"10.1145","volume":"11","author":[{"given":"David","family":"Baelde","sequence":"first","affiliation":[{"name":"Univ Rennes, CNRS, IRISA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phanie","family":"Delaune","sequence":"additional","affiliation":[{"name":"CNRS, Univ Rennes, IRISA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charlie","family":"Jacomme","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, LORIA, Inria Nancy Grand-Est"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrien","family":"Koutsos","sequence":"additional","affiliation":[{"name":"Inria Paris"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph","family":"Lallemand","sequence":"additional","affiliation":[{"name":"CNRS, Univ Rennes, IRISA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,5,16]]},"reference":[{"key":"e_1_2_1_1_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."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919665"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175781"},{"key":"e_1_2_1_4_1","volume-title":"Cryptographic Reductions By Bi-Deduction. (March","author":"Baelde David","year":"2024","unstructured":"David Baelde, Adrien Koutsos, and Justine Sauvage. 2024. Cryptographic Reductions By Bi-Deduction. (March 2024). https:\/\/hal.science\/hal-04511718"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_11"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660276"},{"key":"e_1_2_1_7_1","volume-title":"SoK: Computer-Aided Cryptography. In 42nd IEEE Symposium on Security and Privacy, SP 2021","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 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24--27 May 2021. IEEE, 777--795."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings (Lecture Notes in Computer Science), Phillip Rogaway (Ed.)","volume":"6841","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, Sylvain Heraud, and Santiago Zanella B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14--18, 2011. Proceedings (Lecture Notes in Computer Science), Phillip Rogaway (Ed.), Vol. 6841. Springer, 71--90."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"e_1_2_1_11_1","volume-title":"An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001","author":"Blanchet Bruno","year":"2001","unstructured":"Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11--13 June 2001, Cape Breton, Nova Scotia, Canada. IEEE Computer Society, 82--96."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_2_1_13_1","volume-title":"Formal Verification of Privacy for RFID Systems. In 23rd IEEE Computer Security Foundations Symposium, CSF 2010","author":"Brus\u00f2 Mayla","year":"2010","unstructured":"Mayla Brus\u00f2, Konstantinos Chatzikokolakis, and Jerry den Hartog. 2010. Formal Verification of Privacy for RFID Systems. In 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17--19, 2010. IEEE Computer Society, 75--88."},{"key":"e_1_2_1_14_1","volume-title":"Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets. In 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS","author":"Comon Hubert","year":"2020","unstructured":"Hubert Comon, Charlie Jacomme, and Guillaume Scerri. 2020. Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets. In 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS 2020. ACM, 1427--1444."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833800"},{"key":"e_1_2_1_16_1","volume-title":"22nd Annual Symposium on Foundations of Computer Science","author":"Dolev Danny","year":"1981","unstructured":"Danny Dolev and Andrew Chi-Chih Yao. 1981. On the Security of Public Key Protocols (Extended Abstract). In 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28--30 October 1981. IEEE Computer Society, 350--357."},{"key":"e_1_2_1_17_1","volume-title":"CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.)","volume":"8044","author":"Meier Simon","unstructured":"Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 696--701."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3665453.3665461","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3665453.3665461","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:57:12Z","timestamp":1750291032000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3665453.3665461"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["10.1145\/3665453.3665461"],"URL":"https:\/\/doi.org\/10.1145\/3665453.3665461","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2024,4]]},"assertion":[{"value":"2024-05-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}