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
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
AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations
Guangdong Bai (2013)
Dynamic pharming attacks and locked same-origin policies for web browsers
C. Karlof (2007)
Using static analysis to validate the SAML single sign-on protocol
Steffen M. Hansen (2005)
Contribution to a Rigorous Analysis of Web Application Frameworks
E. Börger (2012)
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)
Alloy: A New Technology for Software Modelling
Daniel Jackson (2002)
Web Storage - W3C Recommendation 30
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)
Discovering Concrete Attacks on Website Authorization by Formal Analysis
Chetan Bansal (2012)
Security Analysis of OpenID
Pavol Sovis (2010)
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
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)
Mobile values, new names, and secure communication
M. Abadi (2001)
Multiset rewriting and the complexity of bounded security protocols
N. Durgin (2004)
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
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage
Chetan Bansal (2013)
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)
An efficient cryptographic protocol verifier based on prolog rules
B. Blanchet (2001)
Security analysis of the SAML single sign-on browser/artifact profile
T. Groß (2003)
Towards a Formal Foundation of Web Security
Devdatta Akhawe (2010)
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)
Systematically breaking and fixing OpenID security: Formal analysis, semi-automated empirical evaluation, and practical countermeasures
San-Tsai Sun (2012)
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)
Characterization of web single sign-on protocols
V. Beltran (2016)
Do Not Trust Me: Using Malicious IdPs for Analyzing and Attacking Single Sign-on
C. Mainka (2016)
Foundations of Security Analysis and Design VII
A. Aldini (2014)
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)
Design Space Exploration for Security
E. Kang (2016)
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)
SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web
Daniel Fett (2015)
SoK: Single Sign-On Security — An Evaluation of OpenID Connect
C. Mainka (2017)
Design, Formal Specification and Analysis of Multi-Factor Authentication Solutions with a Single Sign-On Experience
Giada Sciarretta (2018)
The Web SSO Standard OpenID Connect: In-depth Formal Security Analysis and Security Guidelines
Daniel Fett (2017)
Formal methods for web security
Michele Bugliesi (2017)
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)
Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web
Daniel Fett (2015)
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)
Automated Synthesis of Secure Platform Mappings
Eunsuk Kang (2019)
A Verified Secure Protocol Model of OAuth Dynamic Client Registration
Caimei Wang (2017)
Modelling and Analysis of Web Applications in Tamarin
Sandra Dünki (2019)
On message-level security
C. Mainka (2017)
Analyzing Security and Privacy in Design and Implementation of Web Authentication Protocols
Kailong Wang (2018)
A novel approach to provide Web page recommendation using domain knowledge and web usage knowledge
P. L. Kolekar (2016)
Run-time Monitoring and Formal Analysis of Information Flows in Chromium
Lujo Bauer (2015)
Network-based Origin Confusion Attacks against HTTPS Virtual Hosting
Antoine Delignat-Lavaud (2015)
Towards High Assurance HTML5 Applications
Devdatta Akhawe (2014)
Anatomy of the Facebook solution for mobile single sign-on: Security assessment and improvements
Giada Sciarretta (2017)
Strengthening Password-Based Web Authentication Through Multiple Supplementary Mechanisms
Furkan Alaca (2018)
See more
Semantic Scholar Logo Some data provided by SemanticScholar