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.
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]
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].
We are currently working on mechanizing the WIM.
Literature and Publications
This work has been supported by Deutsche Forschungsgemeinschaft (DFG) as well as by the Studienstiftung des Deutschen Volkes (German National Academic Foundation).