{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T13:23:33Z","timestamp":1774272213556,"version":"3.50.1"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319303024","type":"print"},{"value":"9783319303031","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30303-1_9","type":"book-chapter","created":{"date-parts":[[2016,2,24]],"date-time":"2016-02-24T10:41:07Z","timestamp":1456310467000},"page":"137-155","source":"Crossref","is-referenced-by-count":12,"title":["Performance Evaluations of Cryptographic Protocols Verification Tools Dealing with Algebraic Properties"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Lafourcade","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maxime","family":"Puys","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,2,25]]},"reference":[{"key":"9_CR1","unstructured":"IEEE 802.11 Local Metropolitan Area Networks: Wireless LAN Medium Acess Control (MAC) and Physical (PHY) Specifications (1999)"},{"key":"9_CR2","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":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/3-540-45657-0_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2002","unstructured":"Armando, A., Basin, D., Bouallagui, M., Chevalier, Y., Compagna, L., M\u00f6dersheim, S., Rusinowitch, M., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISS security protocol analysis tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 349\u2013353. Springer, Heidelberg (2002)"},{"issue":"1","key":"9_CR4","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/j.entcs.2004.05.021","volume":"125","author":"Alessandro Armando","year":"2005","unstructured":"Armando, A., Compagna, L.: An optimized intruder model for SAT-based model-checking of security protocols. In: Armando, A., Vigan\u00f2, L. (eds.) ENTCS, vol. 125, pp. 91\u2013108. Elsevier Science Publishers, March 2005","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"4","key":"9_CR5","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1109\/49.839937","volume":"18","author":"G Ateniese","year":"2000","unstructured":"Ateniese, G., Steiner, M., Tsudik, G.: New multiparty authentication services and key agreement protocols. IEEE J. Sel. Areas Commun. 18(4), 628\u2013639 (2000)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"9_CR6","volume-title":"A Classical Introduction to Cryptography Exercise Book","author":"T Baigneres","year":"2010","unstructured":"Baigneres, T., Junod, P., Lu, Y., Monnerat, J., Vaudenay, S.: A Classical Introduction to Cryptography Exercise Book, 1st edn. Springer Publishing Company, Berlin (2010). Incorporated","edition":"1"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-39650-5_15","volume-title":"Computer Security \u2013 ESORICS 2003","author":"D Basin","year":"2003","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: An on-the-fly model-checker for security protocol analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253\u2013270. Springer, Heidelberg (2003)"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"DA Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181\u2013208 (2005)","journal-title":"Int. J. Inf. Secur."},{"issue":"3","key":"9_CR9","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1080\/01611194.2011.583711","volume":"35","author":"Steven M. Bellovin","year":"2011","unstructured":"Bellovin, S.M., Miller, F.: Inventor of the one-time pad. Cryptologia 35(3), 203\u2013222 (2011). An earlier version is available as technical report CUCS-009-11","journal-title":"Cryptologia"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of CSFW 2001, pp. 82\u201396. IEEE Computer Society Press (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"9_CR11","unstructured":"Blanchet, B.: Cryptographic Protocol Verifier User Manual (2004)"},{"key":"9_CR12","unstructured":"Boichut, Y., H\u00e9am, P.-C., Kouchnarenko, O.: TA4SP, 2004. Produit logiciel. TA4SP est un outil de validation de protocoles de s\u00e9curit\u00e9. Gr\u00e2ce \u00e0 une technique d\u2019approximation appliqu\u00e9e sur le probl\u00e8me d\u2019atteignabilit\u00e9 en r\u00e9\u00e9criture, TA4SP peut prouver qu\u2019une propri\u00e9t\u00e9 de secret est inviol\u00e9e pour un nombre de sessions non-born\u00e9 en sur-approximant la connaissance atteignable de l\u2019intrus. L\u2019outil peut \u00e9galement montrer qu\u2019une propri\u00e9t\u00e9 est viol\u00e9e en sous-approximant la connaissance de l\u2019intrus. Une d\u00e9mo de l\u2019outil est disponible \u00e0 l\u2019adresse : http:\/\/lifc.univ-fcomte.fr\/~boichut\/outil\/ta4sp.php"},{"key":"9_CR13","unstructured":"Boichut, Y., H\u00e9am, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Proceedings of AVIS 2004, April 2004"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Boreale, M., Buscemi, M.G.: Experimenting with sta, a tool for automatic analysis of security protocols. In: Proceedings of the ACM Symposium on Applied Computing, SAC 2002, pp. 281\u2013285. New York, NY, USA, ACM (2002)","DOI":"10.1145\/508791.508847"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/3-540-48285-7_20","volume-title":"Advances in Cryptology - EUROCRYPT 1993","author":"C Boyd","year":"1994","unstructured":"Boyd, C., Mao, W.: On a limitation of BAN logic. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 240\u2013247. Springer, Heidelberg (1994)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-45069-6_23","volume-title":"Computer Aided Verification","author":"L Bozga","year":"2003","unstructured":"Bozga, L., Lakhnech, Y., P\u00e9rin, M.: HERMES: an automatic tool for verification of secrecy in security protocols. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 219\u2013222. Springer, Heidelberg (2003)"},{"key":"9_CR17","unstructured":"Bull, J., Otway, D.J.: The authentication protocol. Technical report DRA\/CIS3\/PROJ\/CORBA\/SC\/1\/CSM\/436-04\/03, Defence Research Agency (1997)"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8, 18\u201336 (1990)","journal-title":"ACM Trans. Comput. Syst."},{"key":"9_CR19","unstructured":"Cervesato, I.: The dolev-yao intruder is the most powerful attacker. In: Proceedings of the Sixteenth Annual Symposium on Logic in Computer Science \u2014 LICS 2001, pp. 16\u201319. IEEE Computer Society Press, Short (2001)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Cheminod, M., Bertolotti, I.C., Durante, L., Sisto, R., Valenzano, A.: Experimental comparison of automatic tools for the formal analysis of cryptographic protocols. In: DepCoS-RELCOMEX 2007, pp. 153\u2013160, Szklarska Poreba, Poland. IEEE Computer Society, 14\u201316 June 2007","DOI":"10.1109\/DEPCOS-RELCOMEX.2007.24"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-10373-5_6","volume-title":"Formal Methods and Software Engineering","author":"X Chen","year":"2009","unstructured":"Chen, X., van Deursen, T., Pang, J.: Improving automatic verification of security protocols with XOR. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 107\u2013126. Springer, Heidelberg (2009)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-45789-5_24","volume-title":"Static Analysis","author":"R Corin","year":"2002","unstructured":"Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, p. 326. Springer, Heidelberg (2002)"},{"issue":"1","key":"9_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-2006-14101","volume":"14","author":"V Cortier","year":"2006","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1\u201343 (2006)","journal-title":"J. Comput. Secur."},{"key":"9_CR24","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":"CJF 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. 5123, pp. 414\u2013418. Springer, Heidelberg (2008)"},{"key":"9_CR25","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. 6879, pp. 315\u2013334. Springer, Heidelberg (2011)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-02002-5_5","volume-title":"Formal to Practical Security","author":"CJF Cremers","year":"2009","unstructured":"Cremers, C.J.F., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic security protocol analysis. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds.) Formal to Practical Security. LNCS, vol. 5458, pp. 70\u201394. Springer, Heidelberg (2009)"},{"issue":"10","key":"9_CR27","doi-asserted-by":"publisher","first-page":"779","DOI":"10.4236\/ijcns.2010.310104","volume":"3","author":"N Dalal","year":"2010","unstructured":"Dalal, N., Shah, J., Hisaria, K., Jinwala, D.: A comparative analysis of tools for verification of security protocols. IJCNS 3(10), 779\u2013787 (2010)","journal-title":"IJCNS"},{"issue":"6","key":"9_CR28","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Trans. Inf. Soc. 22(6), 644\u2013654 (1976)","journal-title":"IEEE Trans. Inf. Soc."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of the 22Nd Annual Symposium on Foundations of Computer Science, SFCS 1981, pp. 350\u2013357, Washington, DC, USA. IEEE Computer Society (1981)","DOI":"10.1109\/SFCS.1981.32"},{"issue":"2","key":"9_CR30","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1145\/941566.941570","volume":"12","author":"L Durante","year":"2003","unstructured":"Durante, L., Sisto, R., Valenzano, A.: Automatic testing equivalence verification of spi calculus specifications. ACM Trans. Softw. Eng. Methodol. 12(2), 222\u2013284 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9_CR31","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S1571-0661(04)00034-9","volume":"4","author":"M Clavel","year":"1996","unstructured":"Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of maude. Electron. Notes Theoret. Comput. Sci. 4, 65\u201389 (1996)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"9_CR32","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 V","author":"S Escobar","year":"2007","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. 5705, pp. 1\u201350. Springer, Heidelberg (2007)"},{"issue":"5","key":"9_CR33","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/74681.74682","volume":"19","author":"L Gong","year":"1989","unstructured":"Gong, L.: Using one-way functions for authentication. SIGCOMM Comput. Commun. 19(5), 8\u201311 (1989)","journal-title":"SIGCOMM Comput. Commun."},{"key":"9_CR34","first-page":"1487","volume":"174","author":"L Horng-Twu","year":"2008","unstructured":"Horng-Twu, L., Wen-Shenq, J., Chi-Kai, L.: An electronic online bidding auction protocol with both security and efficiency. Appl. Math. Comput. 174, 1487\u20131497 (2008)","journal-title":"Appl. Math. Comput."},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Hussain, M., Seret, D.: A comparative study of security protocols validation tools: HERMES vs. AVISPA. In: Proceedings of ICACT 2006, vol. 1, pp. 303\u2013308 (2006)","DOI":"10.1109\/ICACT.2006.205974"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Kaufman, C.: Internet key exchange protocol version 2 (IKEv2). IETF RFC 4306, December 2005","DOI":"10.17487\/rfc4306"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Kaufman, C., Hoffman, P., Nir, Y., Eronen, P., Kivinen, T.: Internet key exchange protocol version 2 (IKEv2). IETF RFC 7296, October 2014","DOI":"10.17487\/rfc7296"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the horn theory based approach. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conference on Computer and Communications Security, pp. 129\u2013138. ACM (2008)","DOI":"10.1145\/1455770.1455788"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: Proceedings of the 22nd Computer Security Foundations Symposium (CSF), pp. 157\u2013171. IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.17"},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-12459-4_13","volume-title":"Formal Aspects in Security and Trust","author":"P Lafourcade","year":"2010","unstructured":"Lafourcade, P., Terrade, V., Vigier, S.: Comparison of cryptographic verification tools dealing with algebraic properties. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 173\u2013185. Springer, Heidelberg (2010)"},{"key":"9_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"1\u20132","key":"9_CR42","doi-asserted-by":"crossref","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\u20132), 53\u201384 (1998)","journal-title":"J. Comput. Secur."},{"issue":"10","key":"9_CR43","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G Lowe","year":"1997","unstructured":"Lowe, G., Roscoe, A.W.: Using CSP to detect errors in the TMN protocol. IEEE Trans. Softw. Eng. 23(10), 659\u2013669 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"10","key":"9_CR44","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G Lowe","year":"1997","unstructured":"Lowe, G., Roscoe, B.: Using CSP to detect errors in the TMN protocol. IEEE Trans. Softw. Eng. 23(10), 659\u2013669 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-61770-1_46","volume-title":"Computer Security - ESORICS 96","author":"CA Meadows","year":"1996","unstructured":"Meadows, C.A.: Analyzing the Needham-Schroeder public key protocol: a comparison of two approaches. In: Martella, G., Kurth, H., Montolivo, E., Bertino, Elisa (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 351\u2013364. Springer, Heidelberg (1996)"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Language generation and verification in the NRL protocol analyzer. In: Proceedings of CSFW 1996, pp. 48\u201362. IEEE Computer Society Press (1996)","DOI":"10.21236\/ADA465477"},{"key":"9_CR47","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":"9_CR48","unstructured":"Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: IEEE Symposium on Security and Privacy, May 1997"},{"issue":"12","key":"9_CR49","first-page":"993","volume":"21","author":"R Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. IEEE Trans. Softw. Eng. 21(12), 993\u2013999 (1978)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR50","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-14478-3_16","volume-title":"Recent Trends in Network Security and Applications","author":"R Patel","year":"2010","unstructured":"Patel, R., Borisaniya, B., Patel, A., Patel, D., Rajarajan, M., Zisman, A.: Comparative analysis of formal model checking tools for security protocol verification. In: Meghanathan, N., Boumerdassi, S., Chaki, N., Nagamalai, D. (eds.) CNSA 2010. CCIS, vol. 89, pp. 152\u2013163. Springer, Heidelberg (2010)"},{"key":"9_CR51","unstructured":"Puys, M., Lafourcade, P.: Protocol tool comparison test archive. http:\/\/www-verimag.imag.fr\/~puys\/assets\/files\/LP15_sources.tar.gz"},{"key":"9_CR52","volume-title":"Model-Checking CSP","author":"AW Roscoe","year":"1994","unstructured":"Roscoe, A.W.: Model-Checking CSP. Prentice Hall, Upper Saddle River (1994)"},{"key":"9_CR53","unstructured":"Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: IEEE Symposium on Foundations of Secure Systems (1995)"},{"issue":"1","key":"9_CR54","first-page":"7","volume":"65","author":"PYA Ryan","year":"1998","unstructured":"Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol. a cautionary tale. IEEE Trans. Softw. Eng. 65(1), 7\u201310 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR55","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), 2012 IEEE 25th, pp. 78\u201394, June 2012"},{"key":"9_CR56","volume-title":"Applied Cryptography","author":"B Schneier","year":"1996","unstructured":"Schneier, B.: Applied Cryptography, 2nd edn. Wiley, Hoboken (1996)","edition":"2"},{"issue":"1\/2","key":"9_CR57","first-page":"47","volume":"9","author":"D Song","year":"2001","unstructured":"Song, D., Berezin, S., Perrig, A.: Athena: a novel approach to efficient automatic security protocol analysis. IEEE Trans. Softw. Eng. 9(1\/2), 47\u201374 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/0-387-34805-0_30","volume-title":"Advances in Cryptology - CRYPTO \u201989","author":"M Tatebayashi","year":"1990","unstructured":"Tatebayashi, M., Matsuzaki, N., Newman Jr., D.B.: Key distribution protocol for digital mobile communication systems. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 324\u2013334. Springer, Heidelberg (1990)"},{"key":"9_CR59","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. 4098, pp. 277\u2013286. Springer, Heidelberg (2006)"},{"key":"9_CR60","volume-title":"A Classical Introduction to Cryptography: Applications for Communications Security","author":"S Vaudenay","year":"2005","unstructured":"Vaudenay, S.: A Classical Introduction to Cryptography: Applications for Communications Security. Springer-Verlag New York, Inc., Secaucus, NJ, USA (2005). ISBN: 0387254641, 9780387254647"},{"key":"9_CR61","first-page":"61","volume":"155","author":"L Vigan\u00f2","year":"2006","unstructured":"Vigan\u00f2, L.: Automated security protocol analysis with the AVISPA tool. ENTCS 155, 61\u201386 (2006)","journal-title":"ENTCS"},{"key":"9_CR62","doi-asserted-by":"crossref","unstructured":"Ylonen, T., Lonvick, C.: The secure shell (SSH) transport layer protocol. IETF RFC 4253, January 2006","DOI":"10.17487\/rfc4253"}],"container-title":["Lecture Notes in Computer Science","Foundations and Practice of Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30303-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T14:01:40Z","timestamp":1748786500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30303-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319303024","9783319303031"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30303-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}