{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:26:46Z","timestamp":1748071606350,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001416"},{"type":"electronic","value":"9783540361350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36135-9_14","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:43:21Z","timestamp":1180665801000},"page":"210-225","source":"Crossref","is-referenced-by-count":15,"title":["Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[]},{"given":"Luca","family":"Compagna","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"issue":"4","key":"14_CR1","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1145\/383779.383785","volume":"2","author":"L. Aiello Carlucci","year":"2001","unstructured":"Luigia Carlucci Aiello and Fabio Massacci. Verifying security protocols as planning in logic programming. ACM Transactions on Computational Logic, 2(4):542\u2013580, October 2001.","journal-title":"ACM Transactions on Computational Logic"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"A. Armando, D. Basin, M. Bouallagui, Y. Chevalier, L. Compagna, S. Moedersheim, M. Rusinowitch, M. Turuani, L. Vigan\u00f2, and L. Vigneron. The AVISS Security Proto cols Analysis Tool. In 14th International Conference on Computer-Aided Verification (CAV\u201902). 2002.","DOI":"10.1007\/3-540-45657-0_27"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"David Basin and Grit Denker. Maude versus haskell: an experimental comparison in security protocol analysis. In Kokichi Futatsugi, editor, Electronic Notes in Theoretical Computer Science, volume 36. Elsevier Science Publishers, 2001.","DOI":"10.1016\/S1571-0661(05)80141-0"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"D. Bolignano. Towards the formal verification of electronic commerce protocols. In Proceedings of the IEEE Computer Security Foundations Workshop, pages 133\u2013146. 1997.","DOI":"10.1109\/CSFW.1997.596802"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Cervesato, Durgin, Mitchell, Lincoln, and Scedrov. Relating strands and multiset rewriting for security protocol analysis. In PCSFW: Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer SocietyPress, 2000.","DOI":"10.3233\/JCS-2005-13203"},{"key":"14_CR6","unstructured":"John Clark and Jeremy Jacob. A Surveyof Authentication Protocol Literature: Version 1.0, 17. Nov. 1997. URL http:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz ."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Ernie Cohen. TAPS: A first-order verifier for cryptographic protocols. In Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer SocietyPress, 2000.","DOI":"10.1109\/CSFW.2000.856933"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Sebastian Moedersheim David Basin and Luca Vigan\u00f2. An on-the-fly model checker for security protocol analysis. forthcoming, 2002.","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"14_CR9","series-title":"Technical Report","volume-title":"The CAPSL Integrated Protocol Environment","author":"G. Denker","year":"2000","unstructured":"Grit Denker, Jonathan Millen, and Harald Rue\u03b2. The CAPSL Integrated Protocol Environment. Technical Report SRI-CSL-2000-02, SRI International, Menlo Park, CA, October 2000. Available at http:\/\/www.csl.sri.com\/~millen\/capsl\/ ."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Danny Dolev and Andrew Yao. On the securityof public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.","DOI":"10.1109\/TIT.1983.1056650"},{"key":"14_CR11","unstructured":"B. Donovan, P. Norris, and G. Lowe. Analyzing a libraryof security protocols using Casper and FDR. In Proceedings of the Workshop on Formal Methods and Security Protocols. 1999."},{"key":"14_CR12","unstructured":"Michael D. Ernst, Todd D. Millstein, and Daniel S. Weld. Automatic SATcompilation of planning problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pages 1169\u20131177. Morgan Kaufmann Publishers, San Francisco, 1997."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Enrico Giunchiglia, Marco Maratea, Armando Tacchella, and Davide Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Rajeev Gor\u00e9, Aleander Leitsch, and Tobias Nipkow, editors, Proceedings of IJCAR\u20192001, pages 347\u2013363. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_26"},{"issue":"1\/2","key":"14_CR14","first-page":"3","volume":"9","author":"M. Hui Lin","year":"2001","unstructured":"Mei Lin Hui and Gavin Lowe. Fault-preserving simplifying transformations for security protocols. Journal of Computer Security, 9(1\/2):3\u201346, 2001.","journal-title":"Journal of Computer Security"},{"key":"14_CR15","series-title":"Lect Notes Comput Sci","first-page":"131","volume-title":"Compiling and Verifying Security Protocols","author":"F. Jacquemard","year":"2000","unstructured":"Florent Jacquemard, Michael Rusinowitch, and Laurent Vigneron. Compiling and Verifying Security Protocols. In M. Parigot and A. Voronkov, editors, Proceedings of LPAR 2000, LNCS 1955, pages 131\u2013160. Springer-Verlag, Heidelberg, 2000."},{"key":"14_CR16","first-page":"374","volume-title":"KR\u201996: Principles of Knowledge Representation and Reasoning","author":"H. Kautz","year":"1996","unstructured":"Henry Kautz, David McAllester, and Bart Selman. Encoding plans in propositional logic. In Luigia Carlucci Aiello, Jon Doyle, and Stuart Shapiro, editors, KR\u201996: Principles of Knowledge Representation and Reasoning, pages 374\u2013384. Morgan Kaufmann, San Francisco, California, 1996."},{"issue":"1","key":"14_CR17","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G. Lowe","year":"1998","unstructured":"Gawin Lowe. Casper: a compiler for the analysis of security protocols. Journal of Computer Security, 6(1):53\u201384, 1998. See also http:\/\/www.mcs.le.ac.uk\/~gl7\/Security\/Casper\/ .","journal-title":"Journal of Computer Security"},{"issue":"2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Catherine Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):113\u2013131, 1996. See also http:\/\/chacs.nrl.navy.mil\/projects\/crypto.html .","journal-title":"Journal of Logic Programming"},{"key":"14_CR19","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Cha.: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC\u201901). 2001."},{"issue":"1","key":"14_CR20","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. Journal of Computer Security, 6(1):85\u2013128, 1998.","journal-title":"Journal of Computer Security"},{"key":"14_CR21","unstructured":"D. Song. Athena: A new efficient automatic checker for securityproto col analysis. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW\u2019 99), pages 192\u2013202. IEEE Computer SocietyPress, 1999."},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proceedings of CADE 14, LNAI 1249, pages 272\u2013275. Springer-Verlag, Heidelberg, 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36135-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T20:59:56Z","timestamp":1737061196000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36135-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001416","9783540361350"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-36135-9_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}