SAT-based Model-Checking of Security Protocols: Publications

1. Alessandro Armando, Roberto Carbone, Luca Compagna, Jorge Cuellar, and Llanos Tobarra Abad. Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In the proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), October 27 2008, Alexandria, VA, US. Pages: 1-9 Copyright © ACM SIGSAC.
   
   Abstract. Single-Sign-On (SSO) protocols enable companies to establish a federated environment in which clients sign in the system once and yet are able to access to services offered by different companies. The OASIS Security Assertion Markup Language (SAML) 2.0 Web Browser SSO Profile is the emerging standard in this context. In this paper we provide formal models of the protocol corresponding to one of the most applied use case scenario (the SP-Initiated SSO with Redirect/POST Bindings) and of a variant of the protocol implemented by Google and currently in use by Google's customers (the SAML-based SSO for Google Applications). We have mechanically analysed these formal models with SATMC, a state-of-the-art model checker for security protocols. SATMC has revealed a severe security flaw in the protocol used by Google that allows a dishonest service provider to impersonate a user at another service provider. We have also reproduced this attack in an actual deployment of the SAML-based SSO for Google Applications. This security flaw of the SAML-based SSO for Google Applications was previously unknown.
   [pdf, bibentry]
   
   Note: Here are more details on the Google Apps's security vulnerability including a video of the demo reproducing the attack on the real service. (A compressed version of the video is available here.)
2. Alessandro Armando, and Luca Compagna. SAT-based Model-Checking for Security Protocols Analysis. International Journal of Information Security. ISSN 1615-5262. 21 September 2007. Copyright © SpringerLink.
   
   Abstract. We present a model checking technique for security protocols based on a reduction to propositional logic. At the core of our approach is a procedure that, given a description of the protocol in a multi-set rewriting formalism and a positive integer k, builds a propositional formula whose models (if any) correspond to attacks on the protocol. Thus, finding attacks on protocols boils down to checking a propositional formula for satisfiability, problem that is usually solved very efficiently by modern SAT solvers. Experimental results indicate that the approach scales up to industrial strength security protocols with performance comparable with (and in some cases superior to) that of other state-of-the-art protocol analysers.
   [ps, pdf, bibentry]
3. Alessandro Armando, Roberto Carbone, and Luca Compagna. LTL Model Checking for Security Protocols. In the proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF 2007), July 6-8 2007, Venice, Italy. Pages: 385-396 Copyright © IEEE Computer Society.
   
   Abstract. Most model checking techniques for security protocols make a number of simplifying assumptions on the protocol and/or on its execution environment that prevent their applicability in some important cases. For instance, most techniques assume that communication between honest principals is controlled by a Dolev-Yao intruder, i.e. a malicious agent capable to overhear, divert, and fake messages. Yet we might be interested in establishing the security of a protocol that relies on a less unsecure channel (e.g. a confidential channel provided by some other protocol sitting lower in the protocol stack). In this paper we propose a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as complex security properties that are normally not handled by state-of-the-art protocol analysers. By using our approach we have been able to formalise all the assumptions required by the ASW protocol for optimistic fair exchange as well as some of its security properties. Besides the previously reported attacks on the protocol, we report a new attack on a patched version of the protocol.
   [ps, pdf, bibentry]
4. Luca Compagna. SAT-based Model-Checking of Security Protocols. Ph.D. Thesis. Joint work between Università degli Studi di Genova and the University of Edinburgh, September 2005.
   
   Abstract. Security protocols are communication protocols that aim at providing security guarantees through the application of cryptographic primitives. Since these protocols are at the core of security-sensitive applications in a variety of domains (e.g. health-care, e-commerce, and e-government), their proper functioning is crucial as a failure may undermine the customer and, more in general, the public trust in these applications. In spite of their apparent simplicity, security protocols are notoriously error-prone. It is thus of utmost importance to have tools and specification languages that support the activity of finding flaws in protocols. This thesis presents an high level protocol specification language accessible to protocol designers and easily translatable into a lower-level formalism for protocol insecurity problems. This thesis shows that automatic SATbased model-checking techniques based on a reduction of protocol insecurity problems to propositional satisfiability problems (SAT) can be used effectively to find attacks on security protocols. The approach results from the combination of a reduction of protocol insecurity problems into planning problems and SAT-encoding techniques developed for planning. A modelchecker, SATMC, based on these ideas has been developed and experimental results obtained by running SATMC against industrial-scale security protocols confirm the effectiveness of the approach.
   [ps, pdf, bibentry]
5. Alessandro Armando and Luca Compagna. An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols. ENTCS volume 125, issue 1, pages 91-108, 3 March 2005. Copyright © Elsevier B.V. Presented to the Automated Reasoning for Security Protocol Analysis Workshop (ARSPA 2005), July 04 2004, Cork, Irland.
   
   Abstract. In previous work we showed that automatic SAT-based model-checking techniques based on a reduction of protocol (in)security problems to a sequence of propositional satisfiability problems can be used to effectively find attacks on protocols. In this paper we present an optimized intruder model that may lead in many cases to shorter attacks which can be detected in our framework by generating smaller propositional formulae. The key idea is to assume that some of the abilities of the intruder have instantaneous effect, whereas in the previously adopted approach all the abilities of the intruder were modeled as state transitions. This required non trivial extensions to the SAT-reduction techniques which are formally described in the paper. Experimental results indicate the advantages of the proposed optimization.
   [ps, pdf, bibentry]
6. Alessandro Armando, Luca Compagna, and Yuliya Lierler. Automatic Compilation of Protocol Insecurity Problems into Logic Programming. In the proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), September 27-30 2004, Lisbon, Portugal. LNCS 3229, pages 730-733. Copyright © Springer-Verlag.
   
   Abstract. We describe SATMC, a SAT-based model checker for the automatic analysis of security protocols. Given as input the specification of a security protocol and of the associated security property, SATMC generates a sequence of propositional formulae whose models (quickly found by means of state-of-the-art SAT-solvers) correspond to attacks on the protocol. We provide experimental results that show the effectiveness of the tool.
   [ps, pdf, bibentry]
7. Alessandro Armando and Luca Compagna. SATMC: a SAT-based Model Checker for Security Protocols. In the proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), September 27-30 2004, Lisbon, Portugal. LNCS 3229, pages 730-733. Copyright © Springer-Verlag.
   
   Abstract. We describe SATMC, a SAT-based model checker for the automatic analysis of security protocols. Given as input the specification of a security protocol and of the associated security property, SATMC generates a sequence of propositional formulae whose models (quickly found by means of state-of-the-art SAT-solvers) correspond to attacks on the protocol. We provide experimental results that show the effectiveness of the tool.
   [ps, pdf, bibentry]
8. Alessandro Armando and Luca Compagna. "Abstraction-driven SAT-based Analysis of Security Protocols".
   In LNCS 2919 - Theory and Applications of Satisfiability Testing, Selected Paper, 2004. Copyright © Springer-Verlag. Presented to SAT 2003, May 5-8 2003, S.Margherita Ligure, Italy.
   Abstract. In previous work we proposed an approach to the automatic translation of protocol insecurity problems into propositional logic with the ultimate goal of building an automatic model-checker for security protocols based on state-of-the-art SAT solvers. In this paper we present an improved procedure based on an abstraction/refinement strategy which, by interleaving the encoding and solving phases, leads to a significant improvement of the overall performance of our model-checker.
   [ps, pdf, bibentry]
9. Alessandro Armando, Luca Compagna and Pierre Ganty. SAT-based Model-Checking of Security Protocols using Planning Graph Analysis. In the proceedings of the 12th International FME Symposium (FME 2003) , September 8-14 2003, Pisa, Italy. LNCS 2805, pages 875-893. Copyright © Springer-Verlag.
   
   Abstract. In previous work we showed that automatic SAT-based model-checking techniques based on a reduction of protocol insecurity problems to satisfiability problems in propositional logic (SAT) can be used effectively to find attacks on security protocols. The approach results from the combination of a reduction of protocol insecurity problems to planning problems and well-known SAT-reduction techniques, called linear encodings, developed for planning. Experimental results confirmed the effectiveness of the approach but also showed that the time spent to generate the SAT formula largely dominates the time spent by the SAT solver to check its satisfiability. Moreover, the SAT instances generated by the tool get of unmanageable size on the most complex protocols. In this paper we explore the application of the Graphplan-based encoding technique to the analysis of security protocols and present experimental data showing that Graphplan-based encodings are considerably (i.e.up to 2 orders of magnitude) smaller than linear encodings. These results confirm the effectiveness of the SAT-based approach to the analysis of security protocols and pave the way to its application to large protocols arising in practical applications.
   [ps, pdf, bibentry]
10. Alessandro Armando and Luca Compagna. Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning.In the Proceedings of Formal Techniques for Networked and Distributed Systems (FORTE 2002), November 11-14 2002, Houston, Texas. LNCS 2529, pages 210-225. Copyright © Springer-Verlag.
    
    Abstract. We provide a fully automatic translation from security protocol specifications into propositional logic which can be effectively used to find attacks to protocols. Our approach results from the combination of a reduction of protocol insecurity problems to planning problems and well-known SAT-reduction techniques developed for planning. We also propose and discuss a set of transformations on protocol insecurity problems whose application has a dramatic effect on the size of the propositional encoding obtained with our SAT-compilation technique. We describe a model-checker for security protocols based on our ideas and show that attacks to a set of well-known authentication protocols are quickly found by state-of-the-art SAT solvers.
    [ps, pdf, bibentry]