{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:19:41Z","timestamp":1740028781679,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_22","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"299-314","source":"Crossref","is-referenced-by-count":8,"title":["Pattern-Based Abstraction for Verifying Secrecy in Protocols"],"prefix":"10.1007","author":[{"given":"Liana","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"P\u00e9rin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"22_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/BFb0014571","volume-title":"Theoretical Aspects of Computer Software","author":"M. Abadi","year":"1997","unstructured":"Mart\u00edn Abadi. Secrecy by typing in security protocols. In Theoretical Aspects of Computer Software, volume 1281 of LNCS, p. 611\u2013638, 1997."},{"key":"22_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/3-540-45315-6_2","volume-title":"Foundations of Software Science and Computation Structures","author":"M. Abadi","year":"2001","unstructured":"Mart\u00edn Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. In Foundations of Software Science and Computation Structures, volume 2030 of LNCS, p. 25\u201341, 2001."},{"key":"22_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/3-540-44618-4_28","volume-title":"On the reachability problem in cryptographic protocols","author":"R. M. Amadio","year":"2000","unstructured":"Roberto M. Amadio and Denis Lugiez. On the reachability problem in cryptographic protocols. In International Conference on Concurrency Theory, volume 1877 of LNCS, p. 380\u2013394, 2000."},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"D. Bolignano. An approach to the formal verification of cryptographic protocols. In ACM Conference on Computer and Communications Security, p. 106\u2013118, 1996.","DOI":"10.1145\/238168.238196"},{"key":"22_CR5","unstructured":"L. Bozga, Y. Lakhnech, and M. P\u00e9rin. Abstract interpretation for secrecy using patterns. Technical report, Verimag, 2002."},{"key":"22_CR6","unstructured":"J. Clark and J. Joacob. A survey on authentification protocol. Available at the url http:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareviewps.ps , 1997."},{"key":"22_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_56","volume-title":"International Colloquium on Automata, Languages and Programming","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 International Colloquium on Automata, Languages and Programming, volume 2076 of LNCS, 2001."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"H. Comon, V. Shmatikov. Is it possible to decide whether a cryptographic protocol is secure or not? Journal of Telecommunications and Information Technology, 2002.","DOI":"10.26636\/jtit.2002.4.149"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"H. Comon-Lundh and V. Cortier. Security properties: Two agents are sufficient. Technical report, LSV, 2002.","DOI":"10.1007\/3-540-36575-3_8"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"D. Dolev, S. Even, and R. M. Karp. On the security of ping-pong protocols. In Advances in Cryptology, p. 177\u2013186, 1982.","DOI":"10.1016\/S0019-9958(82)90401-6"},{"issue":"2","key":"22_CR11","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198\u2013208, 1983.","journal-title":"IEEE Transactions on Information Theory"},{"key":"22_CR12","unstructured":"N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Workshop on Formal Methods and Security Protocols, 1999."},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"S. Even and O. Goldreich. On the security of multi-party ping pong protocols. Technical report, Israel Institute of Technology, 1983.","DOI":"10.1109\/SFCS.1983.42"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"F.J.T. F\u00e1brega, J.C. Herzog, and J.D. Guttman. Strand Spaces: Why is a Security Protocol Correct? In IEEE Conference on Security and Privacy, p. 160\u2013171, 1998.","DOI":"10.21236\/ADA459060"},{"key":"22_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/10719839","volume-title":"Rewriting for cryptographic protocol verification","author":"T. Genet","year":"2000","unstructured":"T. Genet and F. Klay. Rewriting for cryptographic protocol verification. In International Conference on Automated Deduction, volume 1831 of LNCS, 2000."},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"A. Gordon and A. Jeffrey. Authenticity by typing for security protocols. In IEEE Computer Security Foundations Workshop, p. 145\u2013159, 2001.","DOI":"10.1109\/CSFW.2001.930143"},{"key":"22_CR17","series-title":"Lect Notes Comput Sci","volume-title":"A method for automatic cryptographic protocol verification","author":"J. Goubault-Larrecq","year":"2000","unstructured":"Jean Goubault-Larrecq. A method for automatic cryptographic protocol verification. In International Workshop on Formal Methods for Parallel Programming: Theory and Applications, volume 1800 of LNCS, 2000."},{"issue":"3","key":"22_CR18","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"G. Lowe. An attack on the Needham-Schroeder public-key authentification protocol. Information Processing Letters, 56(3):131\u2013133, 1995.","journal-title":"Information Processing Letters"},{"key":"22_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","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, p. 147\u2013166, 1996."},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"C. Meadows. Invariant generation techniques in cryptographic protocol analysis. In Computer Security Foundations Workshop, 2000.","DOI":"10.21236\/ADA464088"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In ACM Conference on Computer and Communications Security, p. 166\u2013175, 2001.","DOI":"10.1145\/501983.502007"},{"key":"22_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/3-540-48294-6_10","volume-title":"Abstracting Cryptographic Protocols with Tree Automata","author":"D. Monniaux","year":"1999","unstructured":"David Monniaux. Abstracting Cryptographic Protocols with Tree Automata. In Static Analysis Symposium, volume 1694 of LNCS, p. 149\u2013163, 1999."},{"issue":"12","key":"22_CR23","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"R.M. Needham and M.D. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993\u2013999, 1978.","journal-title":"Communications of the ACM"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is NP-complete. In IEEE Computer Security Foundations Workshop, 2001.","DOI":"10.1109\/CSFW.2001.930145"},{"key":"22_CR25","unstructured":"J. Thayer, J. Herzog, and J. Guttman. Honest Ideals on Strand Spaces. In IEEE Computer Security Foundations Workshop, p. 66\u201378, 1998."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:12:33Z","timestamp":1739992353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}