research-article

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

Authors:

Alessandro Armando,

Roberto Carbone,

Llanos TobarraAuthors Info & Claims

FMSE '08: Proceedings of the 6th ACM workshop on Formal methods in security engineering

Pages 1 - 10

https://doi.org/10.1145/1456396.1456397

Published: 27 October 2008 Publication History

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.

Digital Library

[2]

A. Armando, R. Carbone, and L. Compagna. LTL model checking for security protocols. In 20th IEEE Computer Security Foundations Symposium (CSF20), Venice (Italy), July 2007.

Digital Library

[3]

A. Armando and L. Compagna. SAT-based Model-Checking for Security Protocols Analysis. International Journal of Information Security, 7(1):3--32, January 2008.

Digital Library

[4]

K. Bhargavan, C. Fournet, A. D. Gordon, and N. Swamy. Verified implementations of the information card federated identity-management protocol. In ASIACCS, pages 123--135, 2008.

Digital Library

[5]

B. Blanchet. From secrecy to authenticity in security protocols. In In 9th International Static Analysis Symposium (SAS'02), pages 342--359. Springer, 2002.

Digital Library

[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]

T. Groß. Security analysis of the SAML Single Sign-on Browser/Artifact profile. In Proc. 19th Annual Computer Security Applications Conference. IEEE, Dec. 2003.

Digital Library

[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.

Digital Library

[10]

S. M. Hansen, J. Skriver, and H. R. Nielson. Using static analysis to validate the SAML single sign-on protocol. In WITS'05: Proceedings of the 2005 workshop on Issues in the theory of security, pages 27--40, New York, NY, USA, 2005. ACM Press.

Digital Library

[11]

Internet2. Shibboleth Project. Available at http://shibboleth.internet2.edu/, 2007.

[12]

G. Lowe. A hierarchy of authentication specifications. In Proceedings of the 10th IEEE Computer Security Foundations Workshop (CSFW'97), pages 31--43. IEEE Computer Society Press, 1997.

Digital Library

[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]

B. Pfitzmann and M. Waidner. Analysis of Liberty Single-Sign-on with Enabled Clients. IEEE Internet Computing, 7(6):38--44, 2003.

Digital Library

[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.

Digital Library

Cited By

Kovač MKovač M(2025)Introduction to the Generative Artificial Intelligence SystemsGenerative Artificial Intelligence10.1007/978-3-031-65514-2_4(59-82)Online publication date: 8-Jan-2025
https://doi.org/10.1007/978-3-031-65514-2_4
Pernpruner MCarbone RSciarretta GRanise S(2024)An Automated Multi-Layered Methodology to Assist the Secure and Risk-Aware Design of Multi-Factor Authentication ProtocolsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2023.329621021:4(1935-1950)Online publication date: Jul-2024
https://doi.org/10.1109/TDSC.2023.3296210
Fila BRadomirović S(2024)Nothing is Out-of-Band: Formal Modeling of Ceremonies2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00049(464-478)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00049
Show More Cited By

Index Terms

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

Recommendations

An authentication flaw in browser-based Single Sign-On protocols: Impact and remediations

Browser-based Single Sign-On (SSO) protocols relieve the user from the burden of dealing with multiple credentials thereby improving the user experience and the security. In this paper we show that extreme care is required for specifying and ...
SAT-based model-checking for security protocols analysis

We present a model checking technique for security protocols based on a reduction to propositional logic. At the core of our approach is a procedure that, given a description of the protocol in a multi-set rewriting formalism and a positive integer k, ...
Security Analysis of the SAML Single Sign-on Browser/Artifact Profile
ACSAC '03: Proceedings of the 19th Annual Computer Security Applications Conference

Many influential industrial players are currentlypursuing the development of new protocols for federatedidentity management. The Security AssertionMarkup Language (SAML) is an important standardizedexample of this new protocol class and will bewidely ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FMSE '08: Proceedings of the 6th ACM workshop on Formal methods in security engineering

October 2008

70 pages

ISBN:9781605582887

DOI:10.1145/1456396

Program Chair:
Vitaly Shmatikov
The University of Texas at Austin, USA

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 October 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS08

Sponsor:

CCS08: 15th ACM Conference on Computer and Communications Security 2008

October 27, 2008

Virginia, Alexandria, USA

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

147
Total Citations
View Citations
1,851
Total Downloads

Downloads (Last 12 months)76
Downloads (Last 6 weeks)6

Reflects downloads up to 03 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kovač MKovač M(2025)Introduction to the Generative Artificial Intelligence SystemsGenerative Artificial Intelligence10.1007/978-3-031-65514-2_4(59-82)Online publication date: 8-Jan-2025
https://doi.org/10.1007/978-3-031-65514-2_4
Pernpruner MCarbone RSciarretta GRanise S(2024)An Automated Multi-Layered Methodology to Assist the Secure and Risk-Aware Design of Multi-Factor Authentication ProtocolsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2023.329621021:4(1935-1950)Online publication date: Jul-2024
https://doi.org/10.1109/TDSC.2023.3296210
Fila BRadomirović S(2024)Nothing is Out-of-Band: Formal Modeling of Ceremonies2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00049(464-478)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00049
Cuzzocrea ABelmerabet I(2024)A SOLID-Based Framework for Supporting Privacy-Preserving Identity Management in Multi-Cloud Environments2024 IEEE 48th Annual Computers, Software, and Applications Conference (COMPSAC)10.1109/COMPSAC61105.2024.00375(2334-2340)Online publication date: 2-Jul-2024
https://doi.org/10.1109/COMPSAC61105.2024.00375
Almeida JZúquete APazos AOliveira J(2024)A Federated Authentication Schema among Multiple Identity ProvidersHeliyon10.1016/j.heliyon.2024.e28560(e28560)Online publication date: Mar-2024
https://doi.org/10.1016/j.heliyon.2024.e28560
Paier MVan Eeden RMiculan M(2024)Formal Analysis of Multi-Factor Authentication Schemes in Digital Identity CardsSoftware Engineering and Formal Methods10.1007/978-3-031-77382-2_24(423-440)Online publication date: 26-Nov-2024
https://doi.org/10.1007/978-3-031-77382-2_24
Sempreboni DViganò L(2023)A mutation-based approach for the formal and automated analysis of security ceremoniesJournal of Computer Security10.3233/JCS-21007531:4(293-364)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/JCS-210075
Larriba ALopez D(2023)How to Grant Anonymous AccessIEEE Transactions on Information Forensics and Security10.1109/TIFS.2022.322656118(613-625)Online publication date: 2023
https://doi.org/10.1109/TIFS.2022.3226561
Badirova ADabbaghi SMoghaddam FWieder PYahyapour R(2023)A Survey on Identity and Access Management for Cross-Domain Dynamic Users: Issues, Solutions, and ChallengesIEEE Access10.1109/ACCESS.2023.327949211(61660-61679)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3279492
Gupta BGaurav AKumar Panigrahi P(2023)Analysis of security and privacy issues of information management of big data in B2B based healthcare systemsJournal of Business Research10.1016/j.jbusres.2023.113859162(113859)Online publication date: Jul-2023
https://doi.org/10.1016/j.jbusres.2023.113859
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten