{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,22]],"date-time":"2026-07-22T16:16:17Z","timestamp":1784736977594,"version":"3.55.0"},"reference-count":47,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,5]]},"DOI":"10.1109\/sp.2018.00033","type":"proceedings-article","created":{"date-parts":[[2018,7,26]],"date-time":"2018-07-26T22:05:11Z","timestamp":1532642711000},"page":"529-546","source":"Crossref","is-referenced-by-count":59,"title":["DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice"],"prefix":"10.1109","author":[{"given":"Vincent","family":"Cheval","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Itsaka","family":"Rakotonirina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.40"},{"key":"ref33","first-page":"414","article-title":"The scyther tool: Verification, falsification, and analysis of security protocols","volume":"5123","author":"cremers","year":"2008","journal-title":"Proc 20th International Conference on Computer Aided Verification (CAV'08)"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2012-0458"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133998"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.15"},{"key":"ref37","article-title":"PKI for machine readable travel documents offering ICC read-only access","author":"force","year":"2004","journal-title":"International Civil Aviation Organization Tech Rep"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2004-12203"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1981.32"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0340"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382221"},{"key":"ref40","author":"papadimitriou","year":"2003","journal-title":"Computational Complexity"},{"key":"ref11","first-page":"281","article-title":"The AVISPA tool for the automated validation of internet security protocols and applications","author":"armando","year":"2005","journal-title":"17th International Conference on Computer Aided Verification (CAV'05) Lecture Notes in Computer Science"},{"key":"ref12","first-page":"497","article-title":"Partial order reduction for security protocols","volume":"42","author":"baelde","year":"2015","journal-title":"26th Int Conf Concurrency Theory (CONCUR'15)"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813662"},{"key":"ref14","first-page":"16","article-title":"Deciding security of protocols against off-line guessing attacks","author":"baudet","year":"2005","journal-title":"12th Conference on Computer and Communications Security (CCS'05)"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.8"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.29"},{"key":"ref17","article-title":"Automatic Cryptographic Protocol Verifier","author":"blanchet","year":"2016","journal-title":"MINT Tutorial and User Manual"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00177-7"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2926715"},{"key":"ref28","first-page":"294","article-title":"The finite variant property: How to get rid of some algebraic properties","volume":"3467","author":"comon-lundh","year":"2005","journal-title":"16th International Conference on Rewriting Techniques and Applications (RTA '05)"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9197-7"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19751-2_3"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.12.023"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.15"},{"key":"ref7","first-page":"335","article-title":"Helios: web-based open-audit voting","author":"adida","year":"2008","journal-title":"Proc 17th Conference on Security Symposium (SS '08)"},{"key":"ref2","year":"2018","journal-title":"Deepsec technical report"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45741-3_13"},{"key":"ref1","year":"2018","journal-title":"Deepsec Deciding equivalence properties in security protocols"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.28"},{"key":"ref20","first-page":"587","article-title":"Apte: an algorithm for proving trace equivalence","volume":"8413","author":"cheval","year":"2014","journal-title":"20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)"},{"key":"ref45","first-page":"696","article-title":"The TAMARIN prover for the symbolic analysis of security protocols","volume":"8044","author":"schmidt","year":"2013","journal-title":"25th International Conference on Computer Aided Verification (CAV'13)"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046744"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_5"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/978-3-642-36830-1_12","article-title":"Proving more observational equivalences with Pro Verif","volume":"7796","author":"cheval","year":"2013","journal-title":"Proc 2nd Conference on Principles of Security and Trust (POST'13)"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00490-5"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9199-5"},{"key":"ref41","author":"ranne","year":"2016","journal-title":"Personal communication"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.04.016"},{"key":"ref44","first-page":"162","article-title":"A formal definition of protocol indistinguishability and its verification using Maude-NPA","volume":"8743","author":"santiago","year":"2014","journal-title":"10th International Workshop on Security and Trust Management STM'14"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2811262"},{"key":"ref43","first-page":"313","article-title":"Pret-a-voter with re-encryption mixes","volume":"4189","author":"ryan","year":"2006","journal-title":"Proc 11th European Symp Research in Computer Security (ESORICS)"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.19"}],"event":{"name":"2018 IEEE Symposium on Security and Privacy (SP)","location":"San Francisco, CA","start":{"date-parts":[[2018,5,20]]},"end":{"date-parts":[[2018,5,24]]}},"container-title":["2018 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx7\/8418581\/8418583\/08418623.pdf?arnumber=8418623","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T13:05:38Z","timestamp":1643202338000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/ieeexplore.ieee.org\/document\/8418623\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5]]},"references-count":47,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/sp.2018.00033","relation":{},"subject":[],"published":{"date-parts":[[2018,5]]}}}