{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,25]],"date-time":"2026-10-25T19:54:24Z","timestamp":1792958064362,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439158","type":"print"},{"value":"9783540456070","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45607-4_5","type":"book-chapter","created":{"date-parts":[[2007,5,22]],"date-time":"2007-05-22T19:08:20Z","timestamp":1179860900000},"page":"76-90","source":"Crossref","is-referenced-by-count":4,"title":["Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sandro","family":"Etalle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In Proc. POPL 2002, pages 33\u201344, 2002.","DOI":"10.1145\/503272.503277"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"L. C. Aiello and F. Massacci. Verifying security protocols as planning in logic programming. Trans. on Computational Logic, 2001.","DOI":"10.1145\/383779.383785"},{"key":"5_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]\u2019 99","author":"D. Basin","year":"1999","unstructured":"D. Basin. Lazy infinite-state analysis of security protocols. Secure Networking \u2014 CQRE [Secure]\u2019 99\u201d, LNCS 1740, pages 30\u201342, 1999."},{"key":"5_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BFb0055875","volume-title":"Proc.5th Symp. on Research in Computer Security","author":"G. Bella","year":"1998","unstructured":"G. Bella and L. C. Paulson. Kerberos version IV: Inductive analysis of the secrecy goals. In Proc.5th Symp. on Research in Computer Security, LNCS 1485, pages 361\u2013375, 1998."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Proc. CSFW\u201901, 2001.","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Trans, on Computer Systems, 8(1):18\u201336, 1990.","journal-title":"ACM Trans, on Computer Systems"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In Proc. CSFW\u2019 99, pages 55\u201369, 1999.","DOI":"10.1109\/CSFW.1999.779762"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"I. Cervesato, N. Durgin, J. Mitchell, Lincoln, and A. Scedrov. Relating strands and multiset rewriting for security protocol analysis. In Proc. CSFW\u2019 00, pages 35\u201351, 2000.","DOI":"10.1109\/CSFW.2000.856924"},{"key":"5_CR9","unstructured":"Y. Chevalier, F. Jacquemard, M. Rusinowitch, M. Turuani, and L. Vigneron. CAS-RUL web site. http:\/\/www.loria.fr\/equipes\/protheo\/SOFTWARES\/CASRUL\/ ."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Y. Chevalier and L. Vigneron. A tool for lazy verification of security protocols. In Proc. Int\u2019l Conf. Automated Software Engineering, 2001.","DOI":"10.1109\/ASE.2001.989832"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Y. Chevalier and L. Vigneron. Towards efficient automated verification of security protocols. In Proc. VERIF\u2019 01, 2001.","DOI":"10.1007\/3-540-45657-0_24"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"G. Delzanno. Specifying and debugging security protocols via hereditary harrop formulas and lambda prolog. In Proc. FLOPS\u2019 01, pages 123\u2013137, 2001.","DOI":"10.1007\/3-540-44716-4_8"},{"issue":"2","key":"5_CR13","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 Trans. on Information Theory, 29(2):198\u2013208, 1983.","journal-title":"IEEE Trans. on Information Theory"},{"key":"5_CR14","unstructured":"N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Proc. FMSP\u201999 (FLOC\u2019 99), 1999."},{"key":"5_CR15","unstructured":"A. Huima. Efficient infinite-state analysis of security protocols. In Proc. FMSP\u2019 99 (FLOC\u2019 99), 1999."},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","first-page":"131","volume-title":"Proc. LPAR 2000","author":"F. Jacquemard","year":"2000","unstructured":"F. Jacquemard, M. Rusinowitch, and L. Vigneron. Compiling and verifying security protocols. In Proc. LPAR 2000, LNCS 1995, pages 131\u2013160, 2000."},{"key":"5_CR17","first-page":"93","volume":"17","author":"G. Lowe","year":"1996","unstructured":"G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts and Tools, (17):93\u2013102, 1996.","journal-title":"Software Concepts and Tools"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"G. Lowe. Casper: A compiler for the analysis of security protocols. In Proc.CSFW\u2019 97, pages 18\u201330, 1997.","DOI":"10.1109\/CSFW.1997.596779"},{"issue":"2\u2013-3","key":"5_CR19","first-page":"89","volume":"7","author":"G. Lowe","year":"1998","unstructured":"G. Lowe. Towards a completeness result for model checking of security protocols. J. of Computer Security, 7(2\u2013-3):89\u2013146, 1998.","journal-title":"J. of Computer Security"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"C. Meadows. Formal verification of cryptographic protocols: A survey. In Proc. ASIACRYPT\u2019 94, pages 133\u2013150, 1995.","DOI":"10.21236\/ADA464292"},{"issue":"2","key":"5_CR21","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"C. Meadows. The NRL protocol analyzer: An overview. J. of Logic Programming, 26(2):113\u2013131, 1996.","journal-title":"J. of Logic Programming"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In Proc. 2001 ACM Conf. on Computer and Communication Security, pages 166\u2013175, 2001.","DOI":"10.1145\/501983.502007"},{"issue":"2","key":"5_CR23","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1109\/TSE.1987.233151","volume":"13","author":"J. K. Millen","year":"1987","unstructured":"J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol security analysis. IEEE Trans. on Software Engineering, 13(2):274\u2013288, 1987.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using mur\u03c6. In Proc. Conf. on Security and Privacy, pages 141\u2013153, 1997.","DOI":"10.1109\/SECPRI.1997.601329"},{"issue":"12","key":"5_CR25","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. Comm. of the ACM, 21(12):993\u2013999, 1978.","journal-title":"Comm. of the ACM"},{"key":"5_CR26","unstructured":"L. C. Paulson. Mechanized proofs of security protocols: Needham-Schroeder with public keys. T.R. 413, Univ. of Cambridge, Computer Laboratory, January 1997."},{"key":"5_CR27","doi-asserted-by":"crossref","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. of Computer Security, 6:85\u2013128, 1998.","journal-title":"J. of Computer Security"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe. Modelling and verifying key-exchange protocols using csp and fdr. In IEEE Symp. on Foundations of Secure Systems, 1995.","DOI":"10.1109\/CSFW.1995.518556"},{"key":"5_CR29","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1999."},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is np-complete. In Proc. CSFW\u2019 01, 2001.","DOI":"10.1109\/CSFW.2001.930145"}],"container-title":["Lecture Notes in Computer Science","Logic Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45607-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T14:52:10Z","timestamp":1737039130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45607-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439158","9783540456070"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45607-4_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}