{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T04:30:28Z","timestamp":1741753828223,"version":"3.38.0"},"reference-count":47,"publisher":"SAGE Publications","issue":"4","license":[{"start":{"date-parts":[[2018,6,6]],"date-time":"2018-06-06T00:00:00Z","timestamp":1528243200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2018,7,10]]},"abstract":"<jats:p> We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We propose abstractions that transform a term\u2019s structure based on its type as well as abstractions that remove atomic messages, variables, and redundant terms. Our theory improves on previous work by supporting rewrite theories with the finite-variant property, user-defined types, and untyped variables to cover type flaw attacks. We prove soundness results for an expressive property language that includes secrecy and authentication. Applying our abstractions to realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers. <\/jats:p>","DOI":"10.3233\/jcs-15769","type":"journal-article","created":{"date-parts":[[2018,6,8]],"date-time":"2018-06-08T15:14:25Z","timestamp":1528470865000},"page":"459-508","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":2,"title":["Abstractions for security protocol verification"],"prefix":"10.1177","volume":"26","author":[{"given":"Binh Thanh","family":"Nguyen","sequence":"first","affiliation":[{"name":"Institute of Networks and Security, Johannes Kepler University, Linz, Austria"}]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[{"name":"Institute of Information Security, Department of Computer Science, ETH Zurich, Switzerland"}]},{"given":"Cas","family":"Cremers","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, United Kingdom"}]}],"member":"179","published-online":{"date-parts":[[2018,6,6]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"O.\u00a0Almousa, S.A.\u00a0M\u00f6dersheim, P.\u00a0Modesti and L.\u00a0Vigan\u00f2, Typing and compositionality for security protocols: A generalization to the geometric fragment, in: ESORICS, Lecture Notes in Computer Science, Springer, 2015.","DOI":"10.1007\/978-3-319-24177-7_11"},{"key":"ref002","doi-asserted-by":"crossref","unstructured":"M.\u00a0Arapinis and M.\u00a0Duflot, Bounding messages for free in security protocols, in: FSTTCS, 2007, pp.\u00a0376\u2013387.","DOI":"10.1007\/978-3-540-77050-3_31"},{"key":"ref003","doi-asserted-by":"crossref","unstructured":"M.\u00a0Arapinis, E.\u00a0Ritter and M.D.\u00a0Ryan, StatVerif: Verification of stateful processes, in: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27\u201329 June, 2011, IEEE Computer Society, 2011, pp.\u00a033\u201347. doi:10.1109\/CSF.2011.10.","DOI":"10.1109\/CSF.2011.10"},{"key":"ref004","doi-asserted-by":"crossref","unstructured":"J.\u00a0Arkko and H.\u00a0Haverinen, RFC 4187: Extensible authentication protocol method for 3rd generation authentication and key agreement (EAP-AKA), 2006, http:\/\/www.ietf.org\/rfc\/rfc4187.","DOI":"10.17487\/rfc4187"},{"key":"ref005","doi-asserted-by":"crossref","unstructured":"A.\u00a0Armando, W.\u00a0Arsac, T.\u00a0Avanesov, M.\u00a0Barletta, A.\u00a0Calvi, A.\u00a0Cappai, R.\u00a0Carbone, Y.\u00a0Chevalier, L.\u00a0Compagna, J.\u00a0Cu\u00e9llar, G.\u00a0Erzse, S.\u00a0Frau, M.\u00a0Minea, S.\u00a0M\u00f6dersheim, D.\u00a0von Oheimb, G.\u00a0Pellegrino, S.E.\u00a0Ponta, M.\u00a0Rocchetto, M.\u00a0Rusinowitch, M.T.\u00a0Dashti, M.\u00a0Turuani and L.\u00a0Vigan\u00f2, The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures, in: TACAS, 2012, pp.\u00a0267\u2013282.","DOI":"10.1007\/978-3-642-28756-5_19"},{"key":"ref006","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0041-y"},{"key":"ref007","doi-asserted-by":"crossref","unstructured":"M.\u00a0Backes, A.\u00a0Cortesi, R.\u00a0Focardi and M.\u00a0Maffei, A calculus of challenges and responses, in: Proceedings of the 2007 ACM Workshop on Formal Methods in Security Engineering, FMSE \u201907, ACM, New York, NY, USA, 2007, pp.\u00a051\u201360. ISBN 978-1-59593-887-9. doi:10.1145\/1314436.1314444.","DOI":"10.1145\/1314436.1314444"},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"ref009","doi-asserted-by":"crossref","unstructured":"B.\u00a0Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), Cape Breton, Nova Scotia, Canada, 11\u201313 June 2001, IEEE Computer Seciety, 2001, pp.\u00a082\u201396. doi:10.1109\/CSFW.2001.930138.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref010","doi-asserted-by":"crossref","unstructured":"P.\u00a0Cousot and R.\u00a0Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: POPL, 1977, pp.\u00a0238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"ref011","unstructured":"C.\u00a0Cremers, IKEv1 and IKEv2 protocol suites, 2011, https:\/\/github.com\/cascremers\/scyther\/tree\/master\/gui\/Protocols\/IKE."},{"key":"ref012","unstructured":"C.\u00a0Cremers, ISO\/IEC 9798 authentication protocols, 2012, https:\/\/github.com\/cascremers\/scyther\/tree\/master\/gui\/Protocols\/ISO-9798."},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"C.\u00a0Cremers and S.\u00a0Mauw, Operational Semantics and Verification of Security Protocols, Information Security and Cryptography, Springer, 2012. ISBN 978-3-540-78636-8. doi:10.1007\/978-3-540-78636-8.","DOI":"10.1007\/978-3-540-78636-8"},{"key":"ref014","doi-asserted-by":"crossref","unstructured":"C.J.F.\u00a0Cremers, The Scyther tool: Verification, falsification, and analysis of security protocols, in: CAV, 2008, pp.\u00a0414\u2013418.","DOI":"10.1007\/978-3-540-70545-1_38"},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"C.J.F.\u00a0Cremers, Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2, in: ESORICS, 2011, pp.\u00a0315\u2013334.","DOI":"10.1007\/978-3-642-23822-2_18"},{"key":"ref016","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.034"},{"key":"ref017","unstructured":"A.\u00a0Datta, A.\u00a0Derek, J.C.\u00a0Mitchell and D.\u00a0Pavlovic, Abstraction and refinement in protocol derivation, in: Proc. 17th IEEE Computer Security Foundations Workshop (CSFW), 2004."},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2005-13304"},{"key":"ref019","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"ref020","doi-asserted-by":"crossref","unstructured":"F.\u00a0Dur\u00e1n and J.\u00a0Meseguer, A Church-Rosser checker tool for conditional order-sorted equational maude specifications, in: Rewriting Logic and Its Applications\u00a0\u2013 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers, Paphos, Cyprus, March 20\u201321, 2010, pp.\u00a069\u201385. doi:10.1007\/978-3-642-16310-4_6.","DOI":"10.1007\/978-3-642-16310-4_6"},{"key":"ref021","doi-asserted-by":"crossref","unstructured":"S.\u00a0Escobar, C.\u00a0Meadows and J.\u00a0Meseguer, Maude-NPA: Cryptographic protocol analysis modulo equational properties, in: FOSAD, 2007, pp.\u00a01\u201350.","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"ref022","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"ref023","doi-asserted-by":"crossref","unstructured":"J.\u00a0Giesl, P.\u00a0Schneider-Kamp and R.\u00a0Thiemann, Automatic termination proofs in the dependency pair framework, in: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Proceedings, Seattle, WA, USA, August 17\u201320, 2006, 2006, pp.\u00a0281\u2013286. doi:10.1007\/11814771_24.","DOI":"10.1007\/11814771_24"},{"key":"ref024","doi-asserted-by":"crossref","unstructured":"J.D.\u00a0Guttman, Transformations between cryptographic protocols, in: ARSPA-WITS, 2009, pp.\u00a0107\u2013123.","DOI":"10.1007\/978-3-642-03459-6_8"},{"key":"ref025","doi-asserted-by":"crossref","unstructured":"J.D.\u00a0Guttman, Security goals and protocol transformations, in: Theory of Security and Applications (TOSCA), an ETAPS Associated Event, LNCS, Vol.\u00a06993, Springer, 2011.","DOI":"10.1007\/978-3-642-27375-9_8"},{"key":"ref026","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140499"},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"D.\u00a0Harkins and D.\u00a0Carrel, The Internet key exchange (IKE), IETF RFC 2409 (proposed standard), 1998, Obsoleted by RFC 4306, updated by RFC 4109, http:\/\/www.ietf.org\/rfc\/rfc2409.txt.","DOI":"10.17487\/rfc2409"},{"key":"ref028","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2001-91-202"},{"key":"ref029","doi-asserted-by":"publisher","DOI":"10.1137\/0215084"},{"key":"ref030","doi-asserted-by":"crossref","unstructured":"C.\u00a0Kaufman, P.\u00a0Hoffman, Y.\u00a0Nir and P.\u00a0Eronen, Internet key exchange protocol version 2 (IKEv2), IETF RFC 5996, 2010, http:\/\/tools.ietf.org\/html\/rfc5996.","DOI":"10.17487\/rfc5996"},{"key":"ref031","doi-asserted-by":"crossref","unstructured":"J.\u00a0Lallemand, D.A.\u00a0Basin and C.\u00a0Sprenger, Refining authenticated key agreement with strong adversaries, in: 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26\u201328, 2017, pp.\u00a092\u2013107. doi:10.1109\/EuroSP.2017.22.","DOI":"10.1109\/EuroSP.2017.22"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"G.\u00a0Lowe, A hierarchy of authentication specifications, in: IEEE Computer Security Foundations Workshop, IEEE Computer Society, Los Alamitos, CA, USA, 1997, pp.\u00a031\u201343. doi:10.1109\/CSFW.1997.596782.","DOI":"10.1109\/CSFW.1997.596782"},{"key":"ref033","doi-asserted-by":"crossref","unstructured":"S.\u00a0Meier, C.J.F.\u00a0Cremers and D.A.\u00a0Basin, Strong invariants for the efficient construction of machine-checked protocol security proofs, in: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17\u201319, 2010, IEEE Computer Seciety, 2010, pp.\u00a0231\u2013245. doi:10.1109\/CSF.2010.23.","DOI":"10.1109\/CSF.2010.23"},{"key":"ref034","doi-asserted-by":"crossref","unstructured":"S.\u00a0Meier, B.\u00a0Schmidt, C.\u00a0Cremers and D.A.\u00a0Basin, The TAMARIN prover for the symbolic analysis of security protocols, in: CAV, 2013, pp.\u00a0696\u2013701.","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref035","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"ref036","unstructured":"B.T.\u00a0Nguyen, The Scyther-abstraction tool, 2018, https:\/\/github.com\/binhnguyen1984\/scyther-abstraction."},{"key":"ref037","doi-asserted-by":"crossref","unstructured":"B.T.\u00a0Nguyen and C.\u00a0Sprenger, Sound security protocol transformations, in: POST, 2013, pp.\u00a083\u2013104.","DOI":"10.1007\/978-3-642-36830-1_5"},{"key":"ref038","doi-asserted-by":"crossref","unstructured":"B.T.\u00a0Nguyen and C.\u00a0Sprenger, Abstractions for security protocol verification, in: Principles of Security and Trust\u00a0\u2013 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings, London, UK, April 11\u201318, 2015, R.\u00a0Focardi and A.C.\u00a0Myers, eds, Lecture Notes in Computer Science, Vol.\u00a09036, Springer, 2015, pp.\u00a0196\u2013215. doi:10.1007\/978-3-662-46666-7_11.","DOI":"10.1007\/978-3-662-46666-7_11"},{"key":"ref039","doi-asserted-by":"crossref","unstructured":"B.T.\u00a0Nguyen, C.\u00a0Sprenger and C.\u00a0Cremers, Abstractions for security protocol verification, Technical report, Department of Computer Science, ETH Zurich, 2018. doi:10.3929\/ethz-b-000266360.","DOI":"10.3233\/JCS-15769"},{"key":"ref040","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"ref041","doi-asserted-by":"crossref","unstructured":"D.\u00a0Pavlovic and C.\u00a0Meadows, Deriving secrecy in key establishment protocols, in: Proc. 11th European Symposium on Research in Computer Security (ESORICS), 2006, pp.\u00a0384\u2013403.","DOI":"10.1007\/11863908_24"},{"key":"ref042","doi-asserted-by":"crossref","unstructured":"A.\u00a0Perrig, J.D.\u00a0Tygar, D.\u00a0Song and R.\u00a0Canetti, Efficient authentication and signing of multicast streams over Lossy channels, in: Proceedings of the 2000 IEEE Symposium on Security and Privacy, SP \u201900, IEEE Computer Society, Washington, DC, USA, 2000, p.\u00a056. ISBN 0-7695-0665-8.","DOI":"10.1109\/SECPRI.2000.848446"},{"key":"ref043","doi-asserted-by":"crossref","unstructured":"S.\u00a0Schneider, Verifying authentication protocols with CSP, in: 10th Computer Security Foundations Workshop (CSFW \u201997), Rockport, Massachusetts, USA, June 10\u201312, 1997, 1997, pp.\u00a03\u201317. doi:10.1109\/CSFW.1997.596775.","DOI":"10.1109\/CSFW.1997.596775"},{"key":"ref044","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2008.10.001"},{"key":"ref045","doi-asserted-by":"crossref","unstructured":"C.\u00a0Sprenger and D.\u00a0Basin, Developing security protocols by refinement, in: Proc. 17th ACM Conference on Computer and Communications Security (CCS), 2010, pp.\u00a0361\u2013374. doi:10.1145\/1866307.1866349.","DOI":"10.1145\/1866307.1866349"},{"key":"ref046","doi-asserted-by":"crossref","unstructured":"C.\u00a0Sprenger and D.\u00a0Basin, Refining key establishment, in: Proc. 25th IEEE Computer Security Foundations Symposium (CSF), 2012, pp.\u00a0230\u2013246.","DOI":"10.1109\/CSF.2012.21"},{"key":"ref047","doi-asserted-by":"crossref","unstructured":"M.\u00a0Turuani, The CL-Atse protocol analyser, in: RTA, 2006, pp.\u00a0277\u2013286.","DOI":"10.1007\/11805618_21"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-15769","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-15769","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-15769","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T09:31:23Z","timestamp":1741685483000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-15769"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,6]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,7,10]]}},"alternative-id":["10.3233\/JCS-15769"],"URL":"https:\/\/doi.org\/10.3233\/jcs-15769","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"type":"print","value":"0926-227X"},{"type":"electronic","value":"1875-8924"}],"subject":[],"published":{"date-parts":[[2018,6,6]]}}}