18/07/2008, 16:30 — 17:30 — Sala P3.10, Pavilhão de Matemática
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ò
This seminar will be held in the Alameda campus!