{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T16:18:32Z","timestamp":1772727512673,"version":"3.50.1"},"publisher-location":"Cham","reference-count":100,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_22","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"727-762","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":45,"title":["Model Checking Security Protocols"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cas","family":"Cremers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"1\u20132","key":"22_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1\u20132), 2\u201332 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR2","first-page":"104","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0104\u2013115. ACM, New York (2001)"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1016\/j.ic.2007.07.002","volume":"206","author":"S. Andova","year":"2008","unstructured":"Andova, S., Cremers, C., Gj\u00f8steen, K., Mauw, S., Mj\u00f8lsnes, S.F., Radomirovi\u0107, S.: A framework for compositional verification of security protocols. Inf. Comput. 206, 425\u2013459 (2008)","journal-title":"Inf. Comput."},{"key":"22_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Drielsma, P.H., H\u00e9am, 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.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03576, pp.\u00a0281\u2013285. Springer, Heidelberg (2005)"},{"key":"22_CR5","series-title":"LNCS","first-page":"730","volume-title":"Logics in Artificial Intelligence\u2014Journ\u00e9es Europ\u00e9ennes sur la Logique en Intelligence Artificielle (JELIA)","author":"A. Armando","year":"2004","unstructured":"Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Alferes, J.J., Leite, J.A. (eds.) Logics in Artificial Intelligence\u2014Journ\u00e9es Europ\u00e9ennes sur la Logique en Intelligence Artificielle (JELIA). LNCS, vol.\u00a03229, pp.\u00a0730\u2013733. Springer, Heidelberg (2004)"},{"issue":"1","key":"22_CR6","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. Int. J. Inf. Secur. 7(1), 3\u201332 (2008)","journal-title":"Int. J. Inf. Secur."},{"key":"22_CR7","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)"},{"issue":"2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. J.\u00a0Symb. Comput. 21(2), 211\u2013243 (1996)","journal-title":"J.\u00a0Symb. Comput."},{"key":"22_CR9","series-title":"LNCS","first-page":"178","volume-title":"European Conf. on Research in Computer Security (ESORICS)","author":"M. Backes","year":"2005","unstructured":"Backes, M., Pfitzmann, B.: Limits of the cryptographic realization of Dolev\u2013Yao-style XOR. In: di Vimercati, S.D.C., Syverson, P.F., Gollmann, D. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol.\u00a03679, pp.\u00a0178\u2013196. Springer, Heidelberg (2005)"},{"key":"22_CR10","series-title":"LNCS","first-page":"404","volume-title":"European Conf. on Research in Computer Security (ESORICS)","author":"M. Backes","year":"2006","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Limits of the BRSIM\/UC soundness of Dolev\u2013Yao models with hashes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol.\u00a04189, pp.\u00a0404\u2013423. Springer, Heidelberg (2006)"},{"issue":"12","key":"22_CR11","doi-asserted-by":"publisher","first-page":"1685","DOI":"10.1016\/j.ic.2007.05.002","volume":"205","author":"M. Backes","year":"2007","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685\u20131720 (2007)","journal-title":"Inf. Comput."},{"key":"22_CR12","volume-title":"Handbook of Model Checking","author":"C. Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"22_CR13","volume-title":"Network and Distributed System Security Symp. (NDSS)","author":"D. Balfanz","year":"2002","unstructured":"Balfanz, D., Smetters, D.K., Stewart, P., Wong, H.C.: Talking to strangers: authentication in ad-hoc wireless networks. In: Network and Distributed System Security Symp. (NDSS) (2002)"},{"key":"22_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-46701-7_3","volume-title":"Secure Networking\u2014CQRE [Secure] \u201999","author":"D. Basin","year":"1999","unstructured":"Basin, D.: Lazy infinite-state analysis of security protocols. In: Secure Networking\u2014CQRE [Secure] \u201999. LNCS, vol.\u00a01740, pp.\u00a030\u201342. Springer, Heidelberg (1999)"},{"key":"22_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-15205-4_1","volume-title":"Intl. Workshop Computer Science Logic (CSL)","author":"D. Basin","year":"2010","unstructured":"Basin, D., Cremers, C.: Degrees of security: protocol guarantees in the face of compromising adversaries. In: Dawar, A., Veith, H. (eds.) Intl. Workshop Computer Science Logic (CSL). LNCS, vol.\u00a06247, pp.\u00a01\u201318. Springer, Heidelberg (2010)"},{"key":"22_CR16","series-title":"LNCS","first-page":"340","volume-title":"European Conf. on Research in Computer Security (ESORICS)","author":"D. Basin","year":"2010","unstructured":"Basin, D., Cremers, C.: Modeling and analyzing security in the presence of compromising adversaries. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol.\u00a06345, pp.\u00a0340\u2013356. Springer, Heidelberg (2010)"},{"key":"22_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-28641-4_8","volume-title":"Intl. Conf. Principles of Security and Trust (POST)","author":"D. Basin","year":"2012","unstructured":"Basin, D., Cremers, C., Meier, S.: Provably repairing the ISO\/IEC 9798 standard for entity authentication. In: Degano, P., Guttman, J.D. (eds.) Intl. Conf. Principles of Security and Trust (POST). LNCS, vol.\u00a07215, pp.\u00a0129\u2013148. Springer, Heidelberg (2012)"},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"D. Basin","year":"2001","unstructured":"Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered resolution. J.\u00a0Assoc. Comput. Mach. 48(1), 70\u2013109 (2001)","journal-title":"J.\u00a0Assoc. Comput. Mach."},{"key":"22_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/11591191_38","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: Algebraic intruder deductions. In: Sutcliffe, G., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol.\u00a03835, pp.\u00a0549\u2013564. Springer, Heidelberg (2005)"},{"issue":"3","key":"22_CR20","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D. Basin","year":"2005","unstructured":"Basin, D., 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."},{"key":"22_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03359-9_1","volume-title":"Intl. Conf. on Theorem Proving in Higher Order Logics (TPHOLs)","author":"D. Basin","year":"2009","unstructured":"Basin, D., \u010capkun, S., Schaller, P., Schmidt, B.: Let\u2019s get physical: models and methods for real-world security protocols. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Intl. Conf. on Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol.\u00a05674, pp.\u00a01\u201322. Springer, Heidelberg (2009). Invited paper"},{"key":"22_CR22","first-page":"16","volume-title":"ACM Conf. on Computer and Communications Security (CCS)","author":"M. Baudet","year":"2005","unstructured":"Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Atluri, V., Meadows, C., Juels, A. (eds.) ACM Conf. on Computer and Communications Security (CCS), pp.\u00a016\u201325. ACM, New York (2005)"},{"key":"22_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-02348-4_11","volume-title":"Intl. Conf. Rewriting Techniques and Applications (RTA)","author":"M. Baudet","year":"2009","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. In: Treinen, R. (ed.) Intl. Conf. Rewriting Techniques and Applications (RTA). LNCS, vol.\u00a05595, pp.\u00a0148\u2013163. Springer, Heidelberg (2009)"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-02348-4_11","volume-title":"Intl. Conf. Rewriting Techniques and Applications (RTA)","author":"M. Baudet","year":"2009","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. In: Treinen, R. (ed.) Intl. Conf. Rewriting Techniques and Applications (RTA), pp.\u00a0148\u2013163. Springer, Heidelberg (2009)"},{"issue":"4","key":"22_CR25","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1016\/j.ic.2008.12.005","volume":"207","author":"M. Baudet","year":"2009","unstructured":"Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. Inf. Comput. 207(4), 496\u2013520 (2009)","journal-title":"Inf. Comput."},{"issue":"5","key":"22_CR26","doi-asserted-by":"publisher","first-page":"909","DOI":"10.3233\/JCS-2009-0386","volume":"18","author":"M. Baudet","year":"2010","unstructured":"Baudet, M., Warinschi, B., Abadi, M.: Guessing attacks and the computational soundness of static equivalence. J.\u00a0Comput. Secur. 18(5), 909\u2013968 (2010)","journal-title":"J.\u00a0Comput. Secur."},{"key":"22_CR27","first-page":"459","volume-title":"ACM Conf. on Computer and Communications Security (CCS)","author":"K. Bhargavan","year":"2008","unstructured":"Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conf. on Computer and Communications Security (CCS), pp.\u00a0459\u2013468. ACM, New York (2008)"},{"key":"22_CR28","first-page":"123","volume-title":"Symp. on Information, Computer and Communications Security (ASIACCS)","author":"K. Bhargavan","year":"2008","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D., Swamy, N.: Verified implementations of the information card federated identity-management protocol. In: Abe, M., Gligor, V.D. (eds.) Symp. on Information, Computer and Communications Security (ASIACCS), pp.\u00a0123\u2013135. ACM, New York (2008)"},{"key":"22_CR29","first-page":"82","volume-title":"Computer Security Foundations Workshop (CSFW)","author":"B. Blanchet","year":"2001","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW), pp.\u00a082\u201396. IEEE, Piscataway (2001)"},{"issue":"4","key":"22_CR30","doi-asserted-by":"publisher","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B. Blanchet","year":"2009","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols. J.\u00a0Comput. Secur. 17(4), 363\u2013434 (2009)","journal-title":"J.\u00a0Comput. Secur."},{"key":"22_CR31","first-page":"331","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"B. Blanchet","year":"2005","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0331\u2013340. IEEE, Piscataway (2005)"},{"key":"22_CR32","first-page":"344","volume-title":"Workshop on the Theory and Application of Cryptographic Techniques (EUROCRYPT \u201993)","author":"S. Brands","year":"1994","unstructured":"Brands, S., Chaum, D.: Distance-bounding protocols. In: Helleseth, T. (ed.) Workshop on the Theory and Application of Cryptographic Techniques (EUROCRYPT \u201993), pp.\u00a0344\u2013359. Springer, Heidelberg (1994)"},{"key":"22_CR33","series-title":"LNCS","first-page":"453","volume-title":"Intl. Conf. on the Theory and Application of Cryptographic Techniques (EUROCRYPT)","author":"R. Canetti","year":"2001","unstructured":"Canetti, R., Krawczyk, H.: Analysis of key-exchange protocols and their use for building secure channels. In: Pfitzmann, B. (ed.) Intl. Conf. on the Theory and Application of Cryptographic Techniques (EUROCRYPT). LNCS, vol.\u00a02045, pp.\u00a0453\u2013474. Springer, Heidelberg (2001)"},{"key":"22_CR34","first-page":"355","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"S. Ciob\u00e2ca","year":"2009","unstructured":"Ciob\u00e2ca, S., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. In: Schmidt, R.A. (ed.) Intl. Conf. on Automated Deduction (CADE), pp.\u00a0355\u2013370. Springer, Heidelberg (2009)"},{"issue":"4","key":"22_CR35","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/363516.363528","volume":"9","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Jha, S., Marrero, W.R.: Verifying security protocols with Brutus. Trans. Softw. Eng. Methodol. 9(4), 443\u2013487 (2000)","journal-title":"Trans. Softw. Eng. Methodol."},{"key":"22_CR36","series-title":"LNCS","volume-title":"All About Maude\u2014A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude\u2014A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"22_CR37","series-title":"LNCS","first-page":"294","volume-title":"Intl. Conf. Rewriting Techniques and Applications (RTA)","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.) Intl. Conf. Rewriting Techniques and Applications (RTA). LNCS, vol.\u00a03467, pp.\u00a0294\u2013307. Springer, Heidelberg (2005)"},{"key":"22_CR38","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/978-3-540-39910-0_10","volume-title":"Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Treinen, R.: Easy intruder deductions. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. LNCS, vol.\u00a02772, pp.\u00a0225\u2013242. Springer, Heidelberg (2003)"},{"key":"22_CR39","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-19751-2_3","volume-title":"Intl. Workshop on Formal Aspects of Security and Trust (FAST 2010)","author":"B. Conchinha","year":"2011","unstructured":"Conchinha, B., Basin, D., Caleiro, C.: Efficient decision procedures for message deducibility and static equivalence. In: Degano, P., Etalle, S., Guttman, J.D. (eds.) Intl. Workshop on Formal Aspects of Security and Trust (FAST 2010). LNCS, vol.\u00a06561, pp.\u00a034\u201349 (2011)"},{"key":"22_CR40","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.entcs.2004.10.007","volume":"121","author":"R. Corin","year":"2005","unstructured":"Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. Electron. Notes Theor. Comput. Sci. 121, 47\u201363 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3\u20134","key":"22_CR41","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s10817-010-9187-9","volume":"46","author":"V. Cortier","year":"2011","unstructured":"Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. J.\u00a0Autom. Reason. 46(3\u20134), 225\u2013259 (2011)","journal-title":"J.\u00a0Autom. Reason."},{"key":"22_CR42","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C. Cremers","year":"2008","unstructured":"Cremers, C.: The Scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05123, pp.\u00a0414\u2013418. Springer, Heidelberg (2008)"},{"key":"22_CR43","first-page":"315","volume-title":"European Conf. on Research in Computer Security (ESORICS)","author":"C. Cremers","year":"2011","unstructured":"Cremers, C.: Key exchange in IPsec revisited: formal analysis of IKEv1 and IKEv2. In: Atluri, V., D\u00edaz, C. (eds.) European Conf. on Research in Computer Security (ESORICS), pp.\u00a0315\u2013334. Springer, Heidelberg (2011)"},{"key":"22_CR44","doi-asserted-by":"crossref","unstructured":"Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol version 1.1. Tech. Rep. RFC 4346, Internet Engineering Task Force (2006)","DOI":"10.17487\/rfc4346"},{"issue":"1\u20133","key":"22_CR45","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0019-9958(82)90401-6","volume":"55","author":"D. Dolev","year":"1982","unstructured":"Dolev, D., Even, S., Karp, R.M.: On the security of ping-pong protocols. Inf. Control 55(1\u20133), 57\u201368 (1982)","journal-title":"Inf. Control"},{"key":"22_CR46","first-page":"350","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"D. Dolev","year":"1981","unstructured":"Dolev, D., Yao, A.C.C.: On the security of public key protocols (extended abstract). In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0350\u2013357. IEEE, Piscataway (1981)"},{"issue":"2","key":"22_CR47","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.C.: On the security of public key protocols. Trans. Inf. Theory 29(2), 198\u2013207 (1983)","journal-title":"Trans. Inf. Theory"},{"issue":"2","key":"22_CR48","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"N.A. Durgin","year":"2004","unstructured":"Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. J.\u00a0Comput. Secur. 12(2), 247\u2013311 (2004)","journal-title":"J.\u00a0Comput. Secur."},{"key":"22_CR49","volume-title":"Workshop on Formal Methods and Security Protocols","author":"N.A. Durgin","year":"1999","unstructured":"Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: Undecidability of bounded security protocols. In: Workshop on Formal Methods and Security Protocols (1999)"},{"key":"22_CR50","series-title":"LNCS","first-page":"1","volume-title":"Foundations of Security Analysis and Design (FOSAD), 2007\/2008\/2009 Tutorial Lectures","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.) Foundations of Security Analysis and Design (FOSAD), 2007\/2008\/2009 Tutorial Lectures. LNCS, vol.\u00a05705, pp.\u00a01\u201350. Springer, Heidelberg (2007)"},{"issue":"3","key":"22_CR51","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2009.05.015","volume":"238","author":"S. Escobar","year":"2009","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electron. Notes Theor. Comput. Sci. 238(3), 103\u2013119 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"22_CR52","series-title":"LNCS","first-page":"58","volume-title":"Intl. Cryptology Conf. (CRYPTO)","author":"S. Even","year":"1985","unstructured":"Even, S., Goldreich, O., Shamir, A.: On the security of ping-pong protocols when implemented using the RSA. In: Williams, H.C. (ed.) Intl. Cryptology Conf. (CRYPTO). LNCS, vol.\u00a0218, pp.\u00a058\u201372. Springer, Heidelberg (1985)"},{"key":"22_CR53","first-page":"24","volume-title":"Computer Security Foundations Workshop (CSFW)","author":"J. Guttman","year":"2000","unstructured":"Guttman, J., Thayer, F.: Protocol independence through disjoint encryption. In: Computer Security Foundations Workshop (CSFW), pp.\u00a024\u201334. IEEE, Piscataway (2000)"},{"key":"22_CR54","doi-asserted-by":"crossref","unstructured":"Harkins, D., Carrel, D., et\u00a0al.: The internet key exchange (IKE) (1998)","DOI":"10.17487\/rfc2409"},{"key":"22_CR55","first-page":"441","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol.\u00a03920, pp.\u00a0441\u2013444 (2006)"},{"issue":"5","key":"22_CR56","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"2002","unstructured":"Holzmann, G.: The model checker SPIN. Trans. Softw. Eng. 23(5), 279\u2013295 (2002)","journal-title":"Trans. Softw. Eng."},{"issue":"1","key":"22_CR57","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/s10207-004-0040-1","volume":"3","author":"P.J. Hopcroft","year":"2004","unstructured":"Hopcroft, P.J., Lowe, G.: Analysing a stream authentication protocol using model checking. Int. J. Inf. Secur. 3(1), 2\u201313 (2004)","journal-title":"Int. J. Inf. Secur."},{"key":"22_CR58","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/BFb0034833","volume-title":"Advances in Cryptology (ASIACRYPT \u201996)","author":"M. Just","year":"1996","unstructured":"Just, M., Vaudenay, S.: Authenticated multi-party key agreement. In: Kim, K., Matsumoto, T. (eds.) Advances in Cryptology (ASIACRYPT \u201996). LNCS, vol.\u00a01163, pp.\u00a036\u201349 (1996)"},{"key":"22_CR59","doi-asserted-by":"crossref","unstructured":"Kaufman, C., Hoffman, P., Nir, Y., Eronen, P.: Internet key exchange protocol version 2 (IKEV2). Tech. Rep. RFC 5996, Internet Engineering Task Force (September 2010)","DOI":"10.17487\/rfc5996"},{"key":"22_CR60","series-title":"LNCS","first-page":"389","volume-title":"European Conf. on Research in Computer Security (ESORICS)","author":"S. Kremer","year":"2010","unstructured":"Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) European Conf. on Research in Computer Security (ESORICS). LNCS, vol.\u00a06345, pp.\u00a0389\u2013404. Springer, Heidelberg (2010)"},{"key":"22_CR61","first-page":"129","volume-title":"ACM Conf. on Computer and Communications Security (CCS)","author":"R. K\u00fcsters","year":"2008","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 Conf. on Computer and Communications Security (CCS), pp.\u00a0129\u2013138. ACM, New York (2008)"},{"key":"22_CR62","first-page":"157","volume-title":"Computer Security Foundations Symp. (CSF)","author":"R. K\u00fcsters","year":"2009","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: Computer Security Foundations Symp. (CSF), pp.\u00a0157\u2013171. IEEE, Piscataway (2009)"},{"issue":"3","key":"22_CR63","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"Trans. Program. Lang. Syst."},{"key":"22_CR64","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.entcs.2004.01.020","volume":"112","author":"R. Lanotte","year":"2005","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Automatic analysis of a non-repudiation protocol. Electron. Notes Theor. Comput. Sci. 112, 113\u2013129 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"22_CR65","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0167-4048(92)90222-D","volume":"11","author":"D. Longley","year":"1992","unstructured":"Longley, D., Rigby, S.: An automatic search for security flaws in key management schemes. Comput. Secur. 11(1), 75\u201389 (1992)","journal-title":"Comput. Secur."},{"issue":"3","key":"22_CR66","first-page":"93","volume":"17","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR. Softw., Concepts Tools 17(3), 93\u2013102 (1996)","journal-title":"Softw., Concepts Tools"},{"key":"22_CR67","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/CSFW.1997.596782","volume-title":"Computer Security Foundations Workshop (CSFW)","author":"G. Lowe","year":"1997","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Computer Security Foundations Workshop (CSFW), pp.\u00a031\u201344 (1997)"},{"issue":"1\u20132","key":"22_CR68","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.\u00a0Comput. Secur. 6(1\u20132), 53\u201384 (1998)","journal-title":"J.\u00a0Comput. Secur."},{"key":"22_CR69","volume-title":"Handbook of Model Checking","author":"J. Marques-Silva","year":"2018","unstructured":"Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"1","key":"22_CR70","doi-asserted-by":"publisher","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C. Meadows","year":"1992","unstructured":"Meadows, C.: Applying formal methods to the analysis of a key management protocol. J.\u00a0Comput. Secur. 1(1), 5\u201336 (1992)","journal-title":"J.\u00a0Comput. Secur."},{"issue":"2","key":"22_CR71","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL Protocol Analyzer: an overview. J.\u00a0Log. Program. 26(2), 113\u2013131 (1996)","journal-title":"J.\u00a0Log. Program."},{"key":"22_CR72","first-page":"216","volume-title":"Symp. on Security and Privacy (S & P)","author":"C. Meadows","year":"1999","unstructured":"Meadows, C.: Analysis of the Internet Key Exchange protocol using the NRL Protocol Analyzer. In: Symp. on Security and Privacy (S & P), pp.\u00a0216\u2013231. (1999)"},{"key":"22_CR73","volume-title":"Secure Localization and Time Synchronization in Wireless Ad Hoc and Sensor Networks","author":"C. Meadows","year":"2006","unstructured":"Meadows, C., Poovendran, R., Pavlovic, D., Chang, L., Syverson, P.: Distance bounding protocols: authentication logic analysis and collusion attacks. In: Poovendran, R., Wang, C., Roy, S. (eds.) Secure Localization and Time Synchronization in Wireless Ad Hoc and Sensor Networks. Springer, Heidelberg (2006)"},{"issue":"6","key":"22_CR74","doi-asserted-by":"publisher","first-page":"893","DOI":"10.3233\/JCS-2004-12604","volume":"12","author":"C. Meadows","year":"2004","unstructured":"Meadows, C., Syverson, P.F., Cervesato, I.: Formal specification and analysis of the Group Domain of Interpretation Protocol using NPATRL and the NRL Protocol Analyzer. J.\u00a0Comput. Secur. 12(6), 893\u2013931 (2004)","journal-title":"J.\u00a0Comput. Secur."},{"key":"22_CR75","doi-asserted-by":"publisher","DOI":"10.1201\/9781439821916","volume-title":"Handbook of Applied Cryptography","author":"A. Menezes","year":"1996","unstructured":"Menezes, A., van Oorschot, P., Vanstone, S.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)"},{"key":"22_CR76","volume-title":"Workshop on Formal Methods and Security Protocols","author":"J.K. Millen","year":"1999","unstructured":"Millen, J.K.: A necessarily parallel attack. In: Workshop on Formal Methods and Security Protocols (1999)"},{"issue":"6","key":"22_CR77","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0020-0190(03)00211-4","volume":"86","author":"J.K. Millen","year":"2003","unstructured":"Millen, J.K.: On the freedom of decryption. Inf. Process. Lett. 86(6), 329\u2013333 (2003)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"22_CR78","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1109\/TSE.1987.233151","volume":"13","author":"J.K. Millen","year":"1987","unstructured":"Millen, J.K., Clark, S.C., Freedman, S.B.: The Interrogator: protocol security analysis. Trans. Softw. Eng. 13(2), 274\u2013288 (1987)","journal-title":"Trans. Softw. Eng."},{"key":"22_CR79","first-page":"166","volume-title":"ACM Conf. on Computer and Communications Security (CCS)","author":"J.K. Millen","year":"2001","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Reiter, M.K., Samarati, P. (eds.) ACM Conf. on Computer and Communications Security (CCS), pp.\u00a0166\u2013175 (2001)"},{"key":"22_CR80","first-page":"141","volume-title":"Symp. on Security and Privacy (S & P)","author":"J.C. Mitchell","year":"1997","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: Symp. on Security and Privacy (S & P), pp.\u00a0141\u2013151. IEEE, Piscataway (1997)"},{"issue":"4","key":"22_CR81","doi-asserted-by":"publisher","first-page":"575","DOI":"10.3233\/JCS-2009-0351","volume":"18","author":"S. M\u00f6dersheim","year":"2010","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L., Basin, D.: Constraint differentiation: search-space reduction for the constraint-based analysis of security protocols. J.\u00a0Comput. Secur. 18(4), 575\u2013618 (2010)","journal-title":"J.\u00a0Comput. Secur."},{"issue":"12","key":"22_CR82","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"22_CR83","doi-asserted-by":"crossref","unstructured":"Neuman, C., Hartman, S., Raeburn, K.: The Kerberos network authentication service (V5). Tech. Rep. RFC 4120, Internet Engineering Task Force (July 2005)","DOI":"10.17487\/rfc4120"},{"issue":"6","key":"22_CR84","doi-asserted-by":"publisher","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G. Norman","year":"2006","unstructured":"Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. J.\u00a0Comput. Secur. 14(6), 561\u2013589 (2006)","journal-title":"J.\u00a0Comput. Secur."},{"key":"22_CR85","volume-title":"Handbook of Model Checking","author":"D. Peled","year":"2018","unstructured":"Peled, D.: Partial-order reduction. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"22_CR86","volume-title":"Secure Broadcast Communication in Wired and Wireless Networks","author":"A. Perrig","year":"2002","unstructured":"Perrig, A., Tygar, J.D.: Secure Broadcast Communication in Wired and Wireless Networks. Kluwer Academic, Norwell (2002)"},{"issue":"1","key":"22_CR87","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M. Reiter","year":"1998","unstructured":"Reiter, M., Rubin, A.: Crowds: anonymity for web transactions. Trans. Inf. Syst. Secur. 1(1), 66\u201392 (1998)","journal-title":"Trans. Inf. Syst. Secur."},{"key":"22_CR88","first-page":"174","volume-title":"Computer Security Foundations Workshop (CSFW)","author":"M. Rusinowitch","year":"2001","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Computer Security Foundations Workshop (CSFW), p.\u00a0174. IEEE, Piscataway (2001)"},{"key":"22_CR89","first-page":"109","volume-title":"Computer Security Foundations Symp. (CSF)","author":"P. Schaller","year":"2009","unstructured":"Schaller, P., Schmidt, B., Basin, D., \u010capkun, S.: Modeling and verifying physical properties of security protocols for wireless networks. In: Computer Security Foundations Symp. (CSF), pp.\u00a0109\u2013123. IEEE, Piscataway (2009)"},{"key":"22_CR90","first-page":"78","volume-title":"Computer Security Foundations Symp. (CSF)","author":"B. Schmidt","year":"2012","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Computer Security Foundations Symp. (CSF), pp.\u00a078\u201394 (2012)"},{"key":"22_CR91","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1016\/S0747-7171(89)80037-9","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"Schmidt-Schau\u00df, M.: Unification in permutative theories is undecidable. J.\u00a0Symb. Comput. 8, 415\u2013421 (1989)","journal-title":"J.\u00a0Symb. Comput."},{"issue":"3","key":"22_CR92","doi-asserted-by":"publisher","first-page":"355","DOI":"10.3233\/JCS-2004-123-403","volume":"12","author":"V. Shmatikov","year":"2004","unstructured":"Shmatikov, V.: Probabilistic analysis of an anonymity system. J.\u00a0Comput. Secur. 12(3), 355\u2013377 (2004)","journal-title":"J.\u00a0Comput. Secur."},{"key":"22_CR93","unstructured":"Shoup, V.: On formal models for secure key exchange (version 4) (1999). Revision of IBM Research Report RZ 3120, (April 1999)"},{"key":"22_CR94","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1109\/CSFW.1999.779773","volume-title":"Computer Security Foundations Workshop (CSFW)","author":"D.X.A. Song","year":"1999","unstructured":"Song, D.X.A.: A new efficient automatic checker for security protocol analysis. In: Computer Security Foundations Workshop (CSFW), pp.\u00a0192\u2013202 (1999)"},{"key":"22_CR95","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/3-540-60385-9_13","volume-title":"Correct Hardware Design and Verification Methods","author":"U. Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) Correct Hardware Design and Verification Methods. LNCS, vol.\u00a0987, pp.\u00a0206\u2013224. Springer, Heidelberg (1995)"},{"issue":"1\u20132","key":"22_CR96","first-page":"27","volume":"7","author":"P.F. Syverson","year":"1996","unstructured":"Syverson, P.F., Meadows, C.: A formal language for cryptographic protocol requirements. Des. Codes Cryptogr. 7(1\u20132), 27\u201359 (1996)","journal-title":"Des. Codes Cryptogr."},{"key":"22_CR97","first-page":"79","volume-title":"IFIP International Conference on Trust Management (IFIPTM)","author":"F.J. Thayer","year":"2010","unstructured":"Thayer, F.J., Swarup, V., Guttman, J.D.: Metric strand spaces for locale authentication protocols. In: Nishigaki, M., J\u00f8sang, A., Murayama, Y., Marsh, S. (eds.) IFIP International Conference on Trust Management (IFIPTM), vol.\u00a0321, pp.\u00a079\u201394. Springer, Heidelberg (2010)"},{"key":"22_CR98","series-title":"LNCS","first-page":"277","volume-title":"Intl. Conf. Rewriting Techniques and Applications (RTA)","author":"M. Turuani","year":"2006","unstructured":"Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) Intl. Conf. Rewriting Techniques and Applications (RTA). LNCS, vol.\u00a04098, pp.\u00a0277\u2013286. Springer, Heidelberg (2006)"},{"issue":"2","key":"22_CR99","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/JSAC.2005.861380","volume":"24","author":"S. \u010capkun","year":"2006","unstructured":"\u010capkun, S., Hubaux, J.: Secure positioning in wireless networks. J.\u00a0Sel. Areas Commun. 24(2), 221\u2013232 (2006)","journal-title":"J.\u00a0Sel. Areas Commun."},{"key":"22_CR100","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2005.11.052","volume":"155","author":"L. Vigan\u00f2","year":"2006","unstructured":"Vigan\u00f2, L.: Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61\u201386 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T01:45:03Z","timestamp":1571363103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":100,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_22","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}