Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps

Alessandro Armando (University of Genova, Italy), Roberto Carbone (University of Genova, Italy), Luca Compagna (SAP Research, France), Jorge Cuellar (Siemens AG, Germany), Llanos Tobarra Abad (Universidad de Castilla-La Mancha, Spain)

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.

Presented at the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), October 27th, 2008, Hilton Alexandria Mark Center, Virginia, USA.

BibTeX PDF

Demo


We are grateful to the following people who contributed to the realization of the video: Roberto Basile (implementation) and Sophie Galbraith (voice).

Further information


This work is partially supported by the FP7-ICT-2007-1 Project no. 216471, AVANTSSAR: Automated Validation of Trust and Security of Service-oriented Architectures
Alessandro Armando's Home Page