{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:35:36Z","timestamp":1725561336350},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208518"},{"type":"electronic","value":"9783540246053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_20","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T04:50:35Z","timestamp":1280379035000},"page":"257-271","source":"Crossref","is-referenced-by-count":9,"title":["Abstraction-Driven SAT-based Analysis of Security Protocols"],"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"}]}],"member":"297","reference":[{"issue":"4","key":"20_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":"20_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":"20_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":"20_CR4","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. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, Springer, Heidelberg (2003)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Basin, D., Denker, G.: Maude versus haskell: an experimental comparison in security protocol analysis. In: Futatsugi, K. (ed.). Electronic Notes in Theoretical Computer Science, vol.\u00a036, Elsevier Science Publishers, Amsterdam (2001)","DOI":"10.1016\/S1571-0661(05)80141-0"},{"key":"20_CR6","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":"20_CR7","doi-asserted-by":"crossref","unstructured":"Bolignano, D.: Towards the formal verification of electronic commerce protocols. In: Proc.of the IEEE Computer Security Foundations Workshop, pp. 133\u2013146 (1997)","DOI":"10.1109\/CSFW.1997.596802"},{"key":"20_CR8","volume-title":"PCSFW: Proceedings of The 13th Computer Security Foundations Workshop","author":"Cervesato","year":"2000","unstructured":"Cervesato, Durgin, Mitchell, Lincoln, Scedrov: Relating strands and multiset rewriting for security protocol analysis. In: PCSFW: Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"20_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). IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"20_CR10","unstructured":"Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0 (November 17, 1997), http:\/\/www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2002","unstructured":"Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 265. Springer, Heidelberg (2002)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Cohen, E.: TAPS: A first-order verifier for cryptographic protocols. In: Proc. of The 13th Computer Security Foundations Workshop (2000)","DOI":"10.1109\/CSFW.2000.856933"},{"key":"20_CR13","first-page":"21","volume-title":"Proceedings of the 11th AAAI Conference","author":"J.M. Crawford","year":"1993","unstructured":"Crawford, J.M., Anton, L.D.: Experimental results on the crossover point in satisfiability problems. In: Fikes, R., Lehnert, W. (eds.) Proceedings of the 11th AAAI Conference, California, pp. 21\u201327. AAAI Press, Menlo Park (1993)"},{"key":"20_CR14","unstructured":"Denker, G., Millen, J., Rue\u00df, H.: 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":"20_CR15","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":"20_CR16","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":"20_CR17","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 SAT compilation 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":"20_CR18","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":"20_CR19","volume-title":"PCSFW: Proceedings of The 13th Computer Security Foundations Workshop","author":"Heather","year":"2000","unstructured":"Heather, Lowe, Schneider: 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":"20_CR20","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":"20_CR21","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":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"1","key":"20_CR23","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":"20_CR24","doi-asserted-by":"crossref","unstructured":"Marrero, W., Clarke, E., Jha, S.: Model checking for security protocols (1997)","DOI":"10.21236\/ADA327281"},{"issue":"2","key":"20_CR25","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of Logic Programming"},{"key":"20_CR26","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using murphi. In: Proc. of IEEE Symposium on Security and Privacy, pp. 141\u2013153 (1997)"},{"key":"20_CR27","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":"20_CR28","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)"},{"issue":"1","key":"20_CR29","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":"20_CR30","doi-asserted-by":"crossref","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)"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:54:19Z","timestamp":1559332459000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}