The Web Infrastructure Model (WIM)

The most comprehensive, expressive and precise model of the web infrastructure to date.

About the WIM

The Web Infrastructure Model, or just WIM, is a comprehensive, expressive and precise model of the web infrastructure. The WIM is in fact the most comprehensive formal model of the Web infrastructure to date. It allows for accurate security and privacy analyses of current web standards and applications, and can serve as a reference for web security researchers, developers of new technologies and standards, and for teaching web security concepts.

Case Studies and Impact

The WIM has successfully been used to analyze several security critical web standards and applications. The formal analysis often uncovered attacks and let to fixes in the respective standards and applications, which we then proved secure based on the WIM. In the following, we give a short overview of the web standards and applications analyzed in the WIM so far.

  • Mozilla BrowserID – a Single Sign On (SSO) system developed by Mozilla, with privacy in mind. During our analysis, we found several severe problems and proposed fixes for some of them. But the main design goal – privacy – was found to be broken beyond repair. [S&P2014], [ESORICS2015]
  • SPRESSO – Inspired by BrowserID's unique privacy goal, we designed SPRESSO, the first privacy-preserving Web SSO system: identity providers do not and cannot learn to which relying parties users login to. We utilized the WIM to develop this SSO protocol right from the start. Using the WIM, we showed that SPRESSO indeed provides strong security and privacy guarantees. [CCS2015] See also https://spresso.me.
  • OAuth 2.0 – an open standard commonly used as a way for Internet users to grant websites or applications access to their data on other websites, without giving away passwords. OAuth 2.0 is widely used in the web (e.g., by Facebook, Google, Microsoft, and Amazon). Despite the fact that OAuth 2.0 had been analyzed before, our formal analysis uncovered several new attacks. We developed fixes for those and proved that the protocol is secure under certain assumptions. We closely worked with the responsible IETF working group to improve the standard accordingly. As a result of this collaboration, we initiated the annual OAuth Security Workshop, which connects researchers, industry and standardization organizations to further improve OAuth and related standards. [CCS2016]
  • OpenID Connect – While OAuth 2.0 provides a protocol for delegated authorization, it was not designed for user authentication. OpenID Connect fills this gap by extending OAuth 2.0 to explicitly provide authentication. In our work, we not only prove the security of the protocol, but also provide guidelines for implementors, together with an overview of multiple classes of attacks and their mitigations. [CSF2017]
  • Financial-grade API – The OpenID Financial-grade API is an authorization and authentication scheme designed for high-risk environments, for instance for financial applications. It is based on OAuth 2.0, but extended by various new security mechanisms for providing a secure flow under a stronger attacker model. Suggested by the OpenID Foundation, we analyzed the Financial-grade API with all of its security extensions. Our analysis revealed several attacks not only on the Financial-grade API itself but also on some of the new security mechanisms (e.g., PKCE, mTLS, OAuth Token Binding, JARM). The results of the analysis were discussed, among others, at the 4th OAuth Security Workshop, and also in a guest blog entry for the OpenID Foundation. [S&P2019]
  • Web Payment APIs – The Web Payment APIs are a set of specifications by the W3C Web Payments Working Group that aim to offer new and improved checkout and payment mechanisms for the Web. During our analysis of the Web Payment specification, we discovered several vulnerabilities, one of which even allowed a malicious merchant to charge a customer multiple times for the same transaction. We verified that the attack works in practice and notified the W3C Web Payments Working Group as well as the Chromium developers about our findings. We also proposed fixes for the problem, which have been adopted in the meantime. [not published yet]

History

The first version of the WIM was published at [S&P2014]. Throughout all further papers we improved and extended the WIM. For example, in the [CCS2015] paper, we made several improvements to enable privacy analysis. New features, such as WebRTC and WebSockets, have been added in Daniel Fett's PhD thesis [FettPhD2018].

Future Work

We aim to combine the comprehensiveness of the WIM with mechanized (i.e., tool-supported and tool-verifiable) proofs using F* to encode and verify the WIM and case studies. F* is a functional programming language aimed at program verification. Program specifications, including correctness and security properties, can be expressed precisely and compactly thanks to F*’s type system. With mechanized proofs in the F* web model it becomes easier to reuse proofs. For example, proofs for OAuth could be reused in proofs for OpenID Connect, and changes/extensions to the protocols could be tracked much faster. In a similar manner, regression tests could be run against extensions of the models. Additionally, the F* specification of a protocol could be used to extract runnable code in JavaScript, TypeScript, OCaml, F# or C for execution.

This ongoing project is in cooperation with the groups of Karthikeyan Bhargavan at INRIA Paris and Abhishek Bichawat at Carnegie Mellon University.

Literature and Publications

  1. 2019

    1. Guido Schmitz, “Privacy-Preserving Web Single Sign-On: Formal Security Analysis and Design,” University of Stuttgart, Ph.D. Thesis, 2019.
    2. Daniel Fett, Pedram Hosseyni, and Ralf Küsters, “An Extensive Formal Security Analysis of the OpenID Financial-grade API,” in 2019 IEEE Symposium on Security and Privacy (S&P 2019), 2019, vol. 1, pp. 1054–1072.
    3. Daniel Fett, Pedram Hosseyni, and Ralf Küsters, “An Extensive Formal Security Analysis of the OpenID Financial-grade API,” arXiv, Technical Report arXiv:1901.11520, 2019. Available at http://arxiv.org/abs/1901.11520.
  2. 2018

    1. Daniel Fett, “An Expressive Formal Model of the Web Infrastructure,” Ph.D. Thesis, 2018. received an award from the “Vereinigung von Freunden der Universität Stuttgart” in 2019.
  3. 2017

    1. Daniel Fett, Ralf Küsters, and Guido Schmitz, “The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines,” in IEEE 30th Computer Security Foundations Symposium (CSF 2017), 2017, pp. 189--202.
    2. Daniel Fett, Ralf Küsters, and Guido Schmitz, “The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines,” arXiv, Technical Report arXiv:1704.08539, 2017. Available at http://arxiv.org/abs/1704.08539.
  4. 2016

    1. Daniel Fett, Ralf Küsters, and Guido Schmitz, “A Comprehensive Formal Security Analysis of OAuth 2.0,” in Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS 2016), 2016, pp. 1204--1215.
    2. Daniel Fett, Ralf Küsters, and Guido Schmitz, “A Comprehensive Formal Security Analysis of OAuth 2.0,” arXiv, Technical Report arXiv:1601.01229, 2016. Available at http://arxiv.org/abs/1601.01229.
  5. 2015

    1. Daniel Fett, Ralf Küsters, and Guido Schmitz, “SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web,” arXiv, Technical Report arXiv:1508.01719, 2015. Available at http://arxiv.org/abs/1508.01719.
    2. Daniel Fett, Ralf Küsters, and Guido Schmitz, “SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web,” in Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS 2015), 2015, pp. 1358--1369.
    3. Daniel Fett, Ralf Küsters, and Guido Schmitz, “Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web,” in Computer Security - ESORICS 2015 - 20th European Symposium on Research in Computer Security, Vienna, Austria, September 21-25, 2015, Proceedings, Part I, 2015, pp. 43--65.
    4. Daniel Fett, Ralf Küsters, and Guido Schmitz, “Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web,” arXiv, Technical Report arXiv:1411.7210v2, 2015. Available at http://arxiv.org/abs/1411.7210v2.
  6. 2014

    1. Daniel Fett, Ralf Küsters, and Guido Schmitz, “An Expressive Model for the Web Infrastructure: Definition and Application to the BrowserID SSO System,” arXiv, Technical Report arXiv:1403.1866, 2014. Available at http://arxiv.org/abs/1403.1866.
    2. Daniel Fett, Ralf Küsters, and Guido Schmitz, “An Expressive Model for the Web Infrastructure: Definition and Application to the BrowserID SSO System,” in 35th IEEE Symposium on Security and Privacy (S&P 2014), 2014, pp. 673–688.

Acknowledgements

This work has been supported by Deutsche Forschungsgemeinschaft (DFG) as well as by the Studienstiftung des Deutschen Volkes (German National Academic Foundation).

This picture showsRalf Küsters
Prof. Dr.

Ralf Küsters

Head of Institute

To the top of the page