{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T20:49:31Z","timestamp":1761338971705},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_24","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T10:59:43Z","timestamp":1179572383000},"page":"324-337","source":"Crossref","is-referenced-by-count":31,"title":["Automated Unbounded Verification of Security Protocols"],"prefix":"10.1007","author":[{"given":"Yannick","family":"Chevalier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Vigneron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"R. Amadio and D. Lugiez. On the reachability problem in cryptographic protocols. In CONCUR\u20192000, pages 380\u2013394, 2000.","DOI":"10.1007\/3-540-44618-4_28"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"A. Armando, D. Basin, M. Bouallagui, Y. Chevalier, L. Compagna, S. M\u00f6dersheim, M. Rusinowitch, M. Turuani, L. Vigano, and L. Vigneron. The AVISS Security Protocol Analysis Tool. In CAV\u201902, 2002. Tool presentation.","DOI":"10.1007\/3-540-45657-0_27"},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-46701-7_3","volume-title":"Secure Networking \u2014 CQRE (Secure)\u201999","author":"D. Basin","year":"1999","unstructured":"D. Basin. Lazy Infinite-State Analysis of Security Protocols. In R. Baumgart, editor, Secure Networking \u2014 CQRE (Secure)\u201999, LNCS 1740, pages 30\u201342, Heidelberg, Germany, 1999. Springer-Verlag."},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop, June 2001.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"24_CR5","unstructured":"Y. Chevalier and L. Vigneron. Towards Efficient Automated Verification of Security Protocols. In Verification Workshop (VERIFY\u201901) (in connection with IJCAR\u201901), Universit\u00e0 degli studi di Siena, TR DII 08\/01, pages 19\u201333, 2001."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Y. Chevalier and L. Vigneron. Automated Unbounded Verification of Security Protocols. Research Report 4369, Institut National de Recherche en Informatique et Automatique, Nancy (France), January 2002.","DOI":"10.1007\/3-540-45657-0_24"},{"key":"24_CR7","unstructured":"J. Clark and J. Jacob. A Survey of Authentication Protocol Literature: Version 1.0, 17 Nov. 1997. URL http:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz ."},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/3-540-48224-5_56","volume-title":"28th Int. Coll. Automata, Languages, and Programming (ICALP\u20192001)","author":"H. Comon","year":"2001","unstructured":"H. Comon, V. Cortier, and J. Mitchell. Tree Automata with one Memory, Set Constraints and Ping-Pong Protocols. In 28th Int. Coll. Automata, Languages, and Programming (ICALP\u20192001), LNCS 2076, pages 682\u2013693. Springer, 2001."},{"key":"24_CR9","unstructured":"B. Donovan, P. Norris, and G. Lowe. Analyzing a Library of Security Protocols using Casper and FDR. In W. on Formal Methods and Security Protocols, 1999."},{"key":"24_CR10","unstructured":"N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of Bounded Security Protocols. In FLOC\u201999 Workshop on Formal Methods and Sec. Protocols (FMSP\u201999), 1999."},{"key":"24_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"977","DOI":"10.1007\/3-540-45591-4_134","volume-title":"IPDPS 2000 Workshops, Cancun, Mexico","author":"J. Goubault-Larrecq","year":"2000","unstructured":"J. Goubault-Larrecq. A Method for Automatic Cryptographic Protocol Verification. In IPDPS 2000 Workshops, Cancun, Mexico, LNCS 1800, pages 977\u2013984. Springer, May 2000."},{"key":"24_CR12","series-title":"Lect Notes Comput Sci","first-page":"131","volume-title":"Proceedings of LPAR\u20192000","author":"F. Jacquemard","year":"2000","unstructured":"F. Jacquemard, M. Rusinowitch, and L. Vigneron. Compiling and Verifying Security Protocols. In M. Parigot and A. Voronkov, editors, Proceedings of LPAR\u20192000, LNCS 1955, pages 131\u2013160, Heidelberg, 2000. Springer-Verlag."},{"key":"24_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-1999-72-302","volume":"7","author":"G. Lowe","year":"1999","unstructured":"G. Lowe. Towards a Completeness Result for Model Checking of Security Protocols. Journal of Computer Security 7, 1, 1999.","journal-title":"Journal of Computer Security"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"J. Millen and V. Shmatikov. Constraint Solving for Bounded-Process Cryptographic Protocol Analysis. In 8th ACM Conference on Computer and Communication Security, pages 166\u2013175, November 2001.","DOI":"10.1145\/501983.502007"},{"key":"24_CR15","series-title":"Lect Notes Comput Sci","volume-title":"6th Int. Static Analysis Symposium (SAS\u201999)","author":"D. Monniaux","year":"1999","unstructured":"D. Monniaux. Abstracting Cryptographic Protocols with Tree Automata. In 6th Int. Static Analysis Symposium (SAS\u201999), LNCS 1694. Springer-Verlag, 1999."},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"M. Rusinowitch and M. Turuani. Protocol Insecurity with Finite Number of Sessions is NP-complete. In Proceedings of the 14th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 2001.","DOI":"10.1109\/CSFW.2001.930145"},{"issue":"12","key":"24_CR17","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"D. Song","year":"2001","unstructured":"D. Song, S. Berezin, and A. Perrig. Athena, a Novel Approach to Efficient Automatic Security Protocol Analysis. J. of Computer Security, 9((1,2)):47\u201374, 2001.","journal-title":"J. of Computer Security"},{"key":"24_CR18","unstructured":"S. Stoller. A Bound on Attacks on Authentication Protocols. Technical Report 526, Indiana University, Computer Science Dept, February 2000."},{"key":"24_CR19","series-title":"Lect Notes Comput Sci","first-page":"468","volume-title":"Computer Science Logic","author":"L. Vigneron","year":"1995","unstructured":"L. Vigneron. Positive Deduction modulo Regular Theories. In Hans Kleine-B\u00fcning, editor, Computer Science Logic, LNCS 1092, pages 468\u2013485, Berlin, 1995. Springer-Verlag. URL: http:\/\/www.loria.fr\/equipes\/protheo\/SOFTWARES\/DATAC\/ ."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:21:05Z","timestamp":1556414465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}