User Tools

Site Tools


The Web Infrastructure Model

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, ESORICS 2015]
  • 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. [CCS 2016]
  • 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. [CSF 2017]
  • 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.

Future Work

We are currently working on mechanizing the WIM.

Literature and Publications

2019

  • 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), pages 1054-1072, IEEE Computer Society, 2019. BibTeX  Abstract  pdf 
  • Daniel Fett, Pedram Hosseyni, and Ralf Küsters. An Extensive Formal Security Analysis of the OpenID Financial-grade API. Technical Report arXiv:1901.11520, arXiv, 2019. Available at http://arxiv.org/abs/1901.11520. BibTeX  Abstract 

2018

  • Daniel Fett. An Expressive Formal Model of the Web Infrastructure. PhD Thesis. BibTeX  Abstract  pdf 

2017

  • 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), pages 189-202, IEEE Computer Society, 2017. BibTeX  Abstract  pdf 
  • Daniel Fett, Ralf Küsters, and Guido Schmitz. The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines. Technical Report arXiv:1704.08539, arXiv, 2017. Available at http://arxiv.org/abs/1704.08539. BibTeX  Abstract  pdf 

2016

  • 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), pages 1204-1215, ACM, 2016. BibTeX  Abstract  pdf 
  • Daniel Fett, Ralf Küsters, and Guido Schmitz. A Comprehensive Formal Security Analysis of OAuth 2.0. Technical Report arXiv:1601.01229, arXiv, 2016. Available at http://arxiv.org/abs/1601.01229. BibTeX  Abstract  pdf 

2015

  • Daniel Fett, Ralf Küsters, and Guido Schmitz. SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web. Technical Report arXiv:1508.01719, arXiv, 2015. Available at http://arxiv.org/abs/1508.01719. BibTeX  Abstract  pdf 
  • 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), pages 1358-1369, ACM, 2015. BibTeX  Abstract  pdf 
  • 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, pages 43-65, Springer, 2015. BibTeX  Abstract  pdf 
  • Daniel Fett, Ralf Küsters, and Guido Schmitz. Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web. Technical Report arXiv:1411.7210v2, arXiv, 2015. Available at http://arxiv.org/abs/1411.7210v2. BibTeX  Abstract  pdf 

2014

  • Daniel Fett, Ralf Küsters, and Guido Schmitz. An Expressive Model for the Web Infrastructure: Definition and Application to the BrowserID SSO System. Technical Report arXiv:1403.1866, arXiv, 2014. Available at http://arxiv.org/abs/1403.1866. BibTeX  Abstract  pdf 
  • 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), pages 673-688, IEEE Computer Society, 2014. BibTeX  Abstract  pdf 

Acknowledgments

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