{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:19:12Z","timestamp":1742959152430,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417392"},{"type":"electronic","value":"9783540447160"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","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":[[2001]]},"DOI":"10.1007\/3-540-44716-4_8","type":"book-chapter","created":{"date-parts":[[2007,8,15]],"date-time":"2007-08-15T18:16:34Z","timestamp":1187201794000},"page":"123-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Specifying and Debugging Security Protocols via Hereditary Harrop Formulas and \u03bbProlog \u2010 A Case-study \u2010"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,21]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"M. Bozzano, G. Delzanno, and M. Martelli. A Bottom-up semantics for Linear Logic Programs. In Proc. PPDP\u201900, page 92\u2013102, 2000.","DOI":"10.1145\/351268.351279"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"M. Bozzano, G. Delzanno, and M. Martelli. An Effective Bottom-up Semantics for First-Order Linear Logic Programs. To appear in Proc. FLOPS 2001, March 2001.","DOI":"10.1007\/3-540-44716-4_9"},{"issue":"1","key":"8_CR3","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"M. Burrows, M. Abadi, R. M. Needham. A Logic of Authentication. TOCS 8 (1): 18\u201336, 1990.","journal-title":"A Logic of Authentication. TOCS"},{"key":"8_CR4","unstructured":"I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. A Meta-Notation for Protocol Analysis. In Proc. Computer Security Foundations Workshop CSFW\u201999, pages 28\u201330, 1999."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"I. Cervesato, N. Durgin, M. Kanovich, and A. Scedrov. Interpreting Strands in Linear Logic In Proc. of Formal Methods and Computer Security FMCS\u201900, 2000.","DOI":"10.21236\/ADA465155"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Relating Strands and Multiset Rewriting for Security Protocol Analysis. In Proc. of Computer Security Foundations Workshop CSFW\u201900, pages 35\u201351, 2000.","DOI":"10.1109\/CSFW.2000.856924"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"E. Clarke, S. Jha, W. Marrero. Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols. In Proc. of PRO-COMET\u201998, 1998.","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"8_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1007\/3-540-46419-0_34","volume-title":"Proc. of TACAS 2000","author":"E. Clarke","year":"2000","unstructured":"E. Clarke, S. Jha, W. Marrero. Partial Order Reductions for Security Protocol Verification. In Proc. of TACAS 2000, pages 503\u2013518, LNCS 1785, 2000."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"D. Dolev and A. Yao. On the Security pf Public-key Protocols. IEEE Transactions on Information Theory, 2(29), 1983.","DOI":"10.1109\/TIT.1983.1056650"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"J.Y. Girard. Linear logic. Theoretical Computer Science, 50:1\u2013102, 1987.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J. Hodas","year":"1994","unstructured":"J. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation, 110(2):327\u2013365, 1994.","journal-title":"Information and Computation"},{"key":"8_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/3-540-55844-6_145","volume-title":"Proc. PLILP 1992","author":"A. H. B. Hoa","year":"1992","unstructured":"A. Hui Bon Hoa. A Bottom-Up Interpreter for a Higher-Order Logic Programming Language. In Proc. PLILP 1992, pages 326\u2013340, LNCS 631, 1992."},{"key":"8_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Proc. TACAS\u201996","author":"G. Lowe","year":"1996","unstructured":"G. Lowe. Breaking and Fixing the Needham-Schroeder Public-key Protocol using CSP and FDR. In Proc. TACAS\u201996, page 147\u2013166, LNCS 1055, 1996."},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"F. Massacci. Automated Reasoning and the Verification of Security Protocols In Proc. of TABLEAUX \u201999, pages 32\u201333, LNAI 1617, 1999.","DOI":"10.1007\/3-540-48754-9_6"},{"issue":"2","key":"8_CR15","first-page":"113","volume":"26","author":"C. Meadows","year":"1996","unstructured":"C. Meadows. The NRL Protocol Analyzer: An Overview. JLP 26(2): 113\u2013131, 1996.","journal-title":"The NRL Protocol Analyzer: An Overview"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"R. McDowell, D. Miller. A Logic for Reasoning with Higher-Order Abstract Syntax. In Proc. LICS \u201997, pages 434\u2013445, 1997.","DOI":"10.1109\/LICS.1997.614968"},{"key":"8_CR17","unstructured":"D. Miller. Lexical Scoping as Universal Quantification. In Proc. ICLP \u201989, pages 268\u2013283, 1989."},{"issue":"1&2","key":"8_CR18","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0743-1066(89)90031-9","volume":"6","author":"D. Miller","year":"1989","unstructured":"D. Miller. A Logical Analysis of Modules in Logic Programming. JLP 6(1&2): 79\u2013108, 1989.","journal-title":"JLP"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"D. Miller","year":"1996","unstructured":"D. Miller. Forum: A Multiple-Conclusion Specification Logic. Theoretical Computer Science, 165(1):201\u2013232, 1996.","journal-title":"Theoretical Computer Science"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logic, 51:125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"8_CR21","unstructured":"G. Nadathur and D. Miller. An Overview of \u03bb-Prolog. In Proc. of ILPS\/SLP \u201988, pages 810\u2013827, 1988."},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"Proc CADE\u201999","author":"G. Nadathur","year":"1999","unstructured":"G. Nadathur, D. J. Mitchell. System Description: Teyjus-A Compiler and Abstract Machine Based Implementation of lambda-Prolog. In Proc CADE\u201999, LNCS 1632, pages 287\u2013291, 1999."},{"issue":"12","key":"8_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. CACM 21(12): 993\u2013999, 1978.","journal-title":"CACM"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44716-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T10:55:00Z","timestamp":1737370500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44716-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417392","9783540447160"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-44716-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"21 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}