A Mechanized Rich Model of the Web Infrastructure

• Applicant: Professor Dr. Ralf Küsters
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: from 2015 to 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 276807658

• Final Report Year: 2024

Final Report Abstract

Many of the nowadays ubiquitous Web applications need several parties to interoperate. For example, so-called Single-Sign-On (SSO) systems, such as “Sign in with Apple” allow users to log in at various Web sites, e.g., tripadvisor.com, simply by using their existing account at an Identity Provider (IdP). Here, the interaction between the various entities, the Web site, the IdP, and the user’s Web browser, is governed by a (Web) protocol, namely in this case the OpenID Connect (OIDC) Web protocol. Such protocols are of course highly security-critical, e.g., to prevent identity theft. However, the Web is complex, making it impossible to establish the absence of attacks just by “closely looking” at protocols or following best practices. Instead, formal analysis provides a way to prove protocols secure. For Web protocols, this requires modeling the Web environment: Web browsers, JavaScript, Web servers, HTTP(S), and so on. At the onset of this project, only a handful of models of the Web environment existed, and most of them were very abstract, with the exception of the Web Infrastructure Model (WIM) that we developed in preliminary work. Based on our preliminary work, the main goal of this project was to further develop the WIM and to use it to formally analyze the security of numerous important international protocol standards, including (1) OIDC, used, e.g., by Apple, Microsoft, Google, and Facebook with billions of users, (2) OAuth 2.0, used to authorize 3rd-party access to user data, e.g., user’s GMail, and (3) the Financial-grade API 1.0, used, e.g., for eGovernment and banking, with hundreds of millions of users. In all these formal analyses, we uncovered previously unknown attacks for which we proposed fixes, along with security proofs, to the responsible standardization groups, resulting in improved protocol standards. For OAuth 2.0, these attacks were so severe that the standardization group asked for an emergency meeting with us that resulted in a now annual OAuth Security Workshop with participants from academia, industry, and standardization organizations. We also took first steps towards mechanizing the WIM, and hence, enable tool-supported security analyses, by developing the tool DY*. This tool broadens the landscape of tools for general formal security protocol analysis, combines two previously disjoint paradigms for protocol analysis, and with several unique features overcomes limitations of existing analysis tools. As such, DY* is not only well suited as a basis for mechanizing the WIM but is also of general interest beyond the scope of this project.

Publications

• Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web. Lecture Notes in Computer Science, 43-65.
  Fett, Daniel; Küsters, Ralf & Schmitz, Guido
  
• SPRESSO. Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 1358-1369.
  Fett, Daniel; Küsters, Ralf & Schmitz, Guido
  
• A Comprehensive Formal Security Analysis of OAuth 2.0. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 1204-1215.
  Fett, Daniel; Küsters, Ralf & Schmitz, Guido
  
• Guest Blog: Formal Analysis of the OpenID Financialgrade API. 2017. Invited blog post
  D. Fett; P. Hosseyni & R. Küsters
  
• The Web SSO Standard OpenID Connect: In-depth Formal Security Analysis and Security Guidelines. 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 189-202.
  Fett, Daniel; Kusters, Ralf & Schmitz, Guido
  
• “An Expressive Formal Model of the Web Infrastructure”. PhD thesis. University of Stuttgart, Germany, 2018
  D. Fett
  
• An Extensive Formal Security Analysis of the OpenID Financial-Grade API. 2019 IEEE Symposium on Security and Privacy (SP).
  Fett, Daniel; Hosseyni, Pedram & Kusters, Ralf
  
• “Privacy-Preserving Web Single Sign-On: Formal Security Analysis and Design”. PhD thesis. University of Stuttgart, Germany, 2019
  G. Schmitz
  
• $\text{DY}^{\star}$: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. 2021 IEEE European Symposium on Security and Privacy (EuroS&P), 523-542.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Do Quoc, Huy; Hosseyni, Pedram; Küsters, Ralf; Schmitz, Guido & Würtele, Tim
  
• A Tutorial-Style Introduction to $$\textsf {DY}^\star $$. Lecture Notes in Computer Science, 77-97.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Do Quoc, Huy; Hosseyni, Pedram; Küsters, Ralf; Schmitz, Guido & Würtele, Tim
  
• An In-Depth Symbolic Security Analysis of the ACME Standard. Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, 2601-2617.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Do Quoc, Huy; Hosseyni, Pedram; Küsters, Ralf; Schmitz, Guido & Würtele, Tim
  
• DY* Code
  K. Bhargavan; A. Bichhawat; Q. H. Do; P. Hosseyni; R. Küsters; G. Schmitz & T. Würtele
  
• Layered Symbolic Security Analysis in $$\textsf {DY}^\star $$. Lecture Notes in Computer Science, 3-21.
  Bhargavan, Karthikeyan; Bichhawat, Abhishek; Hosseyni, Pedram; Küsters, Ralf; Pruiksma, Klaas; Schmitz, Guido; Waldmann, Clara & Würtele, Tim