2014/03/07 by Daniel Fett, Fett, Daniel, R. Kuesters +3 · 1 citation
Computer Science · #Advanced Malware Detection Techniques #Cryptography and Security (cs.CR) #D.4.6 #FOS: Computer and information sciences #K.6.5 #Spam and Phishing Detection #User Authentication and Security Systems #Web Application Security Vulnerabilities #Web Data Mining and Analysis
paper · pdf · doi:10.48550/arxiv.1403.1866
openalex publication_date 2014/03/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The web constitutes a complex infrastructure and as demonstrated by numerous\nattacks, rigorous analysis of standards and web applications is indispensable.\n Inspired by successful prior work, in particular the work by Akhawe et al. as\nwell as Bansal et al., in this work we propose a formal model for the web\ninfrastructure. While unlike prior works, which aim at automatic analysis, our\nmodel so far is not directly amenable to automation, it is much more\ncomprehensive and accurate with respect to the standards and specifications. As\nsuch, it can serve as a solid basis for the analysis of a broad range of\nstandards and applications.\n As a case study and another important contribution of our work, we use our\nmodel to carry out the first rigorous analysis of the BrowserID system (a.k.a.\nMozilla Persona), a recently developed complex real-world single sign-on system\nthat employs technologies such as AJAX, cross-document messaging, and HTML5 web\nstorage. Our analysis revealed a number of very critical flaws that could not\nhave been captured in prior models. We propose fixes for the flaws, formally\nstate relevant security properties, and prove that the fixed system in a\nsetting with a so-called secondary identity provider satisfies these security\nproperties in our model. The fixes for the most critical flaws have already\nbeen adopted by Mozilla and our findings have been rewarded by the Mozilla\nSecurity Bug Bounty Program.\n