{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:53:32Z","timestamp":1725566012602},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540232421"},{"type":"electronic","value":"9783540302278"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30227-8_51","type":"book-chapter","created":{"date-parts":[[2010,9,19]],"date-time":"2010-09-19T01:34:52Z","timestamp":1284860092000},"page":"617-627","source":"Crossref","is-referenced-by-count":7,"title":["Automatic Compilation of Protocol Insecurity Problems into Logic Programming"],"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":"Yuliya","family":"Lierler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"51_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":"51_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., M\u00f6dersheim, S., Rusinowitch, M., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISS Security Protocol Analysis Tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 349\u2013354. Springer, Heidelberg (2002)"},{"key":"51_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_14","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)"},{"key":"51_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":"51_CR5","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L.: An optimized intruder model for sat-based model-checking of security protocols. To appear in the Proc. of ARSPA 2004 (2004)","DOI":"10.1007\/978-3-540-30227-8_68"},{"key":"51_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_47","volume-title":"FME 2003: Formal Methods","author":"A. Armando","year":"2003","unstructured":"Armando, A., Compagna, L., Ganty, P.: SAT-based Model-Checking of Security Protocols using Planning Graph Analysis. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, Springer, Heidelberg (2003)"},{"key":"51_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-39650-5_15","volume-title":"Computer Security \u2013 ESORICS 2003","author":"D. Basin","year":"2003","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: An On-The-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 253\u2013270. Springer, Heidelberg (2003)"},{"key":"51_CR8","unstructured":"Clark, J., Jacob, J.: ASurvey ofAuthentication Protocol Literature:Version 1.0 (November 17,1997), www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz"},{"key":"51_CR9","first-page":"251","volume-title":"Proc. of DISCEX 2000","author":"G. Denker","year":"2000","unstructured":"Denker, G., Meseguer, J., Talcott, C.: Formal specification and analysis of active networks and communication protocols: The Maude experience. In: Proc. of DISCEX 2000, pp. 251\u2013265. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"51_CR10","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":"51_CR11","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R., Bowen, K. (eds.) Logic Programming: Proc. Fifth Int\u2019l Conf. and Symp., pp. 1070\u20131080 (1988)"},{"key":"51_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/BF03037169","volume":"9","author":"M. Gelfond","year":"1991","unstructured":"Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Generation Computing\u00a09, 365\u2013385 (1991)","journal-title":"New Generation Computing"},{"key":"51_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-24609-1_32","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"Y. Lierler","year":"2003","unstructured":"Lierler, Y., Maratea, M.: Cmodels-2: SAT-based answer set solver enhanced to non-tight programs. In: Lifschitz, V., Niemel\u00e4, I. (eds.) LPNMR 2004. LNCS (LNAI), vol.\u00a02923, pp. 346\u2013350. Springer, Heidelberg (2003)"},{"issue":"1","key":"51_CR14","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G. Lowe","year":"1998","unstructured":"Lowe, G.: Casper: a Compiler for the Analysis of Security Protocols. Journal of Computer Security\u00a06(1), 53\u201384 (1998)","journal-title":"Journal of Computer Security"},{"key":"51_CR15","doi-asserted-by":"crossref","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. of CCS 2001, pp. 166\u2013175 (2001)","DOI":"10.1145\/501983.502007"},{"key":"51_CR16","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":"51_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/3-540-63255-7_32","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"I. Niemel\u00e4","year":"1997","unstructured":"Niemel\u00e4, I., Simons, P.: Smodels\u2014an implementation of the stable model and wellfounded semanics for normal logic programs. In: Fuhrbach, U., Dix, J., Nerode, A. (eds.) LPNMR 1997. LNCS (LNAI), vol.\u00a01265, pp. 420\u2013429. Springer, Heidelberg (1997)"},{"key":"51_CR18","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-1-4615-1567-8_21","volume-title":"Logic-Based Artificial Intelligence","author":"I. Niemel\u00e4","year":"2000","unstructured":"Niemel\u00e4, I., Simons, P.: Extending the Smodels system with cardinality and weight constraints. In: Minker, J. (ed.) Logic-Based Artificial Intelligence, pp. 491\u2013521. Kluwer, Dordrecht (2000)"},{"key":"51_CR19","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0004-3702(02)00187-X","volume":"138","author":"I. Niemel\u00e4","year":"2002","unstructured":"Niemel\u00e4, I., Simons, P., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence\u00a0138, 181\u2013234 (2002)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"51_CR20","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security\u00a06(1), 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"51_CR21","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1109\/CSFW.1999.779773","volume-title":"Proc. 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: Proc. of the 12th IEEE Computer Security Foundations Workshop (CSFW 1999), pp. 192\u2013202. IEEE Computer Society Press, Los Alamitos (1999)"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30227-8_51.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:51:00Z","timestamp":1605761460000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30227-8_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232421","9783540302278"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30227-8_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}