{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:40:40Z","timestamp":1774946440038,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548611","type":"print"},{"value":"9783642548628","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_3","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:33:34Z","timestamp":1395408814000},"page":"31-45","source":"Crossref","is-referenced-by-count":21,"title":["SATMC: A SAT-Based Model Checker for Security-Critical Systems"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Carbone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Compagna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 267\u2013282. Springer, Heidelberg (2012)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. In: 20th IEEE Computer Security Foundations Symposium (CSF), pp. 385\u2013396. IEEE Computer Society (2007)","DOI":"10.1109\/CSF.2007.24"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. In: JANCL, pp. 403\u2013429. Hermes Lavoisier (2009)","DOI":"10.3166\/jancl.19.403-429"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.cose.2012.08.007","volume":"33","author":"A. Armando","year":"2013","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Pellegrino, G., Sorniotti, A.: An Authentication Flaw in Browser-based Single Sign-On Protocols: Impact and Remediations. Computers & Security\u00a033, 41\u201358 (2013)","journal-title":"Computers & Security"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Tobarra, L.: Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In: Shmatikov, V. (ed.) Proc. ACM Workshop on Formal Methods in Security Engineering, pp. 1\u201310. ACM Press (2008)","DOI":"10.1145\/1456396.1456397"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1007\/978-3-642-38631-2_63","volume-title":"Network and System Security","author":"A. Armando","year":"2013","unstructured":"Armando, A., Carbone, R., Zanetti, L.: Formal Modeling and Automatic Security Analysis of Two-Factor and Two-Channel Authentication Protocols. In: Lopez, J., Huang, X., Sandhu, R. (eds.) NSS 2013. LNCS, vol.\u00a07873, pp. 728\u2013734. Springer, Heidelberg (2013)"},{"key":"3_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1007\/978-3-540-30227-8_68","volume-title":"Logics in Artificial Intelligence","author":"A. Armando","year":"2004","unstructured":"Armando, A., Compagna, L.: SATMC: A SAT-Based Model Checker for Security Protocols. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 730\u2013733. Springer, Heidelberg (2004)"},{"issue":"1","key":"3_CR9","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10207-007-0041-y","volume":"7","author":"A. Armando","year":"2008","unstructured":"Armando, A., Compagna, L.: SAT-based Model-Checking for Security Protocols Analysis. International Journal of Information Security\u00a07(1), 3\u201332 (2008)","journal-title":"International Journal of Information Security"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-12459-4_6","volume-title":"Formal Aspects in Security and Trust","author":"A. Armando","year":"2010","unstructured":"Armando, A., Ponta, S.E.: Model Checking of Security-Sensitive Business Processes. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol.\u00a05983, pp. 66\u201380. Springer, Heidelberg (2010)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-19125-1_3","volume-title":"Engineering Secure Software and Systems","author":"W. Arsac","year":"2011","unstructured":"Arsac, W., Compagna, L., Pellegrino, G., Ponta, S.E.: Security Validation of Business Processes via Model-Checking. In: Erlingsson, \u00da., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol.\u00a06542, pp. 29\u201342. Springer, Heidelberg (2011)"},{"key":"3_CR12","unstructured":"AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v.1 (2008), http:\/\/www.avantssar.eu"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A Symbolic Model-Checker for Security Protocols. International Journal of Information Security (2004)","DOI":"10.1007\/s10207-004-0055-7"},{"key":"3_CR14","unstructured":"Biere, A.: Bounded Model Checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 457\u2013481. IOS Press (2009)"},{"key":"3_CR15","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":"3_CR16","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: Computer Security Foundations Workshop (CSFW), pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Blum, A., Furst, M.: Fast Planning Through Planning Graph Analysis. In: Proc. International Joint Conference on Artificial Intelligence, IJCAI 1995 (1995)","DOI":"10.21236\/ADA303260"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and Fixing PKCS#11 Security Tokens. In: Proc. ACM Conference on Computer and Communications Security (CCS 2010), Chicago, USA, pp. 260\u2013269. ACM Press (2010)","DOI":"10.1145\/1866307.1866337"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Compagna, L., Guilleminot, P., Brucker, A.D.: Business Process Compliance via Security Validation as a Service. In: ICST 2013, pp. 455\u2013462 (2013)","DOI":"10.1109\/ICST.2013.63"},{"key":"3_CR21","unstructured":"OASIS Consortium. SAML V2.0 Technical Overview (March 2008), http:\/\/wiki.oasis-open.org\/security\/Saml2TechOverview"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-23082-0_2","volume-title":"Foundations of Security Analysis and Design VI","author":"R. Focardi","year":"2011","unstructured":"Focardi, R., Luccio, F.L., Steel, G.: An Introduction to Security API Analysis. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol.\u00a06858, pp. 35\u201365. Springer, Heidelberg (2011)"},{"key":"3_CR24","unstructured":"Holzmann, G.: The Spin model checker: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)"},{"key":"3_CR25","unstructured":"RSA Se: Inc. PKCS#11: Cryptographic Token Interface Standard v2.20 (2004)"},{"key":"3_CR26","unstructured":"Kautz, H., McAllester, H., Selman, B.: Encoding Plans in Propositional Logic. In: Aiello, L.C., Doyle, J., Shapiro, S. (eds.) KR 1996: Principles of Knowledge Representation and Reasoning, pp. 374\u2013384. Morgan Kaufmann (1996)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M. Turuani","year":"2006","unstructured":"Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 277\u2013286. Springer, Heidelberg (2006)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Vigan\u00f2, L.: The SPaCIoS Project: Secure Provision and Consumption in the Internet of Services. In: ICST 2013, pp. 497\u2013498 (2013)","DOI":"10.1109\/ICST.2013.75"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:46:58Z","timestamp":1746157618000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}