{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:51:34Z","timestamp":1743155494060,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408284"},{"type":"electronic","value":"9783540452362"}],"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\/978-3-540-45236-2_47","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:08:38Z","timestamp":1277496518000},"page":"875-893","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Compagna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"issue":"4","key":"47_CR1","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1145\/383779.383785","volume":"2","author":"L. Carlucci Aiello","year":"2001","unstructured":"Carlucci Aiello, L., Massacci, F.: Verifying security protocols as planning in logic programming. ACM Trans. on Computational Logic\u00a02(4), 542\u2013580 (2001)","journal-title":"ACM Trans. on Computational Logic"},{"key":"47_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/3-540-45657-0_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2002","unstructured":"Armando, A., Basin, D., Bouallagui, M., Chevalier, Y., Compagna, L., Moedersheim, S., Rusinowitch, M., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISS Security Protocols Analysis Tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 349. Springer, Heidelberg (2002)"},{"key":"47_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45988-X","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"A. Armando","year":"2002","unstructured":"Armando, A., Compagna, L.: Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529. Springer, Heidelberg (2002); Also presented at the FCS & Verify Workshops, Copenhagen, Denmark (July 2002)"},{"key":"47_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-540-24605-3_20","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Armando","year":"2004","unstructured":"Armando, A., Compagna, L.: Abstraction-driven SAT-based Analysis of Security Protocols. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 257\u2013271. Springer, Heidelberg (2004)"},{"key":"47_CR5","doi-asserted-by":"crossref","unstructured":"Basin, D., Moedersheim, S., Vigan\u00f2, L.: An On-the-Fly Model- Checker for security protocol analysis (2003) (forthcoming)","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"47_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"47_CR7","doi-asserted-by":"crossref","unstructured":"Blum, A., Furst, M.: Fast planning through planning graph analysis. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI 1995), pp. 1636\u20131642 (1995)","DOI":"10.21236\/ADA303260"},{"key":"47_CR8","unstructured":"Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55\u201369 (1999)"},{"key":"47_CR9","volume-title":"Proceedings of the Automated Software Engineering Conference (ASE 2001)","author":"Y. Chevalier","year":"2001","unstructured":"Chevalier, Y., Vigneron, L.: A Tool for Lazy Verification of Security Protocols. In: Proceedings of the Automated Software Engineering Conference (ASE 2001), France). IEEE Computer Society Press, Los Alamitos (2001); Long version available as Technical Report A01- R-140, LORIA, Nancy (France)"},{"key":"47_CR10","unstructured":"Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0, November 17 (1997), \n\nhttp:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz"},{"key":"47_CR11","unstructured":"Do, M.B., Srivastava, B., Kambhampati, S.: Investigating the effect of relevance and reachability constraints on SAT encodings of planning. Artificial Intelligence Planning Systems, 308\u2013314 (2000)"},{"key":"47_CR12","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory\u00a02(29) (1983)","DOI":"10.1109\/TIT.1983.1056650"},{"key":"47_CR13","unstructured":"Donovan, B., Norris, P., Lowe, G.: Analyzing a library of security protocols using Casper and FDR. In: Proceedings of the Workshop on Formal Methods and Security Protocols (1999)"},{"key":"47_CR14","first-page":"1169","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997)","author":"M.D. Ernst","year":"1997","unstructured":"Ernst, M.D., Millstein, T.D., Weld, D.S.: Automatic SATcompilation of planning problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), pp. 1169\u20131177. Morgan Kaufmann Publishers, San Francisco (1997)"},{"key":"47_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45744-5_26","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A., Zambonin, D.: Evaluating search heuristics and optimization techniques in propositional satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 347\u2013363. Springer, Heidelberg (2001)"},{"key":"47_CR16","volume-title":"PCSFW: Proceedings of The 13th Computer Security Foundations Workshop","author":"J. Heather","year":"2000","unstructured":"Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: PCSFW: Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"47_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-44404-1_10","volume-title":"Logic for Programming and Automated Reasoning","author":"F. Jacquemard","year":"2000","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 131\u2013160. Springer, Heidelberg (2000)"},{"key":"47_CR18","first-page":"374","volume-title":"KR 1996: Principles of Knowledge Representation and Reasoning","author":"H. Kautz","year":"1996","unstructured":"Kautz, H., McAllester, D., Selman, B.: Encoding plans in propositional logic. In: KR 1996: Principles of Knowledge Representation and Reasoning, pp. 374\u2013384. Morgan Kaufmann, San Francisco (1996)"},{"key":"47_CR19","first-page":"318","volume-title":"Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI 1999)","author":"H.A. Kautz","year":"1999","unstructured":"Kautz, H.A., Selman, B.: Unifying SAT-based and graph-based planning. In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI 1999), Stockholm, Sweden, July 31-August 6, pp. 318\u2013325. Morgan Kaufmann, San Francisco (1999)"},{"key":"47_CR20","series-title":"Lecture Notes in Computer Science","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":"Lowe, G.: Breaking and fixing the Needham-Shroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"47_CR21","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using murphi. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 141\u2013153 (1997)"},{"key":"47_CR22","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"47_CR23","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Technical Report CSL-78-4, Xerox Palo Alto Research Center, Palo Alto, CA, USA, 1978. Reprinted (June 1982)"},{"key":"47_CR24","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/CSFW.1999.779773","volume-title":"Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 1999)","author":"D. Song","year":"1999","unstructured":"Song, D.: Athena: A new efficient automatic checker for security protocol analysis. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 1999), pp. 192\u2013202. IEEE Computer Society Press, Los Alamitos (1999)"},{"issue":"2","key":"47_CR25","first-page":"93","volume":"20","author":"D.S. Weld","year":"1999","unstructured":"Weld, D.S.: Recent advances in AI planning. AI Magazine\u00a020(2), 93\u2013123 (1999)","journal-title":"AI Magazine"},{"key":"47_CR26","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,23]],"date-time":"2020-01-23T13:07:31Z","timestamp":1579784851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_47","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":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}