{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:10:02Z","timestamp":1748581802560,"version":"3.41.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319231648"},{"type":"electronic","value":"9783319231655"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23165-5_7","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T03:57:43Z","timestamp":1440561463000},"page":"160-180","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Alice and Bob Meet Equational Theories"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[]},{"given":"Michel","family":"Keller","sequence":"additional","affiliation":[]},{"given":"Sa\u0161a","family":"Radomirovi\u0107","sequence":"additional","affiliation":[]},{"given":"Ralf","family":"Sasse","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He\u00e1m, P.C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"7_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"7_CR3","unstructured":"Basin, D., Keller, M., Radomirovi\u0107, S., Sasse, R.: Alice&Bob protocols. http:\/\/www.infsec.ethz.ch\/research\/software\/anb.html"},{"issue":"6","key":"7_CR4","doi-asserted-by":"publisher","first-page":"817","DOI":"10.3233\/JCS-130472","volume":"21","author":"D Basin","year":"2013","unstructured":"Basin, D., Cremers, C., Meier, S.: Provably repairing the ISO\/IEC 9798 standard for entity authentication. J. Comput. Secur. 21(6), 817\u2013846 (2013)","journal-title":"J. Comput. Secur."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Basin, D., Cremers, C., Kim, T.H.-J., Perrig, A., Sasse, R., Szalachowski, P.: ARPKI: attack resilient public-key infrastructure. In: Ahn, G.-J., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 3\u20137 November 2014, Scottsdale, AZ, USA, pp. 382\u2013393. ACM (2014)","DOI":"10.1145\/2660267.2660298"},{"key":"7_CR6","unstructured":"Blanchet, B.: Proverif automatic cryptographic protocol verifier user manual. CNRS, Departement d\u2019Informatique, Ecole Normale Superieure, Paris (2005)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundations Workshop (CSFW), pp. 82\u201396. IEEE (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"1","key":"7_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.06.007","volume":"135","author":"C Caleiro","year":"2005","unstructured":"Caleiro, C., Vigan\u00f2, L., Basin, D.: Deconstructing Alice and Bob. Electron. Notes Theoret. Comput. Sci. 135(1), 3\u201322 (2005). Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, ARSPA 2005","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"issue":"1\u20132","key":"7_CR9","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.tcs.2006.08.041","volume":"367","author":"C Caleiro","year":"2006","unstructured":"Caleiro, C., Vigan\u00f2, L., Basin, D.: On the semantics of Alice&Bob specifications of security protocols. Theor. Comput. Sci. 367(1\u20132), 88\u2013122 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"7_CR10","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.ipl.2009.11.004","volume":"110","author":"Y Chevalier","year":"2010","unstructured":"Chevalier, Y., Rusinowitch, M.: Compiling and securing cryptographic protocols. Inf. Process. Lett. 110(3), 116\u2013122 (2010)","journal-title":"Inf. Process. Lett."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Cremers, C.: Unbounded verification, falsification, and characterization of security protocols by pattern refinement. In: ACM Conference on Computer and Communications Security (CCS), pp. 119\u2013128. ACM (2008)","DOI":"10.1145\/1455770.1455787"},{"key":"7_CR14","unstructured":"Denker, G., Millen, J.K.: CAPSL intermediate language. In: Proceedings of FMSP 1999 (1999). http:\/\/www.csl.sri.com\/users\/millen\/capsl\/"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design","author":"S Escobar","year":"2007","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cyptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2007)"},{"issue":"7\u20138","key":"7_CR16","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Logic Algebraic Program. 81(7\u20138), 898\u2013928 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJT Fabrega","year":"1999","unstructured":"Fabrega, F.J.T., Herzog, J., Guttman, J.: Strand spaces: what makes a security protocol correct? J. Comput. Secur. 7, 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"7_CR18","unstructured":"Keller, M.: Converting Alice and Bob protocol specifications to Tamarin. Bachelor\u2019s thesis, ETH Zurich (2014). http:\/\/www.infsec.ethz.ch\/research\/software\/anb.html"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS, pp. 147\u2013166 (1996)","DOI":"10.1007\/3-540-61042-1_43"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Workshop on Computer Security Foundations, CSFW 1997, pp. 31\u201343, Washington, DC, USA. IEEE Computer Society (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"issue":"1","key":"7_CR21","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G Lowe","year":"1998","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1), 53\u201384 (1998)","journal-title":"J. Comput. Secur."},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-540-88313-5_34","volume-title":"Computer Security - ESORICS 2008","author":"J McCarthy","year":"2008","unstructured":"McCarthy, J., Krishnamurthi, S.: Cryptographic protocol explication and end-point projection. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 533\u2013547. Springer, Heidelberg (2008)"},{"key":"7_CR23","unstructured":"Meier, S.: GitHub repository of scyther-proof Project. https:\/\/github.com\/meiersi\/scyther-proof"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Meier, S., Cremers, C., Basin, D.: Strong invariants for the efficient construction of machine-checked protocol security proofs. In: CSF, pp. 231\u2013245. IEEE Computer Society (2010)","DOI":"10.1109\/CSF.2010.23"},{"key":"7_CR25","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.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S.: Algebraic properties in Alice and Bob notation. In: ARES, pp. 433\u2013440. IEEE Computer Society (2009)","DOI":"10.1109\/ARES.2009.95"},{"issue":"9","key":"7_CR27","first-page":"33","volume":"32","author":"BC Neuman","year":"1994","unstructured":"Neuman, B.C., Ts\u2019o, T.: Kerberos: an authentication service for computer networks. Communications 32(9), 33\u201338 (1994)","journal-title":"Communications"},{"key":"7_CR28","unstructured":"Schmidt, B.: Formal analysis of key exchange protocols and physical protocols. Ph.D. dissertation, ETH Zurich (2012)"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Computer Security Foundations Symposium (CSF), pp. 78\u201394. IEEE (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Sasse, R., Cremers, C., Basin, D.: Automated verification of group key agreement protocols. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, 18\u201321 May 2014, Berkeley, CA, USA, pp. 179\u2013194. IEEE Computer Society (2014)","DOI":"10.1109\/SP.2014.19"}],"container-title":["Lecture Notes in Computer Science","Logic, Rewriting, and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23165-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:39:57Z","timestamp":1748579997000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23165-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231648","9783319231655"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}