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]

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. The most recent version of the WIM, including new features, such as WebRTC and WebSockets, can be found in Daniel Fett's PhD thesis [FettPhD2018].

Future Work

We are currently working on mechanizing the WIM.

Literature and Publications

  1. 2019

    1. D. Fett, P. Hosseyni, and R. 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.
    2. D. Fett, P. Hosseyni, and R. Küsters, “An Extensive Formal Security Analysis of the OpenID Financial-grade API,” arXiv, Technical Report arXiv:1901.11520, 2019.
  2. 2018

    1. D. Fett, “An Expressive Formal Model of the Web Infrastructure.” 2018.
  3. 2017

    1. D. Fett, R. Küsters, and G. 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. D. Fett, R. Küsters, and G. Schmitz, “The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines,” arXiv, Technical Report arXiv:1704.08539, 2017.
  4. 2016

    1. D. Fett, R. Küsters, and G. 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. D. Fett, R. Küsters, and G. Schmitz, “A Comprehensive Formal Security Analysis of OAuth 2.0,” arXiv, Technical Report arXiv:1601.01229, 2016.
  5. 2015

    1. D. Fett, R. Küsters, and G. Schmitz, “SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web,” arXiv, Technical Report arXiv:1508.01719, 2015.
    2. D. Fett, R. Küsters, and G. 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. D. Fett, R. Küsters, and G. 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. D. Fett, R. Küsters, and G. Schmitz, “Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web,” arXiv, Technical Report arXiv:1411.7210v2, 2015.
  6. 2014

    1. D. Fett, R. Küsters, and G. Schmitz, “An Expressive Model for the Web Infrastructure: Definition and Application to the BrowserID SSO System,” arXiv, Technical Report arXiv:1403.1866, 2014.
    2. D. Fett, R. Küsters, and G. 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).

Ralf Küsters
Prof. Dr.

Ralf Küsters

Head of Institute

Guido Schmitz
Dipl.-Inf.

Guido Schmitz

Ph.D. Student

To the top of the page