{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T22:04:12Z","timestamp":1755036252879,"version":"3.37.3"},"reference-count":26,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"funder":[{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1109\/csf54842.2022.9919665","type":"proceedings-article","created":{"date-parts":[[2022,11,4]],"date-time":"2022-11-04T01:29:20Z","timestamp":1667525360000},"page":"289-304","source":"Crossref","is-referenced-by-count":7,"title":["Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant"],"prefix":"10.1109","author":[{"given":"David","family":"Baelde","sequence":"first","affiliation":[{"name":"Univ Rennes, CNRS, IRISA,France"}]},{"given":"St\u00e9phanie","family":"Delaune","sequence":"additional","affiliation":[{"name":"Univ Rennes, CNRS, IRISA,France"}]},{"given":"Adrien","family":"Koutsos","sequence":"additional","affiliation":[{"name":"Inria Paris,France"}]},{"given":"Sol\u00e8ne","family":"Moreau","sequence":"additional","affiliation":[{"name":"Univ Rennes, CNRS, IRISA,France"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9187-9"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00032"},{"key":"ref14","first-page":"281","article-title":"The AVISPA tool for the automated validation of internet security protocols and applications","author":"armando","year":"2005","journal-title":"CAV"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"ref10","first-page":"71","article-title":"Computer-aided security proofs for the working cryptographer","volume":"6841","author":"barthe","year":"2011","journal-title":"Crypto"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813707"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2012.08.007"},{"key":"ref17","first-page":"609","article-title":"A computationally complete symbolic attacker for equivalence properties","author":"bana","year":"2014","journal-title":"CCS"},{"journal-title":"The Squirrel Prover repository","year":"0","key":"ref16"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38004-4_17"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00078"},{"key":"ref24","first-page":"310","article-title":"Attacks on RFID protocols","volume":"2008","author":"van deursen","year":"2008","journal-title":"IACR Cryptol ePrint Arch"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6503"},{"journal-title":"Foundations for analyzing security APIs in the symbolic and computational model (fondations d'analyse de APIs de sécurité dans le modèle symbolique et calculatoire)","year":"2014","author":"k\u00fcnnemann","key":"ref26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919665"},{"key":"ref22","article-title":"Cryptographic approach to “privacy-friendly” tags","volume":"82","author":"ohkubo","year":"2003","journal-title":"RFID Privacy Workshop"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_11"},{"key":"ref8","article-title":"DY*: a modular symbolic verification framework for executable cryptographic protocol code","author":"bhargavan","year":"0","journal-title":"EuroS&P 2021–6th IEEE European Symposium on Security and Privacy"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_4"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"ref4","first-page":"696","article-title":"The TAMARIN prover for the symbolic analysis of security protocols","volume":"8044","author":"meier","year":"2013","journal-title":"CAV"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2926715"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1561\/9781680832075"}],"event":{"name":"2022 IEEE 35th Computer Security Foundations Symposium (CSF)","start":{"date-parts":[[2022,8,7]]},"location":"Haifa, Israel","end":{"date-parts":[[2022,8,10]]}},"container-title":["2022 IEEE 35th Computer Security Foundations Symposium (CSF)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9919409\/9919636\/09919665.pdf?arnumber=9919665","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T23:21:10Z","timestamp":1699485670000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9919665\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/csf54842.2022.9919665","relation":{},"subject":[],"published":{"date-parts":[[2022,8]]}}}