Information Security Seminar 

18/07/2008, 16:30 — 17:30 — Room P3.10, Mathematics Building
Luca Viganò, Università di Verona

Formal Analysis of a SAML Web Browser Single Sign-On Protocol

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 Security Assertion Markup Language (SAML) 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 used use case scenario (the SP-Initiated SSO with Redirect/POST Bindings) and of the implementation used by SAML-based SSO for Google Applications. In the context of the AVANTSSAR project, we have techanically 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 Google's implementation that allows a dishonest service provider to impersonate a user and get unauthorized access to Google Applications (and viceversa). We have reproduced this attack in an actual deployment of the SAML-based SSO for Google Applications. To the best of our knowledge this security flaw of the SAML-based SSO for Google Applications was previously unknown. This work was carried out by A. Armando, R. Carbone, L. Compagna, J. Cuellar, L. Tobarra Abad in the context of the FP7 Project AVANTSSAR coordinated by L. Viganò