Skip to main content
Log in

SATMC: a SAT-based model checker for security protocols, business processes, and security APIs

  • Tacas 2014
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

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).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Notes

  1. http://scn.sap.com/docs/DOC-32838.

  2. http://www.kb.cert.org/vuls/id/612636.

  3. http://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2008-3891.

  4. http://tools.oasis-open.org/issues/browse/SECURITY-12.

  5. http://javadoc.iaik.tugraz.at/pkcs11_wrapper/1.2.15/iaik/pkcs/pkcs11/wrapper/PKCS11.html.

  6. http://cryptosense.com/.

References

  1. 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)

    Google Scholar 

  2. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS’99. LNCS, vol. 1579. Springer (1999)

  3. 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)

  4. Holzmann, Gerard: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)

    Google Scholar 

  5. 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)

  6. Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.), Term rewriting and applications. LNCS, vol. 4098. pp. 277–286. Springer (2006)

  7. Basin, D., Mödersheim, S., Viganò, L.: OFMC: A symbolic model-checker for security protocols. Int. J. Inf. Secur. 4(30), 181–208 (2004)

    Google Scholar 

  8. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Computer Security Foundations Workshop (CSFW). pp. 82–96 (2001)

  9. 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)

  10. 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)

  11. 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)

  12. Viganò, L.: The SPaCIoS project: secure provision and consumption in the internet of services. In: ICST’13. pp. 497–498 (2013)

  13. 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)

  14. 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)

  15. 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)

    Article  Google Scholar 

  16. 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)

  17. AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v. 1. http://www.avantssar.eu (2008)

  18. 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)

  19. 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)

  20. OASIS Consortium. SAML V2.0 Technical Overview. http://wiki.oasis-open.org/security/Saml2TechOverview (2008)

  21. 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)

  22. 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)

  23. Compagna, L., Guilleminot, P., Brucker, A.D.: Business process compliance via security validation as a service. In: ICST’13. pp. 455–462 (2013)

  24. RSA Sec. Inc. PKCS#11: Cryptographic Token Interface Standard v2.20, (2004)

  25. 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)

  26. Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  27. Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. J. Appl. Non Class. Logics 19(4), 403–429 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  28. Blum, A., Furst, M.: Fast planning through planning graph analysis. In: Proceedings International Joint Conference on Artificial Intelligence (IJCAI 95) (1995)

  29. 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)

    Google Scholar 

  30. Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Secur. 7(1), 3–32 (2008)

    Article  Google Scholar 

  31. 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)

  32. 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)

    Google Scholar 

  33. Pimentel, J.C.L., Monroy, R.: Formal support to security protocol development: a survey. Comput. Sist. 12(1), 89–108 (2008)

    Google Scholar 

  34. Cortier, V., Kremer, S.: Formal models and techniques for analyzing security protocols-a tutorial (2014)

  35. 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/

  36. 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)

  37. CSP–Communicating Sequential Processes. http://www.formal.demon.co.uk/CSP.html

  38. FDR2 System—Failures-Divergence Refinement. http://www.formal.demon.co.uk/CSP.html

  39. Cremers, C.J.F.: Scyther documentation. http://www.win.tue.nl/~ccremers/scyther

  40. 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)

  41. 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)

  42. 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)

  43. 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)

  44. Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols. Theor. Comput. Sci. 283(2), 419–450 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  45. Steel, G.: Formal analysis of security APIs (2011)

  46. Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1–43 (2006)

    Google Scholar 

Download references

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

Authors

Corresponding author

Correspondence to Roberto Carbone.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

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

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-015-0385-y

Keywords

Navigation