{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T05:06:08Z","timestamp":1737176768719,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008972"},{"type":"electronic","value":"9783540365761"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","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":[[2003]]},"DOI":"10.1007\/3-540-36576-1_9","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:42:17Z","timestamp":1181616137000},"page":"136-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Verification of Cryptographic Protocols: Tagging Enforces Termination"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Blanchet","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th ACM Symp. on Principles of Programming Languages (POPL\u201902), pages 33\u201344, Jan. 2002.","key":"9_CR1","DOI":"10.1145\/503272.503277"},{"issue":"1","key":"9_CR2","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6\u201315, Jan. 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-45694-5_33","volume-title":"CONCUR\u201902\u2013Concurrency Theory","author":"R. Amadio","year":"2002","unstructured":"R. Amadio and W. Charatonik. On Name Generation and Set-Based Analysis in the Dolev-Yao Model. In CONCUR\u201902\u2013Concurrency Theory, volume 2421 of LNCS, pages 499\u2013514. Springer, Aug. 2002."},{"doi-asserted-by":"crossref","unstructured":"B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82\u201396, June 2001.","key":"9_CR4","DOI":"10.1109\/CSFW.2001.930138"},{"key":"9_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"From Secrecy to Authenticity in Security Protocols","author":"B. Blanchet","year":"2002","unstructured":"B. Blanchet. From Secrecy to Authenticity in Security Protocols. In 9th Internat. Static Analysis Symposium (SAS\u201902), volume 2477 of LNCS, pages 342\u2013359. Springer, Sept. 2002."},{"key":"9_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/10722599_11","volume-title":"Automating Data Independence","author":"P. Broadfoot","year":"2000","unstructured":"P. Broadfoot, G. Lowe, and B. Roscoe. Automating Data Independence. In 6th European Symp. on Research in Computer Security (ESORICS\u201900), volume 1895 of LNCS, pages 175\u2013190. Springer, Oct. 2000."},{"doi-asserted-by":"crossref","unstructured":"P. J. Broadfoot and A. W. Roscoe. Capturing Parallel Attacks within the Data Independence Framework. In 15th IEEE Computer Security Foundations Workshop (CSFW\u201902), pages 147\u2013159, June 2002.","key":"9_CR7","DOI":"10.1109\/CSFW.2002.1021813"},{"doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. Proceedings of the Royal Society of London A, 426:233\u2013271, 1989.","key":"9_CR8","DOI":"10.1145\/74850.74852"},{"doi-asserted-by":"crossref","unstructured":"E. Cohen. TAPS: A First-Order Verifier for Cryptographic Protocols. In 13th IEEE Computer Security Foundations Workshop (CSFW-13), pages 144\u2013158, 2000.","key":"9_CR9","DOI":"10.1109\/CSFW.2000.856933"},{"key":"9_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"682","DOI":"10.1007\/3-540-48224-5_56","volume-title":"Tree Automata with One Memory, Set Constraints, and Ping-Pong Protocols","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 Automata, Languages and Programming, 28th Internat. Colloq., ICALP\u201901, volume 2076 of LNCS, pages 682\u2013693. Springer, July 2001."},{"key":"9_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/3-540-45789-5_24","volume-title":"An Improved Constraint-Based System for the verification of Security Protocols","author":"R. Corin","year":"2002","unstructured":"R. Corin and S. Etalle. An Improved Constraint-Based System for the verification of Security Protocols. In 9th Internat. Static Analysis Symposium (SAS\u201902), volume 2477 of LNCS, pages 326\u2013341. Springer, Sept. 2002."},{"doi-asserted-by":"crossref","unstructured":"V. Cortier, J. Millen, and H. Rue\u00df. Proving secrecy is easy enough. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 97\u2013108, June 2001.","key":"9_CR12","DOI":"10.1109\/CSFW.2001.930139"},{"unstructured":"N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Workshop on Formal Methods and Security Protocols (FMSP\u201999), July 1999.","key":"9_CR13"},{"doi-asserted-by":"crossref","unstructured":"A. Gordon and A. Jeffrey. Authenticity by Typing for Security Protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 145\u2013159, June 2001.","key":"9_CR14","DOI":"10.1109\/CSFW.2001.930143"},{"key":"9_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"977","DOI":"10.1007\/3-540-45591-4_134","volume-title":"A Method for Automatic Cryptographic Protocol verification (Extended Abstract)","author":"J. Goubault-Larrecq","year":"2000","unstructured":"J. Goubault-Larrecq. A Method for Automatic Cryptographic Protocol verification (Extended Abstract), invited paper. In 5th Internat. Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA\u201900), volume 1800 of LNCS, pages 977\u2013984. Springer, May 2000."},{"doi-asserted-by":"crossref","unstructured":"J. Heather, G. Lowe, and S. Schneider. How to Prevent Type Flaw Attacks on Security Protocols. In 13th IEEE Computer Security Foundations Workshop (CSFW-13), pages 255\u2013268, July 2000.","key":"9_CR16","DOI":"10.1109\/CSFW.2000.856942"},{"doi-asserted-by":"crossref","unstructured":"J. Heather and S. Schneider. Towards automatic verification of authentication protocols on an unbounded network. In 13th IEEE Computer Security Foundations Workshop (CSFW-13), pages 132\u2013143, July 2000.","key":"9_CR17","DOI":"10.1109\/CSFW.2000.856932"},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","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":"G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of LNCS, pages 147\u2013166. Springer, 1996."},{"doi-asserted-by":"crossref","unstructured":"J. Millen and V. Shmatikov. Constraint Solving for Bounded-Process Cryptographic Protocol Analysis. In 8th ACM Conf. on Computer and Communications Security (CCS\u201901), pages 166\u2013175, 2001.","key":"9_CR19","DOI":"10.1145\/501983.502007"},{"doi-asserted-by":"crossref","unstructured":"F. Nielson, H. R. Nielson, and H. Seidl. Cryptographic Analysis in Cubic Time. In TOSCA 2001-Theory of Concurrency, Higher Order Languages and Types, volume 62 of ENTCS, Nov. 2001.","key":"9_CR20","DOI":"10.1007\/3-540-45309-1_17"},{"issue":"1\u20132","key":"9_CR21","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. C. Paulson","year":"1998","unstructured":"L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. J. Computer Security, 6(1\u20132):85\u2013128, 1998.","journal-title":"J. Computer Security"},{"issue":"2 3","key":"9_CR22","doi-asserted-by":"publisher","first-page":"147","DOI":"10.3233\/JCS-1999-72-303","volume":"7","author":"A.W. Roscoe","year":"1999","unstructured":"A.W. Roscoe and P. J. Broadfoot. Proving Security Protocols with Model Checkers by Data Independence Techniques. J. Computer Security, 7(2, 3):147\u2013190, 1999.","journal-title":"J. Computer Security"},{"doi-asserted-by":"crossref","unstructured":"M. Rusinovitch and M. Turuani. Protocol Insecurity with Finite Number of Sessions is NP-complete. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 174\u2013187, June 2001.","key":"9_CR23","DOI":"10.1109\/CSFW.2001.930145"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction \u2014 CADE-16","author":"Christoph Weidenbach","year":"1999","unstructured":"C. Weidenbach. Towards an Automatic Analysis of Security Protocols in First-Order Logic. In 16th Internat. Conf. on Automated Deduction (CADE-16), volume 1632 of LNAI, pages 314\u2013328. Springer, July 1999."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36576-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:54:19Z","timestamp":1737093259000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36576-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008972","9783540365761"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-36576-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}