Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps

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.

REFERENCES

• 1: A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. Heám, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05). Springer-Verlag, 2005. Available at www.avispa-project.org.
• 2: Alessandro Armando , Roberto Carbone , Luca Compagna, LTL Model Checking for Security Protocols, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.385-396, July 06-08, 2007 [doi>10.1109/CSF.2007.24]
• 3: Alessandro Armando , Luca Compagna, SAT-based model-checking for security protocols analysis, International Journal of Information Security, v.7 n.1, p.3-32, January 2008 [doi>10.1007/s10207-007-0041-y]
• 4: Karthikeyan Bhargavan , Cédric Fournet , Andrew D. Gordon , Nikhil Swamy, Verified implementations of the information card federated identity-management protocol, Proceedings of the 2008 ACM symposium on Information, computer and communications security, March 18-20, 2008, Tokyo, Japan [doi>10.1145/1368310.1368330]
• 5: Bruno Blanchet, From Secrecy to Authenticity in Security Protocols, Proceedings of the 9th International Symposium on Static Analysis, p.342-359, September 17-20, 2002
• 6: D. Dolev and A. Yao. On the Security of Public-Key Protocols. IEEE Transactions on Information Theory, 2(29), 1983.
• 7: Google. Web-based reference implementation of SAML--based SSO for Google Apps. http://code.google.com/apis/apps/sso/saml_reference_implementation_web.%html, 2008.
• 8: Thomas Groβ, Security Analysis of the SAML Single Sign-on Browser/Artifact Profile, Proceedings of the 19th Annual Computer Security Applications Conference, p.298, December 08-12, 2003
• 9: T. Groß, B. Pfitzmann, and A.-R. Sadeghi. Browser model for security analysis of browser-based protocols. In S. D. C. di Vimercati, P. F. Syverson, and D. Gollmann, editors, ESORICS, volume 3679 of Lecture Notes in Computer Science, pages 489--508. Springer, 2005.
• 10: Steffen M. Hansen , Jakob Skriver , Hanne Riis Nielson, Using static analysis to validate the SAML single sign-on protocol, Proceedings of the 2005 workshop on Issues in the theory of security, p.27-40, January 10-11, 2005, Long Beach, California [doi>10.1145/1045405.1045409]
• 11: Internet2. Shibboleth Project. Available at http://shibboleth.internet2.edu/, 2007.
• 12: Gavin Lowe, A Hierarchy of Authentication Specifications, Proceedings of the 10th IEEE workshop on Computer Security Foundations, p.31, June 10-12, 1997
• 13: OASIS. Identity Federation. Liberty Alliance Project. Available at http://www.projectliberty.org/resources/specifications.php, 2004.
• 14: OASIS. Profiles for the OASIS Security Assertion Markup Language (SAML) V2.0. Available at http://www.oasis-open.org/committees/tc_home.php?wg_abbrev=security, March 2005.
• 15: OASIS. Security Assertion Markup Language (SAML) v2.0. Available at http://www.oasis-open.org/committees/tc_home.php?wg_abbrev=security, April 2005.
• 16: Birgit Pfitzmann , Michael Waidner, Analysis of Liberty Single-Sign-on with Enabled Clients, IEEE Internet Computing, v.7 n.6, p.38-44, November 2003 [doi>10.1109/MIC.2003.1250582]
• 17: B. Pfitzmann and M. Waidner. Federated identity-management protocols. In B. Christianson, B. Crispo, J. A. Malcolm, and M. Roe, editors, Security Protocols Workshop, volume 3364 of Lecture Notes in Computer Science, pages 153--174. Springer, 2003.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.0 General
          Subjects: Security and protection (e.g., firewalls)

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification
      C.2.6 Internetworking

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  E. Data
  E.4 CODING AND INFORMATION THEORY
      Subjects: Formal models of communication

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Process models; Program analysis

  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Security
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Authentication

General Terms:
Security, Verification

Keywords:
bounded model checking, saml single sign-on, sat-based model checking, security protocols