Abstract
We present SATMC 3.0, a SAT-based bounded model checker for security-critical systems that stems from a successful combination of encoding techniques originally developed for planning with techniques developed for the analysis of reactive systems. SATMC has been successfully applied in a variety of application domains (security protocols, security-sensitive business processes, and cryptographic APIs) and for different purposes (design-time security analysis and security testing). SATMC strikes a balance between general purpose model checkers and security protocol analyzers as witnessed by a number of important success stories including the discovery of a serious man-in-the-middle attack on the SAML-based single sign-on (SSO) for Google Apps, an authentication flaw in the SAML 2.0 Web Browser SSO Profile, and a number of attacks on PKCS#11 Security Tokens. SATMC is integrated and used as back-end in a number of research prototypes (e.g., the AVISPA Tool, Tookan, the SPaCIoS Tool) and industrial-strength tools (e.g., the Security Validator plugin for SAP NetWeaver BPM).
Similar content being viewed by others
Notes
References
Kautz, H., McAllester, H., Selman, B.: Encoding plans in propositional logic. In: Aiello, L.C., Doyle, J., Shapiro, S. (eds.) KR’96: Principles of Knowledge Representation and Reasoning, pp. 374–384. Morgan Kaufmann, San Francisco (1996)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS’99. LNCS, vol. 1579. Springer (1999)
Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Proceedings European Conference on Logics in Artificial Intelligence. LNAI, vol. 3229. pp. 730–733, Lisbon, Portugal, Springer (2004)
Holzmann, Gerard: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An opensource tool for symbolic model checking. In: Proceedings International Conference on Computer-Aided Verification (CAV 2002). LNCS, vol. 2404. Springer, Copenhagen, (2002)
Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.), Term rewriting and applications. LNCS, vol. 4098. pp. 277–286. Springer (2006)
Basin, D., Mödersheim, S., Viganò, L.: OFMC: A symbolic model-checker for security protocols. Int. J. Inf. Secur. 4(30), 181–208 (2004)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW). pp. 82–96 (2001)
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Heám, P. C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA Tool for the automated validation of internet security protocols and applications. In: CAV’05. Springer (2005)
Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and fixing PKCS#11 security tokens. In: Proceedings ACM Conference on Computer and Communications Security (CCS’10). pp. 260–269, ACM Press, Chicago (2010)
Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cuéllar, J., Erzse, G., Frau, S., Minea, M., Mödersheim, S., Oheimb, D., Pellegrino, G., Ponta, S.E., Rocchetto, M., Rusinowitch, M., Torabi Dashti, M., Turuani, M., Viganò, L.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: TACAS’12. LNCS, vol. 7214, pp. 267–282. Springer, New York (2012)
Viganò, L.: The SPaCIoS project: secure provision and consumption in the internet of services. In: ICST’13. pp. 497–498 (2013)
Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. In: 20th IEEE Computer Security Foundations Symposium (CSF). pp. 385–396. IEEE Computer Society (2007)
Armando, A., Carbone, R., Compagna, L., Cuéllar, 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. (eds.), Proceedings ACM Workshop on Formal Methods in Security Engineering. pp. 1–10. ACM Press (2008)
Armando, A., Carbone, R., Compagna, L., Cuéllar, J., Pellegrino, G., Sorniotti, A.: An authentication flaw in browser-based single sign-on protocols: impact and remediations. Comput. Secur. 33, 41–58 (2013)
Armando, A., Carbone, R., Zanetti, L.: Formal modeling and automatic security analysis of two-factor and two-channel authentication protocols. In: Network and System Security (NSS). LNCS, vol. 7873. pp. 728–734. Springer (2013)
AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v. 1. http://www.avantssar.eu (2008)
Eén, N., Sörensson, N: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.), SAT. LNCS, vol. 2919. pp. 502–518. Springer (2003)
Armando, A., Carbone, R., Compagna, L.: SATMC: A SAT-based model checker for security-critical systems. In: Ábrahám, E., Havelund, K, (ed.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science. pp. 31–45. Springer (2014)
OASIS Consortium. SAML V2.0 Technical Overview. http://wiki.oasis-open.org/security/Saml2TechOverview (2008)
Armando, A., Ponta, S.E.: Model checking of security-sensitive business processes. In: Degano, P., Guttman, J.D. (ed.), Formal Aspects in Security and Trust. LNCS, 5983. pp. 66–80. Springer (2009)
Arsac, W., Compagna, L., Pellegrino, G., Ponta, S.E.: Security validation of business processes via model-checking. In: International Symposium on Engineering Secure Software and Systems (ESSoS 2011). LNCS, Springer (2011)
Compagna, L., Guilleminot, P., Brucker, A.D.: Business process compliance via security validation as a service. In: ICST’13. pp. 455–462 (2013)
RSA Sec. Inc. PKCS#11: Cryptographic Token Interface Standard v2.20, (2004)
Focardi, R., Luccio, F.L., Steel, G.: An introduction to security API analysis. In: Foundations of Security Analysis and Design—FOSAD Tutorial Lectures (FOSAD’VI). LNCS, vol. 6858. pp. 35–65 (2011)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)
Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. J. Appl. Non Class. Logics 19(4), 403–429 (2009)
Blum, A., Furst, M.: Fast planning through planning graph analysis. In: Proceedings International Joint Conference on Artificial Intelligence (IJCAI 95) (1995)
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, pp. 457–481. IOS Press, Amsterdam (2009)
Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Secur. 7(1), 3–32 (2008)
Cremers, C.J.F., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic security protocol analysis. In: Formal to practical security. pp. 70–94. Springer, Berlin (2009)
Dalal, N., Shah, J., Hisaria, K., Jinwala, D., et al.: A comparative analysis of tools for verification of security protocols. Int. J. Commun. Netw. Syst. Sci. 3(10), 779 (2010)
Pimentel, J.C.L., Monroy, R.: Formal support to security protocol development: a survey. Comput. Sist. 12(1), 89–108 (2008)
Cortier, V., Kremer, S.: Formal models and techniques for analyzing security protocols-a tutorial (2014)
Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1), 53–84 (1998). See http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Casper/
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)
CSP–Communicating Sequential Processes. http://www.formal.demon.co.uk/CSP.html
FDR2 System—Failures-Divergence Refinement. http://www.formal.demon.co.uk/CSP.html
Cremers, C.J.F.: Scyther documentation. http://www.win.tue.nl/~ccremers/scyther
Boichut, Y., Héam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the genet and klay technique to automatically verify security protocols. In: Proceedings of Automated Verification of Infinite States Systems (AVIS’04), ENTCS (2004)
Dilloway, C., Lowe, G.: On the specification of secure channels. In: Proceedings of the Workshop on Issues in the Theory of Security (WITS ’07) (2007)
Bansal, C., Bhargavan, K., Maffeis, S.: Discovering concrete attacks on website authorization by formal analysis. In: Proceedings of the 2012 IEEE 25th Computer Security Foundations Symposium, CSF ’12. pp. 247–262. IEEE Computer Society, Washington (2012)
Mödersheim, S., Viganò, L.: Secure pseudonymous channels. In: Backes, M., Ning, P. (eds.) Computer Security ESORICS 2009. Lecture Notes in Computer Science, vol. 5789, pp. 337–354. Springer, Berlin (2009)
Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols. Theor. Comput. Sci. 283(2), 419–450 (2002)
Steel, G.: Formal analysis of security APIs (2011)
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1–43 (2006)
Acknowledgments
We are grateful to Luca Zanetti for his contribution in the design and implementation of the Goal Grounding and PLTL2SAT modules. This work has partially been supported by the FP7-ICT Project SPaCIoS (No. 257876), by the PRIN project “Security Horizons” (No. 2010XSEMLC) funded by MIUR, and by the Activities “STIATE” (No. 14231) and “FIDES” (No. 15383) funded by the EIT ICT Labs.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Armando, A., Carbone, R. & Compagna, L. SATMC: a SAT-based model checker for security protocols, business processes, and security APIs. Int J Softw Tools Technol Transfer 18, 187–204 (2016). https://doi.org/10.1007/s10009-015-0385-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-015-0385-y