{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:28:39Z","timestamp":1747888119287,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466650"},{"type":"electronic","value":"9783662466667"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46666-7_11","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T22:57:12Z","timestamp":1427756232000},"page":"196-215","source":"Crossref","is-referenced-by-count":3,"title":["Abstractions for Security Protocol Verification"],"prefix":"10.1007","author":[{"given":"Binh Thanh","family":"Nguyen","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Armando","year":"2012","unstructured":"Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Erzse, G., Frau, S., Minea, M., M\u00f6dersheim, S., von Oheimb, D., Pellegrino, G., Ponta, S.E., Rocchetto, M., Rusinowitch, M., Torabi Dashti, M., Turuani, M., Vigan\u00f2, L.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 267\u2013282. Springer, Heidelberg (2012)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-540-77050-3_31","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"M. Arapinis","year":"2007","unstructured":"Arapinis, M., Duflot, M.: Bounding messages for free in security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 376\u2013387. Springer, Heidelberg (2007)"},{"key":"11_CR3","unstructured":"Arkko, J., Haverinen, H.: RFC 4187: Extensible authentication protocol method for 3rd generation authentication and key agreement (EAP-AKA) (2006), http:\/\/www.ietf.org\/rfc\/rfc4187"},{"issue":"1","key":"11_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10207-007-0041-y","volume":"7","author":"A. Armando","year":"2008","unstructured":"Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. International Journal of Information Security\u00a07(1), 3\u201332 (2008)","journal-title":"International Journal of Information Security"},{"issue":"3","key":"11_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D.A. Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f3, L.: OFMC: A symbolic model checker for security protocols. Int. J. Inf. Sec.\u00a04(3), 181\u2013208 (2005)","journal-title":"Int. J. Inf. Sec."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR8","unstructured":"Cremers, C.: IKEv1 and IKEv2 protocol suites (2011), https:\/\/github.com\/cascremers\/scyther\/tree\/master\/gui\/Protocols\/IKE"},{"key":"11_CR9","unstructured":"Cremers, C.: ISO\/IEC 9798 authentication protocols (2012), https:\/\/github.com\/cascremers\/scyther\/tree\/master\/gui\/Protocols\/ISO-9798"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","volume-title":"Computer Aided Verification","author":"C.J.F. Cremers","year":"2008","unstructured":"Cremers, C.J.F.: The Scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 414\u2013418. Springer, Heidelberg (2008)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-23822-2_18","volume-title":"Computer Security \u2013 ESORICS 2011","author":"C. Cremers","year":"2011","unstructured":"Cremers, C.: Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol.\u00a06879, pp. 315\u2013334. Springer, Heidelberg (2011)"},{"key":"11_CR12","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Abstraction and refinement in protocol derivation. In: Proc. 17th IEEE Computer Security Foundations Workshop (CSFW) (2004)"},{"key":"11_CR13","doi-asserted-by":"crossref","first-page":"423","DOI":"10.3233\/JCS-2005-13304","volume":"13","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security\u00a013, 423\u2013482 (2005)","journal-title":"Journal of Computer Security"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol.\u00a05705, pp. 1\u201350. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-03459-6_8","volume-title":"Foundations and Applications of Security Analysis","author":"J.D. Guttman","year":"2009","unstructured":"Guttman, J.D.: Transformations between cryptographic protocols. In: Degano, P., Vigan\u00f2, L. (eds.) ARSPA-WITS 2009. LNCS, vol.\u00a05511, pp. 107\u2013123. Springer, Heidelberg (2009)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-27375-9_8","volume-title":"Theory of Security and Applications","author":"J.D. Guttman","year":"2012","unstructured":"Guttman, J.D.: Security goals and protocol transformations. In: M\u00f6dersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol.\u00a06993, pp. 130\u2013147. Springer, Heidelberg (2012)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Harkins, D., Carrel, D.: The Internet Key Exchange (IKE) IETF RFC 2409 (Proposed Standard) (November 1998), http:\/\/www.ietf.org\/rfc\/rfc2409.txt","DOI":"10.17487\/rfc2409"},{"issue":"1\/2","key":"11_CR18","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/JCS-2001-91-202","volume":"9","author":"M.L. Hui","year":"2001","unstructured":"Hui, M.L., Lowe, G.: Fault-preserving simplifying transformations for security protocols. Journal of Computer Security\u00a09(1\/2), 3\u201346 (2001)","journal-title":"Journal of Computer Security"},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. Jouannaud","year":"1986","unstructured":"Jouannaud, J., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput.\u00a015(4), 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Kaufman, C., Hoffman, P., Nir, Y., Eronen, P.: Internet Key Exchange Protocol Version 2 (IKEv2). IETF RFC 5996 (September 2010), http:\/\/tools.ietf.org\/html\/rfc5996","DOI":"10.17487\/rfc5996"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S. Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Nguyen, B.T., Sprenger, C.: Sound security protocol transformations. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol.\u00a07796, pp. 83\u2013104. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36830-1_5"},{"key":"11_CR23","unstructured":"Nguyen, B.T., Sprenger, C.: Abstractions for security protocol verification. Tech. rep. Department of Computer Science, ETH Zurich (January 2015), http:\/\/dx.doi.org\/10.3929\/ethz-a-010347780"},{"key":"11_CR24","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. Paulson","year":"1998","unstructured":"Paulson, L.: The inductive approach to verifying cryptographic protocols. J. Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"J. Computer Security"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/11863908_24","volume-title":"Computer Security \u2013 ESORICS 2006","author":"D. Pavlovic","year":"2006","unstructured":"Pavlovic, D., Meadows, C.: Deriving secrecy in key establishment protocols. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 384\u2013403. Springer, Heidelberg (2006)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M. Turuani","year":"2006","unstructured":"Turuani, M.: The CL-atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 277\u2013286. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46666-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:25:47Z","timestamp":1747855547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46666-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466650","9783662466667"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46666-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}