Automated Validation of Trust and Security of Service-Oriented Architectures: how we found a vulnerability in the SAML-based Single Sign-On Protocol for Google Applications

 (Work by A. Armando, R. Carbone, L. Compagna, J. Cuellar, L. Tobarra 
Abad in the context of the FP7 Project AVANTSSAR coordinated by L. Vigano`)

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. We have provided 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. We have then 
mechanically analyzed these formal models with a state-of-the-art model 
checker for security protocols, which has revealed a severe security 
flaw in Google's implementation that allows a dishonest service provider 
to impersonate a user and get unauthorized access to Google Applications 
(and vice versa). We have reproduced this attack in an actual deployment 
of the SAML-based SSO for Google Applications.
This result demonstrates the need for a rigorous technology for the 
formal specification and automated validation of trust and security of 
service-oriented architectures such as the technology that is currently 
being developed in the AVANTSSAR project (www.avantssar.eu).