Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2016

01.04.2016 | Tacas 2014

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

verfasst von: Alessandro Armando, Roberto Carbone, Luca Compagna

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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).
Vorheriger Artikel Many-core on-the-fly model checking of safety properties using GPUs
Nächster Artikel Monitoring modulo theories

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
Literatur
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)
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)
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)
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)CrossRef
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.
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.
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.
27.
Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. J. Appl. Non Class. Logics 19(4), 403–429 (2009)MathSciNetCrossRefMATH
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)
30.
Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Secur. 7(1), 3–32 (2008)CrossRef
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)
33.
Pimentel, J.C.L., Monroy, R.: Formal support to security protocol development: a survey. Comput. Sist. 12(1), 89–108 (2008)
34.
Cortier, V., Kremer, S.: Formal models and techniques for analyzing security protocols-a tutorial (2014)
35.
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.
38.
39.
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)MathSciNetCrossRefMATH
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)
Metadaten
Titel
SATMC: a SAT-based model checker for security protocols, business processes, and security APIs
verfasst von
Alessandro Armando
Roberto Carbone
Luca Compagna
Publikationsdatum
01.04.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2016
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-015-0385-y

Weitere Artikel der Ausgabe 2/2016

International Journal on Software Tools for Technology Transfer 2/2016 Zur Ausgabe

TACAS 2014

FDR3: a parallel refinement checker for CSP

TACAS 2014

Some recent advances in automated analysis

TACAS 2014

Concurrent depth-first search algorithms based on Tarjan’s Algorithm

TACAS 2014

Many-core on-the-fly model checking of safety properties using GPUs

TACAS 2014

Probabilistic verification and synthesis of the next generation airborne collision avoidance system

TACAS 2014

Monitoring modulo theories

Premium Partner

    Bildnachweise