{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:04:49Z","timestamp":1771700689894,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540232421","type":"print"},{"value":"9783540302278","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30227-8_68","type":"book-chapter","created":{"date-parts":[[2010,9,19]],"date-time":"2010-09-19T01:34:52Z","timestamp":1284860092000},"page":"730-733","source":"Crossref","is-referenced-by-count":66,"title":["SATMC: A SAT-Based Model Checker for 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":"68_CR1","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1145\/383779.383785","volume":"2","author":"L.C. Aiello","year":"2001","unstructured":"Aiello, L.C., 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":"68_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, p. 349. Springer, Heidelberg (2002)"},{"key":"68_CR3","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L.: Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. In: Proc.of FORTE 2002 (2002)","DOI":"10.1007\/3-540-36135-9_14"},{"key":"68_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":"68_CR5","doi-asserted-by":"crossref","unstructured":"Armando, A., Compagna, L.: An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols. In: Proc. of ARSPA Workshop (2004)","DOI":"10.1007\/978-3-540-30227-8_68"},{"key":"68_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":"68_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/978-3-540-30227-8_51","volume-title":"Logics in Artificial Intelligence","author":"A. Armando","year":"2004","unstructured":"Armando, A., Compagna, L., Lierler, Y.: Automatic compilation of protocol insecurity problems into logic programming. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 617\u2013627. Springer, Heidelberg (2004)"},{"key":"68_CR8","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, p. 193. Springer, Heidelberg (1999)"},{"key":"68_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"68_CR10","unstructured":"Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0 (November 17, 1997), www.cs.york.ac.uk\/~jac\/papers\/drareview.ps.gz"},{"key":"68_CR11","unstructured":"Denker, G., Meseguer, J., Talcott, C.: Protocol specification and analysis in Maude. In: Proc. of the Workshop on Formal Methods and Security Protocols (1998)"},{"key":"68_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":"68_CR13","unstructured":"Kautz, H., McAllester, H., Selman, B.: Encoding Plans in Propositional Logic. In: Proc. of KR 1996 (1996)"},{"issue":"1","key":"68_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":"68_CR15","doi-asserted-by":"crossref","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. of the CCS 2001, pp. 166\u2013175 (2001)","DOI":"10.1145\/501983.502007"},{"key":"68_CR16","doi-asserted-by":"crossref","unstructured":"Song, D.: Athena: A new efficient automatic checker for security protocol analysis. In: Proc. of 12th Computer Security Foundation Workshop, pp. 192\u2013202 (1999)","DOI":"10.1109\/CSFW.1999.779773"}],"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_68.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:51:03Z","timestamp":1605761463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30227-8_68"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232421","9783540302278"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30227-8_68","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}