Online citations, reference lists, and bibliographies.

Formal Analysis Of SAML 2.0 Web Browser Single Sign-on: Breaking The SAML-based Single Sign-on For Google Apps

A. Armando, R. Carbone, L. Compagna, J. Cuéllar, Llanos Tobarra
Published 2008 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
Share
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.
This paper references
OASIS SAML(Security Assertion Markup Language) v2.0 고찰 및 활용
조영섭 (2006)
10.1145/1368310.1368330
Verified implementations of the information card federated identity-management protocol
K. Bhargavan (2008)
10.1109/CSFW.1997.596782
A hierarchy of authentication specifications
G. Lowe (1997)
10.1109/MIC.2003.1250582
Analysis of Liberty Single-Sign-on with Enabled Clients
B. Pfitzmann (2003)
Available at http://shibboleth.internet2
Shibboleth Internet (2007)
10.1109/TIT.1983.1056650
On the security of public key protocols
D. Dolev (1981)
Web-based reference implementation of SAML-based SSO for Google Apps
Google (2008)
10.1007/11513988_27
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
A. Armando (2005)
Security Assertion Markup Language (SAML) v2.0. Available at http://www.oasis-open.org/ committees/tc_home.php?wg_abbrev=security
(2005)
10.1515/9783111576855-009
D
Saskia Bonjour (1824)
10.1145/1045405.1045409
Using static analysis to validate the SAML single sign-on protocol
Steffen M. Hansen (2005)
10.1007/3-540-45789-5_25
From Secrecy to Authenticity in Security Protocols
B. Blanchet (2002)
10.1109/CSAC.2003.1254334
Security analysis of the SAML single sign-on browser/artifact profile
T. Groß (2003)
10.1007/11555827_28
Browser Model for Security Analysis of Browser-Based Protocols
T. Groß (2005)
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
(2005)
10.1007/s10207-007-0041-y
SAT-based model-checking for security protocols analysis
A. Armando (2007)
Liberty Alliance Project
C. Tabin (2007)
Available at http://www.projectliberty.org/ resources/specifications.php
(2004)
10.1007/11542322_20
Federated Identity-Management Protocols
B. Pfitzmann (2003)
10.1109/CSF.2007.24
LTL Model Checking for Security Protocols
A. Armando (2007)



This paper is referenced by
10.4018/978-1-4666-2854-0.CH011
An Efficient, Robust, and Secure SSO Architecture for Cloud Computing Implemented in a Service Oriented Architecture
Khandakar Ahmed (2013)
10.1007/978-3-642-36830-1_1
Formal Analysis of Privacy for Routing Protocols in Mobile Ad Hoc Networks
Rémy Chrétien (2013)
10.1109/CSF.2014.33
Provably Sound Browser-Based Enforcement of Web Session Integrity
M. Bugliesi (2014)
Personal and Password-Based Cryptography
Kai Samelin (2018)
10.1145/2976749.2978385
A Comprehensive Formal Security Analysis of OAuth 2.0
Daniel Fett (2016)
10.1109/ITIME.2009.5236204
Digital identity control mechanism for e-learning
Jianming Yong (2009)
WPSE: Fortifying Web Protocols via Browser-Side Security Monitoring
Stefano Calzavara (2018)
10.1145/2664168.2664171
Guardians of the Clouds: When Identity Providers Fail
Andreas Mayer (2014)
10.1007/978-3-642-04444-1_21
Secure Pseudonymous Channels
S. Mödersheim (2009)
10.1109/CSF.2007.24
LTL Model Checking for Security Protocols
A. Armando (2007)
DOCTEUR DE L'UNIVERSIT E DU LUXEMBOURG EN INFORMATIQUE
Rosario Giustolisi (2015)
Automated analysis of equivalence properties for cryptographic protocols. (Analyse automatique de propriétés d'équivalence pour les protocoles cryptographiques)
Rémy Chrétien (2016)
10.1109/ICSNS.2015.7292381
Security issues of single sign on web services
Anjali N. Nair (2015)
A Comparative Study of Formal Verification Techniques for Authentication Protocols
Hernan M. Palombo (2015)
10.1109/PDP50117.2020.00074
Decidability of Deterministic Process Equivalence for Finitary Deduction Systems
Yannick Chevalier (2020)
10.1145/2046707.2046717
A composable computational soundness notion
V. Cortier (2011)
On message-level security
C. Mainka (2017)
10.1109/CSF.2010.29
Protocol Composition for Arbitrary Primitives
Stefan Ciobaca (2010)
10.1007/s10009-015-0385-y
SATMC: a SAT-based model checker for security protocols, business processes, and security APIs
Alessandro Armando (2015)
10.1109/CRISIS.2010.5764918
An intruder model for trust negotiation
Philippe Balbiani (2010)
Reward Path Deep Q Network Initial Tree Construction Verification Tree Endpoint Node SubtreeConstruction Tree Merger Correctness Determination Termination Acquisition Verification Yes YesNo Protocol Model Is path Complete ?
Yan Xiong (2019)
A formal privacy analysis of identity management systems
Meilof Veeningen (2012)
Attack-preserving Security Protocol Transformations
B. Nguyen (2012)
10.4230/LIPIcs.FSTTCS.2018.29
A Symbolic Framework to Analyse Physical Proximity in Security Protocols
A. Debant (2018)
On Breaking SAML: Be Whoever You Want to Be
Juraj Somorovsky (2012)
10.3233/JCS-140503
Discovering concrete attacks on website authorization by formal analysis
Chetan Bansal (2014)
10.23638/LMCS-13(2:8)2017
A Reduced Semantics for Deciding Trace Equivalence
David Baelde (2017)
An Analysis of sSven Concepts and Design Flaws in Identity Management Systems
João José Calixto das Chagas (2015)
10.1145/2810103.2813726
SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web
Daniel Fett (2015)
Authentication , Authorisation & Accountability ( AAA )
Dieter Gollmann ()
10.1145/2897845.2897874
Model-based Security Testing: An Empirical Study on OAuth 2.0 Implementations
R. Yang (2016)
10.1145/1655108.1655112
TruWallet: trustworthy and migratable wallet-based web authentication
Sebastian Gajek (2009)
See more
Semantic Scholar Logo Some data provided by SemanticScholar