Automatic Security Analysis of SAML-Based Single Sign-On Protocols

Introduction

Single Sign-On (SSO) protocols are the cornerstones of Identity and Access Management systems as they enable companies to establish a federated environment in which users sign in once and yet are able to access to services offered by different organizations.

The Security Assertion Markup Language (SAML) 2.0 Web Browser SSO Profile (SAML SSO, for short) (OASIS, 2005a) is the emerging standard in this context: it defines an XML-based format for encoding security assertions as well as a number of protocols and bindings that prescribe how assertions should be exchanged in a wide variety of applications and/or deployment scenarios. This is done to the minimum extent necessary to guarantee the interoperability among different implementations. As a consequence, SAML SSO features many configuration options ranging from optional fields in messages, usage of SSL 3.0 or TLS 1.0 channels (SSL channels from here on) at the transport layer, application of encryption and/or digital signature on specific sensitive message elements which need to be instantiated according to the requirements posed by the application scenario and the available security mechanisms.

The security recommendations that are available throughout the bulky SAML specifications (OASIS, 2005a, 2005b) are useful in avoiding the most common security pitfalls but are of little help in ensuring their absence in specific instances of the protocol. Indeed the designer of a SAML-based SSO solution, while striving to meet the requirements posed by the application scenario, may overlook the security implications associated with the choice of some optional elements or may even decide to deviate from the SAML standard. Needless to say, this may have dramatic consequences on the security of the SSO solution.

The situation is exemplified by the SAML-based SSO for Google Apps. The protocol is inspired by the SAML standard but the version in operation until June 2008 deviated from it in a few, seemingly minor aspects (see Section «The SAML Web Browser SSO Profile» for the details). In May 2008 a severe security flaw was discovered and reported to Google and US-CERT (Armando, Carbone, Compagna, Cuéllar, & Tobarra, 2008, US-CERT, 2008). The vulnerability allowed a dishonest service provider to impersonate a user at another service provider. In reaction to the finding, Google immediately asked their customers to implement counter-measures to mitigate potential exploits and then to migrate to a new, patched solution of their SSO solution. Interestingly, the vulnerability was found by using a model checker for security protocols.

By leveraging this experience, this chapter will show that model checking techniques for security protocols can support the development and analysis of SSO solutions helping designers not only to detect serious security flaws early in the development life-cycle but also to provide assurance on the security of the solutions identified. By using SAML-based SSO protocols as running examples it will be illustrated how the design space can be iteratively explored with the aid of a model checker leading to the identification of vulnerabilities and hence to more secure solutions.

This work is part of a wider project aimed at the development of automated verification technologies for security protocols and, more generally, for security-sensitive, distributed applications (Armando et al., 2005, The AVANTSSAR Team).