Online citations, reference lists, and bibliographies.

An Expressive Model For The Web Infrastructure: Definition And Application To The Browser ID SSO System

Daniel Fett, Ralf Küsters, Guido Schmitz
Published 2014 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
Share
The web constitutes a complex infrastructure and, as demonstrated by numerous attacks, rigorous analysis of standards and web applications is indispensable. Inspired by successful prior work, in particular the work by Akhawe et al. as well as Bansal et al., in this work we propose a formal model for the web infrastructure. While unlike prior works, which aim at automatic analysis, our model so far is not directly amenable to automation, it is much more comprehensive and accurate with respect to the standards and specifications. As such, it can serve as a solid basis for the analysis of a broad range of standards and applications. As a case study and another important contribution of our work, we use our model to carry out the first rigorous analysis of the Browser ID system (a.k.a. Mozilla Persona), a recently developed complex real-world single sign-on system that employs technologies such as AJAX, cross-document messaging, and HTML5 web storage. Our analysis revealed a number of very critical flaws that could not have been captured in prior models. We propose fixes for the flaws, formally state relevant security properties, and prove that the fixed system in a setting with a so-called secondary identity provider satisfies these security properties in our model. The fixes for the most critical flaws have already been adopted by Mozilla and our findings have been rewarded by the Mozilla Security Bug Bounty Program.
This paper references
Cross-Origin Resource Sharing -W3C Recommendation 29
(2013)
AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations
Guangdong Bai (2013)
10.1145/1315245.1315254
Dynamic pharming attacks and locked same-origin policies for web browsers
C. Karlof (2007)
10.1145/1045405.1045409
Using static analysis to validate the SAML single sign-on protocol
Steffen M. Hansen (2005)
10.1007/978-3-642-30885-7_1
Contribution to a Rigorous Analysis of Web Application Frameworks
E. Börger (2012)
10.1145/2420950.2420993
Using automated model analysis for reasoning about security of web protocols
Apurva Kumar (2012)
The Postman Always Rings Twice: Attacking and Defending postMessage in HTML5 Websites
Sooel Son (2013)
10.1007/3-540-46002-0_2
Alloy: A New Technology for Software Modelling
Daniel Jackson (2002)
Web Storage - W3C Recommendation 30
(2013)
Universally Composable Security Analysis of OAuth v2.0
S. Chari (2011)
An Expressive Model for the Web Infrastructure: Definition and Application to the BrowserID SSO System
D. Fett (2014)
OpenID Foundation website
W3C Candidate Recommendation
Web Html (2012)
10.1109/CSF.2012.27
Discovering Concrete Attacks on Website Authorization by Formal Analysis
Chetan Bansal (2012)
Security Analysis of OpenID
Pavol Sovis (2010)
10.1145/1456396.1456397
Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps
A. Armando (2008)
Mozilla Identity Team. Persona. Mozilla Developer Network. Last visited
(2013)
10.1145/2382196.2382238
The devil is in the (implementation) details: an empirical analysis of OAuth SSO systems
San-Tsai Sun (2012)
An Expressive Model for the Web Infrastructure: Definition and Application to the Browser ID SSO System
Daniel Fett (2014)
10.1145/360204.360213
Mobile values, new names, and secure communication
M. Abadi (2001)
10.3233/JCS-2004-12203
Multiset rewriting and the complexity of bounded security protocols
N. Durgin (2004)
10.1109/EDOC.2011.26
OpenID and the Enterprise: A Model-Based Analysis of Single Sign-On Authentication
Jacob Bellamy-McIntyre (2011)
Cross-Origin Resource Sharing -W3C Recommendation 29 Available at http://www
(2013)
10.1007/978-3-642-36830-1_7
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage
Chetan Bansal (2013)
10.1109/SP.2011.26
How to Shop for Free Online -- Security Analysis of Cashier-as-a-Service Based Web Stores
Rui Wang (2011)
Featherweight Firefox: Formalizing the Core of a Web Browser
A. Bohannon (2010)
10.1109/CSFW.2001.930138
An efficient cryptographic protocol verifier based on prolog rules
B. Blanchet (2001)
10.1109/CSAC.2003.1254334
Security analysis of the SAML single sign-on browser/artifact profile
T. Groß (2003)
10.1109/CSF.2010.27
Towards a Formal Foundation of Web Security
Devdatta Akhawe (2010)
10.1109/SP.2012.30
Signing Me onto Your Accounts through Facebook and Google: A Traffic-Guided Security Study of Commercially Deployed Single-Sign-On Web Services
R. Wang (2012)
The Emperor ’ s New APIs : On the ( In ) Secure Usage of New Client-side Primitives
Steve Hanna (2010)
10.1016/j.cose.2012.02.005
Systematically breaking and fixing OpenID security: Formal analysis, semi-automated empirical evaluation, and practical countermeasures
San-Tsai Sun (2012)
10.1109/SECCOM.2007.4550368
Simple cross-site attack prevention
F. Kerschbaum (2007)



This paper is referenced by
Automatic recognition, processing and attacking of single sign-on protocols with burp suite
C. Mainka (2015)
Synthesis of Property-Preserving Mappings
Eunsuk Kang (2017)
10.1109/MCOM.2016.7514160
Characterization of web single sign-on protocols
V. Beltran (2016)
10.1109/EuroSP.2016.33
Do Not Trust Me: Using Malicious IdPs for Analyzing and Attacking Single Sign-on
C. Mainka (2016)
10.1007/978-3-319-10082-1
Foundations of Security Analysis and Design VII
A. Aldini (2014)
10.1109/ACCESS.2019.2920675
Towards Further Formal Foundation of Web Security: Expression of Temporal Logic in Alloy and Its Application to a Security Model With Cache
Hayato Shimamoto (2019)
10.1109/SecDev.2016.017
Design Space Exploration for Security
E. Kang (2016)
10.1145/2976749.2978385
A Comprehensive Formal Security Analysis of OAuth 2.0
Daniel Fett (2016)
On the security of authentication protocols on the web. (La sécurité des protocoles d'authentification sur leWeb)
Antoine Delignat-Lavaud (2016)
10.1145/2810103.2813726
SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web
Daniel Fett (2015)
10.1109/EuroSP.2017.32
SoK: Single Sign-On Security — An Evaluation of OpenID Connect
C. Mainka (2017)
10.1007/978-3-319-89722-6_8
Design, Formal Specification and Analysis of Multi-Factor Authentication Solutions with a Single Sign-On Experience
Giada Sciarretta (2018)
10.1109/CSF.2017.20
The Web SSO Standard OpenID Connect: In-depth Formal Security Analysis and Security Guidelines
Daniel Fett (2017)
10.1016/j.jlamp.2016.08.006
Formal methods for web security
Michele Bugliesi (2017)
10.1145/3184558.3186232
Surviving the Web: A Journey into Web Session Security
S. Calzavara (2018)
Analysis and prevention of security threats in web and cryptographic applications
M. Squarcina (2018)
Comparative Analysis and Framework Evaluating Web Single Sign-On Systems
Furkan Alaca (2018)
10.1007/978-3-319-24174-6_3
Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web
Daniel Fett (2015)
10.1109/SecDev.2016.035
Self-Verifying Execution (Position Paper)
Matt McCutchen (2016)
Browser-to-Browser Authentication and Trust Relationships for WebRTC
Ibrahim Tariq Javed (2016)
Towards secure and standard-compliant implementations of the PSD2 Directive
Tobias Wich (2017)
10.1007/978-3-030-25540-4_12
Automated Synthesis of Secure Platform Mappings
Eunsuk Kang (2019)
10.1109/BIGCOM.2017.50
A Verified Secure Protocol Model of OAuth Dynamic Client Registration
Caimei Wang (2017)
10.3929/ethz-b-000372337
Modelling and Analysis of Web Applications in Tamarin
Sandra Dünki (2019)
On message-level security
C. Mainka (2017)
10.1007/978-3-030-02450-5_31
Analyzing Security and Privacy in Design and Implementation of Web Authentication Protocols
Kailong Wang (2018)
10.1109/CESYS.2016.7889983
A novel approach to provide Web page recommendation using domain knowledge and web usage knowledge
P. L. Kolekar (2016)
10.14722/NDSS.2015.23295
Run-time Monitoring and Formal Analysis of Information Flows in Chromium
Lujo Bauer (2015)
10.1145/2736277.2741089
Network-based Origin Confusion Attacks against HTTPS Virtual Hosting
Antoine Delignat-Lavaud (2015)
Towards High Assurance HTML5 Applications
Devdatta Akhawe (2014)
10.1016/j.cose.2017.04.011
Anatomy of the Facebook solution for mobile single sign-on: Security assessment and improvements
Giada Sciarretta (2017)
10.22215/etd/2018-12840
Strengthening Password-Based Web Authentication Through Multiple Supplementary Mechanisms
Furkan Alaca (2018)
See more
Semantic Scholar Logo Some data provided by SemanticScholar