Position within the page tree

Start
Research
The Web Infrastructure Model

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.

A consolidated version of the WIM is available here.

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. [S&P2022]
GNAP – The "Grant Negotiation and Authorization Protocol" is designed to address many of the use-cases of OAuth 2.0 and OpenID Connect, including several common extensions to these protocols, in a clean and secure way. We performed a formal security analysis of a mature draft of the GNAP specifications and found several attacks. We proposed and discussed fixes with the GNAP Working Group, leading to according changes to the specifications, and finally proved the fixed protocol to be secure. [ESORICS 2023, to appear] [Technical Report]
OpenID FAPI 2.0 Security Profile – The FAPI 2.0 family of specifications embodies a complete re-design of the Financial-grade API mentioned above aiming to incorporate lessons learned and provide the same level of security under very strong attacker assumptions, while at the same time improving interoperability. A unique feature of the FAPI 2.0 family of specifications is the so-called "FAPI 2.0 Attacker Model" document: it not only explicitly lays out a (strong) attacker model, but also defines the desired security properties for the FAPI 2.0 Security Profile protocol. The OpenID Foundation asked us to accompany the standardization process with a formal security analysis of a mature draft of the specifications to ensure the aforementioned security properties hold under their strong attacker model. Our analysis revealed several attacks to which we proposed and discussed fixes with the FAPI Working Group, resulting in several changes to the specifications. We then proved the fixed protocol to be secure. [CSF2024, to appear]
OpenID FAPI 2.0 Security Profile with FAPI 2.0 Message Signing, FAPI-CIBA, Dynamic Client Registration, and Dynamic Client Management – Following our analysis of the FAPI 2.0 Security Profile, the OpenID Foundation proposed to extend said analysis with a set of extensions and additional protocols. The FAPI 2.0 Message Signing specification aims to add non-repudiation properties to the FAPI 2.0 Security Profile by combining several existing specifications for signing the various message types. FAPI-CIBA builds on top of the "Client Initiated Backchannel-Authentication" protocol and provides means for FAPI clients to initiate an authentication flow without the need for a user-agent to be involved. The actual user authentication is then typically initiated by means of a push notification to the user's phone. Furthermore, Dynamic Client Registration and Management are meant to allow FAPI clients to dynamically register (or update their registration) at an authorization server. Our security analysis covered an ecosystem in which all these protocols and extensions are used in parallel and lead to the discovery of new attacks. We discussed these attacks and possible fixes with the FAPI Working Group, resulting again in changes to the specifications, which we incorporated into our model and were then able to prove security of the fixed protocol.

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.

Work towards a mechanized WIM has lead to the development of DY*, a formal verification framework for the symbolic security analysis of cryptographic protocol code written in F*.

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

Literature and Publications

2024
1. Pedram Hosseyni, Ralf Küsters, and Tim Würtele, “Formal Security Analysis of the OpenID FAPI 2.0: Accompanying a Standardization Process,” Cryptology ePrint Archive, Technical Report 2024/078, 2024.
  Abstract
  In recent years, the number of third-party services that can access highly-sensitive data has increased steadily, e.g., in the financial sector, in eGovernment applications, or in high-assurance identity services. Protocols that enable this access must provide strong security guarantees. A prominent and widely employed protocol for this purpose is the OpenID Foundation's FAPI protocol. The FAPI protocol is already in widespread use, e.g., as part of the UK's Open Banking standards and Brazil's Open Banking Initiative as well as outside of the financial sector, for instance, as part of the Australian government's Consumer Data Rights standards. Based on lessons learned from FAPI 1.0, the OpenID Foundation has developed a completely new protocol, called FAPI 2.0. The specifications of FAPI 2.0 include a concrete set of security goals and attacker models under which the protocol aims to be secure. Following an invitation from the OpenID Foundation's FAPI Working Group (FAPI WG), we have accompanied the standardization process of the FAPI 2.0 protocol by an in-depth formal security analysis. In this paper, we report on our analysis and findings. Our analysis incorporates the first formal model of the FAPI 2.0 protocol and is based on a detailed model of the web infrastructure, the Web Infrastructure Model, originally proposed by Fett, Küsters, and Schmitz. Our analysis has uncovered several types of attacks on the protocol, violating the aforementioned security goals set by the FAPI WG. We subsequently have worked with the FAPI WG to fix the protocol, resulting in several changes to the specifications. After adapting our model to the changed specifications, we have proved the security properties to hold under the strong attacker model defined by the FAPI WG.
  BibTeX
  @techreport{HosseyniKuestersWuertele-IACR-2024-078, abstract = {In recent years, the number of third-party services that can access highly-sensitive data has increased steadily, e.g., in the financial sector, in eGovernment applications, or in high-assurance identity services. Protocols that enable this access must provide strong security guarantees. A prominent and widely employed protocol for this purpose is the OpenID Foundation's FAPI protocol. The FAPI protocol is already in widespread use, e.g., as part of the UK's Open Banking standards and Brazil's Open Banking Initiative as well as outside of the financial sector, for instance, as part of the Australian government's Consumer Data Rights standards. Based on lessons learned from FAPI 1.0, the OpenID Foundation has developed a completely new protocol, called FAPI 2.0. The specifications of FAPI 2.0 include a concrete set of security goals and attacker models under which the protocol aims to be secure. Following an invitation from the OpenID Foundation's FAPI Working Group (FAPI WG), we have accompanied the standardization process of the FAPI 2.0 protocol by an in-depth formal security analysis. In this paper, we report on our analysis and findings. Our analysis incorporates the first formal model of the FAPI 2.0 protocol and is based on a detailed model of the web infrastructure, the Web Infrastructure Model, originally proposed by Fett, Küsters, and Schmitz. Our analysis has uncovered several types of attacks on the protocol, violating the aforementioned security goals set by the FAPI WG. We subsequently have worked with the FAPI WG to fix the protocol, resulting in several changes to the specifications. After adapting our model to the changed specifications, we have proved the security properties to hold under the strong attacker model defined by the FAPI WG.}, author = {Hosseyni, Pedram and K{\"u}sters, Ralf and W{\"u}rtele, Tim}, institution = {Cryptology ePrint Archive}, number = {2024/078}, title = {{Formal Security Analysis of the OpenID FAPI 2.0: Accompanying a Standardization Process}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/hosseynikuesterswuertele-iacr-2024-078.pdf}, year = 2024 }
  Link
  https://publ.sec.uni-stuttgart.de/hosseynikuesterswuertele-iacr-2024-078.pdf
2. Pedram Hosseyni, Ralf Küsters, and Tim Würtele, “Formal Security Analysis of the OpenID FAPI 2.0: Accompanying a Standardization Process,” in 37th IEEE Computer Security Foundations Symposium (CSF 2024), IEEE, 2024. To appear.
  Abstract
  In recent years, the number of third-party services that can access highly-sensitive data has increased steadily, e.g., in the financial sector, in eGovernment applications, or in high-assurance identity services. Protocols that enable this access must provide strong security guarantees. A prominent and widely employed protocol for this purpose is the OpenID Foundation's FAPI protocol. The FAPI protocol is already in widespread use, e.g., as part of the UK's Open Banking standards and Brazil's Open Banking Initiative as well as outside of the financial sector, for instance, as part of the Australian government's Consumer Data Rights standards. Based on lessons learned from FAPI 1.0, the OpenID Foundation has developed a completely new protocol, called FAPI 2.0. The specifications of FAPI 2.0 include a concrete set of security goals and attacker models under which the protocol aims to be secure. Following an invitation from the OpenID Foundation's FAPI Working Group (FAPI WG), we have accompanied the standardization process of the FAPI 2.0 protocol by an in-depth formal security analysis. In this paper, we report on our analysis and findings. Our analysis incorporates the first formal model of the FAPI 2.0 protocol and is based on a detailed model of the web infrastructure, the Web Infrastructure Model, originally proposed by Fett, Küsters, and Schmitz. Our analysis has uncovered several types of attacks on the protocol, violating the aforementioned security goals set by the FAPI WG. We subsequently have worked with the FAPI WG to fix the protocol, resulting in several changes to the specifications. After adapting our model to the changed specifications, we have proved the security properties to hold under the strong attacker model defined by the FAPI WG.
  BibTeX
  @inproceedings{HosseyniKuestersWuertele-CSF-2024, abstract = {In recent years, the number of third-party services that can access highly-sensitive data has increased steadily, e.g., in the financial sector, in eGovernment applications, or in high-assurance identity services. Protocols that enable this access must provide strong security guarantees. A prominent and widely employed protocol for this purpose is the OpenID Foundation's FAPI protocol. The FAPI protocol is already in widespread use, e.g., as part of the UK's Open Banking standards and Brazil's Open Banking Initiative as well as outside of the financial sector, for instance, as part of the Australian government's Consumer Data Rights standards. Based on lessons learned from FAPI 1.0, the OpenID Foundation has developed a completely new protocol, called FAPI 2.0. The specifications of FAPI 2.0 include a concrete set of security goals and attacker models under which the protocol aims to be secure. Following an invitation from the OpenID Foundation's FAPI Working Group (FAPI WG), we have accompanied the standardization process of the FAPI 2.0 protocol by an in-depth formal security analysis. In this paper, we report on our analysis and findings. Our analysis incorporates the first formal model of the FAPI 2.0 protocol and is based on a detailed model of the web infrastructure, the Web Infrastructure Model, originally proposed by Fett, Küsters, and Schmitz. Our analysis has uncovered several types of attacks on the protocol, violating the aforementioned security goals set by the FAPI WG. We subsequently have worked with the FAPI WG to fix the protocol, resulting in several changes to the specifications. After adapting our model to the changed specifications, we have proved the security properties to hold under the strong attacker model defined by the FAPI WG.}, author = {Hosseyni, Pedram and K{\"u}sters, Ralf and W{\"u}rtele, Tim}, booktitle = {{37th IEEE Computer Security Foundations Symposium (CSF 2024)}}, note = {To appear.}, publisher = {IEEE}, title = {{Formal Security Analysis of the OpenID FAPI 2.0: Accompanying a Standardization Process}}, url = {https://publ.sec.uni-stuttgart.de/hosseynikuesterswuertele-iacr-2024-078.pdf}, year = 2024 }
  Link
  https://publ.sec.uni-stuttgart.de/hosseynikuesterswuertele-iacr-2024-078.pdf
2023
1. Florian Helmschmidt, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Clara Waldmann, and Tim Würtele, “The Grant Negotiation and Authorization Protocol: Attacking, Fixing, and Verifying an Emerging Standard,” in 28th European Symposium on Research in Computer Security (ESORICS 2023), Springer, 2023, pp. 222--242.
  Abstract
  The Grant Negotiation and Authorization Protocol (GNAP) is an emerging authorization and authentication protocol which aims to consolidate and unify several use-cases of OAuth 2.0 and many of its common extensions while providing a higher degree of security. OAuth 2.0 is an essential cornerstone of the security of authorization and authentication for the Web, IoT, and beyond, and is used, among others, by many global players, like Google, Facebook, and Microsoft. Historical limitations of OAuth 2.0 and its extensions have led prominent members of the OAuth community to create GNAP, a newly designed protocol for authorization and authentication. Given GNAP's advantages over OAuth 2.0 and its support within the OAuth community, GNAP is expected to become at least as important as OAuth 2.0. In this paper, we present the first formal security analysis of GNAP. We build a detailed formal model of GNAP, based on the Web Infrastructure Model (WIM) of Fett, Küsters, and Schmitz, and provide formal statements of the key security properties of GNAP, namely authorization, authentication, and session integrity. We discovered several attacks on GNAP in the process of trying to prove these properties. We present these attacks, as well as changes to the protocol that prevent them. These modifications have been incorporated into the GNAP specification after discussion with the GNAP working group. We give the first formal security guarantees for GNAP, by proving that GNAP, with our modifications applied, satisfies the mentioned security properties. GNAP was still an early draft when we began our analysis, but is now on track to be adopted as an IETF standard. Hence, our analysis is just in time to help ensure the security of this important emerging standard.
  BibTeX
  @inproceedings{HelmschmidtHosseyniKuestersPruiksmaWaldmannWuertele-ESORICS-2023, abstract = {The Grant Negotiation and Authorization Protocol (GNAP) is an emerging authorization and authentication protocol which aims to consolidate and unify several use-cases of OAuth 2.0 and many of its common extensions while providing a higher degree of security. OAuth 2.0 is an essential cornerstone of the security of authorization and authentication for the Web, IoT, and beyond, and is used, among others, by many global players, like Google, Facebook, and Microsoft. Historical limitations of OAuth 2.0 and its extensions have led prominent members of the OAuth community to create GNAP, a newly designed protocol for authorization and authentication. Given GNAP's advantages over OAuth 2.0 and its support within the OAuth community, GNAP is expected to become at least as important as OAuth 2.0. In this paper, we present the first formal security analysis of GNAP. We build a detailed formal model of GNAP, based on the Web Infrastructure Model (WIM) of Fett, Küsters, and Schmitz, and provide formal statements of the key security properties of GNAP, namely authorization, authentication, and session integrity. We discovered several attacks on GNAP in the process of trying to prove these properties. We present these attacks, as well as changes to the protocol that prevent them. These modifications have been incorporated into the GNAP specification after discussion with the GNAP working group. We give the first formal security guarantees for GNAP, by proving that GNAP, with our modifications applied, satisfies the mentioned security properties. GNAP was still an early draft when we began our analysis, but is now on track to be adopted as an IETF standard. Hence, our analysis is just in time to help ensure the security of this important emerging standard.}, author = {Helmschmidt, Florian and Hosseyni, Pedram and K{\"u}sters, Ralf and Pruiksma, Klaas and Waldmann, Clara and W{\"u}rtele, Tim}, booktitle = {{28th European Symposium on Research in Computer Security (ESORICS 2023)}}, doi = {10.1007/978-3-031-51479-1_12}, pages = {222--242}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{The Grant Negotiation and Authorization Protocol: Attacking, Fixing, and Verifying an Emerging Standard}}, url = {https://publ.sec.uni-stuttgart.de/helmschmidthosseynikuesterspruiksmawaldmannwuertele-iacr-2023-1325.pdf}, volume = 14346, year = 2023 }
  Link
  https://publ.sec.uni-stuttgart.de/helmschmidthosseynikuesterspruiksmawaldmannwuertele-iacr-2023-1325.pdf
  DOI
  10.1007/978-3-031-51479-1_12
2. Florian Helmschmidt, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Clara Waldmann, and Tim Würtele, “The Grant Negotiation and Authorization Protocol: Attacking, Fixing, and Verifying an Emerging Standard,” Cryptology ePrint Archive, Technical Report 2023/1325, 2023.
  Abstract
  The Grant Negotiation and Authorization Protocol (GNAP) is an emerging authorization and authentication protocol which aims to consolidate and unify several use-cases of OAuth 2.0 and many of its common extensions while providing a higher degree of security. OAuth 2.0 is an essential cornerstone of the security of authorization and authentication for the Web, IoT, and beyond, and is used, among others, by many global players, like Google, Facebook, and Microsoft. Historical limitations of OAuth 2.0 and its extensions have led prominent members of the OAuth community to create GNAP, a newly designed protocol for authorization and authentication. Given GNAP's advantages over OAuth 2.0 and its support within the OAuth community, GNAP is expected to become at least as important as OAuth 2.0. In this paper, we present the first formal security analysis of GNAP. We build a detailed formal model of GNAP, based on the Web Infrastructure Model (WIM) of Fett, Küsters, and Schmitz, and provide formal statements of the key security properties of GNAP, namely authorization, authentication, and session integrity. We discovered several attacks on GNAP in the process of trying to prove these properties. We present these attacks, as well as changes to the protocol that prevent them. These modifications have been incorporated into the GNAP specification after discussion with the GNAP working group. We give the first formal security guarantees for GNAP, by proving that GNAP, with our modifications applied, satisfies the mentioned security properties. GNAP was still an early draft when we began our analysis, but is now on track to be adopted as an IETF standard. Hence, our analysis is just in time to help ensure the security of this important emerging standard.
  BibTeX
  @techreport{HelmschmidtHosseyniKuestersPruiksmaWaldmannWuertele-IACR-2023-1325, abstract = {The Grant Negotiation and Authorization Protocol (GNAP) is an emerging authorization and authentication protocol which aims to consolidate and unify several use-cases of OAuth 2.0 and many of its common extensions while providing a higher degree of security. OAuth 2.0 is an essential cornerstone of the security of authorization and authentication for the Web, IoT, and beyond, and is used, among others, by many global players, like Google, Facebook, and Microsoft. Historical limitations of OAuth 2.0 and its extensions have led prominent members of the OAuth community to create GNAP, a newly designed protocol for authorization and authentication. Given GNAP's advantages over OAuth 2.0 and its support within the OAuth community, GNAP is expected to become at least as important as OAuth 2.0. In this paper, we present the first formal security analysis of GNAP. We build a detailed formal model of GNAP, based on the Web Infrastructure Model (WIM) of Fett, Küsters, and Schmitz, and provide formal statements of the key security properties of GNAP, namely authorization, authentication, and session integrity. We discovered several attacks on GNAP in the process of trying to prove these properties. We present these attacks, as well as changes to the protocol that prevent them. These modifications have been incorporated into the GNAP specification after discussion with the GNAP working group. We give the first formal security guarantees for GNAP, by proving that GNAP, with our modifications applied, satisfies the mentioned security properties. GNAP was still an early draft when we began our analysis, but is now on track to be adopted as an IETF standard. Hence, our analysis is just in time to help ensure the security of this important emerging standard.}, author = {Helmschmidt, Florian and Hosseyni, Pedram and K{\"u}sters, Ralf and Pruiksma, Klaas and Waldmann, Clara and W{\"u}rtele, Tim}, institution = {Cryptology ePrint Archive}, number = {2023/1325}, title = {{The Grant Negotiation and Authorization Protocol: Attacking, Fixing, and Verifying an Emerging Standard}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/helmschmidthosseynikuesterspruiksmawaldmannwuertele-iacr-2023-1325.pdf}, year = 2023 }
  Link
  https://publ.sec.uni-stuttgart.de/helmschmidthosseynikuesterspruiksmawaldmannwuertele-iacr-2023-1325.pdf
2022
1. Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Nils Wenzler, and Tim Würtele, “A Formal Security Analysis of the W3C Web Payment APIs: Attacks and Verification,” in 43rd IEEE Symposium on Security and Privacy (S&P 2022), IEEE, 2022, pp. 134–153.
  Abstract
  Payment is an essential part of e-commerce. Merchants usually rely on third-parties, so-called payment processors, who take care of transferring the payment from the customer to the merchant. How a payment processor interacts with the customer and the merchant varies a lot. Each payment processor typically invents its own protocol that has to be integrated into the merchant's application and provides the user with a new, potentially unknown and confusing user experience. Pushed by major companies, including Apple, Google, Mastercard, and Visa, the W3C is currently developing a new set of standards to unify the online checkout process and "streamline the user's payment experience". The main idea is to integrate payment as a native functionality into web browsers, referred to as the Web Payment APIs. While this new checkout process will indeed be simple and convenient from an end-user perspective, the technical realization requires rather significant changes to browsers. Many major browsers, such as Chrome, Firefox, Edge, Safari, and Opera, already implement these new standards, and many payment processors, such as Google Pay, Apple Pay, or Stripe, support the use of Web Payment APIs for payments. The ecosystem is constantly growing, meaning that the Web Payment APIs will likely be used by millions of people worldwide. So far, there has been no in-depth security analysis of these new standards. In this paper, we present the first such analysis of the Web Payment APIs standards, a rigorous formal analysis. It is based on the Web Infrastructure Model (WIM), the most comprehensive model of the web infrastructure to date, which, among others, we extend to integrate the new payment functionality into the generic browser model. Our analysis reveals two new critical vulnerabilities that allow a malicious merchant to over-charge an unsuspecting customer. We have verified our attacks using the Chrome implementation and reported these problems to the W3C as well as the Chrome developers, who have acknowledged these problems. Moreover, we propose fixes to the standard, which by now have been adopted by the W3C and Chrome, and prove that the fixed Web Payment APIs indeed satisfy strong security properties.
  BibTeX
  @inproceedings{DoHosseyniKuestersSchmitzWenzlerWuertele-SP-2022, abstract = {Payment is an essential part of e-commerce. Merchants usually rely on third-parties, so-called payment processors, who take care of transferring the payment from the customer to the merchant. How a payment processor interacts with the customer and the merchant varies a lot. Each payment processor typically invents its own protocol that has to be integrated into the merchant's application and provides the user with a new, potentially unknown and confusing user experience. Pushed by major companies, including Apple, Google, Mastercard, and Visa, the W3C is currently developing a new set of standards to unify the online checkout process and "streamline the user's payment experience". The main idea is to integrate payment as a native functionality into web browsers, referred to as the Web Payment APIs. While this new checkout process will indeed be simple and convenient from an end-user perspective, the technical realization requires rather significant changes to browsers. Many major browsers, such as Chrome, Firefox, Edge, Safari, and Opera, already implement these new standards, and many payment processors, such as Google Pay, Apple Pay, or Stripe, support the use of Web Payment APIs for payments. The ecosystem is constantly growing, meaning that the Web Payment APIs will likely be used by millions of people worldwide. So far, there has been no in-depth security analysis of these new standards. In this paper, we present the first such analysis of the Web Payment APIs standards, a rigorous formal analysis. It is based on the Web Infrastructure Model (WIM), the most comprehensive model of the web infrastructure to date, which, among others, we extend to integrate the new payment functionality into the generic browser model. Our analysis reveals two new critical vulnerabilities that allow a malicious merchant to over-charge an unsuspecting customer. We have verified our attacks using the Chrome implementation and reported these problems to the W3C as well as the Chrome developers, who have acknowledged these problems. Moreover, we propose fixes to the standard, which by now have been adopted by the W3C and Chrome, and prove that the fixed Web Payment APIs indeed satisfy strong security properties.}, author = {Do, Quoc Huy and Hosseyni, Pedram and K{\"u}sters, Ralf and Schmitz, Guido and Wenzler, Nils and W{\"u}rtele, Tim}, booktitle = {{43rd IEEE Symposium on Security and Privacy (S{\&}P 2022)}}, doi = {10.1109/SP46214.2022.9833681}, month = {5}, pages = {134-153}, publisher = {IEEE}, title = {{A Formal Security Analysis of the W3C Web Payment APIs: Attacks and Verification}}, url = {https://publ.sec.uni-stuttgart.de/dohosseynikuestersschmitzwenzlerwuertele-sp-2022.pdf}, year = 2022 }
  Link
  https://publ.sec.uni-stuttgart.de/dohosseynikuestersschmitzwenzlerwuertele-sp-2022.pdf
  DOI
  10.1109/SP46214.2022.9833681
2021
1. Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Nils Wenzler, and Tim Würtele, “A Formal Security Analysis of the W3C Web Payment APIs: Attacks and Verification,” Cryptology ePrint Archive, Technical Report 2021/1012, 2021.
  Abstract
  Payment is an essential part of e-commerce. Merchants usually rely on third-parties, so-called payment processors, who take care of transferring the payment from the customer to the merchant. How a payment processor interacts with the customer and the merchant varies a lot. Each payment processor typically invents its own protocol that has to be integrated into the merchant’s application and provides the user with a new, potentially unknown and confusing user experience. Pushed by major companies, including Apple, Google, Mastercard, and Visa, the W3C is currently developing a new set of standards to unify the online checkout process and “streamline the user’s payment experience”. The main idea is to integrate payment as a native functionality into web browsers, referred to as the Web Payment APIs. While this new checkout process will indeed be simple and convenient from an end-user perspective, the technical realization requires rather significant changes to browsers. Many major browsers, such as Chrome, Firefox, Edge, Safari, and Opera, already implement these new standards, and many payment processors, such as Google Pay, Apple Pay, or Stripe, support the use of Web Payment APIs for payments. The ecosystem is constantly growing, meaning that the Web Payment APIs will likely be used by millions of people worldwide. So far, there has been no in-depth security analysis of these new standards. In this paper, we present the first such analysis of the Web Payment APIs standards, a rigorous formal analysis. It is based on the Web Infrastructure Model (WIM), the most comprehensive model of the web infrastructure to date, which, among others, we extend to integrate the new payment functionality into the generic browser model. Our analysis reveals two new critical vulnerabilities that allow a malicious merchant to over-charge an unsuspecting customer. We have verified our attacks using the Chrome implementation and reported these problems to the W3C as well as the Chrome developers, who have acknowledged these problems. Moreover, we propose fixes to the standard, which by now have been adopted by the W3C and Chrome, and prove that the fixed Web Payment APIs indeed satisfy strong security properties.
  BibTeX
  @techreport{DoHosseyniKuestersSchmitzWenzlerWuertele-IACR-2021, abstract = {Payment is an essential part of e-commerce. Merchants usually rely on third-parties, so-called payment processors, who take care of transferring the payment from the customer to the merchant. How a payment processor interacts with the customer and the merchant varies a lot. Each payment processor typically invents its own protocol that has to be integrated into the merchant’s application and provides the user with a new, potentially unknown and confusing user experience. Pushed by major companies, including Apple, Google, Mastercard, and Visa, the W3C is currently developing a new set of standards to unify the online checkout process and “streamline the user’s payment experience”. The main idea is to integrate payment as a native functionality into web browsers, referred to as the Web Payment APIs. While this new checkout process will indeed be simple and convenient from an end-user perspective, the technical realization requires rather significant changes to browsers. Many major browsers, such as Chrome, Firefox, Edge, Safari, and Opera, already implement these new standards, and many payment processors, such as Google Pay, Apple Pay, or Stripe, support the use of Web Payment APIs for payments. The ecosystem is constantly growing, meaning that the Web Payment APIs will likely be used by millions of people worldwide. So far, there has been no in-depth security analysis of these new standards. In this paper, we present the first such analysis of the Web Payment APIs standards, a rigorous formal analysis. It is based on the Web Infrastructure Model (WIM), the most comprehensive model of the web infrastructure to date, which, among others, we extend to integrate the new payment functionality into the generic browser model. Our analysis reveals two new critical vulnerabilities that allow a malicious merchant to over-charge an unsuspecting customer. We have verified our attacks using the Chrome implementation and reported these problems to the W3C as well as the Chrome developers, who have acknowledged these problems. Moreover, we propose fixes to the standard, which by now have been adopted by the W3C and Chrome, and prove that the fixed Web Payment APIs indeed satisfy strong security properties.}, author = {Do, Quoc Huy and Hosseyni, Pedram and K{\"{u}}sters, Ralf and Schmitz, Guido and Wenzler, Nils and W{\"{u}}rtele, Tim}, institution = {Cryptology ePrint Archive}, number = {2021/1012}, title = {{A Formal Security Analysis of the W3C Web Payment APIs: Attacks and Verification}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/dohosseynikuestersschmitzwenzlerwuertele-iacr-2021.pdf}, year = 2021 }
  Link
  https://publ.sec.uni-stuttgart.de/dohosseynikuestersschmitzwenzlerwuertele-iacr-2021.pdf
2019
1. Guido Schmitz, “Privacy-Preserving Web Single Sign-On: Formal Security Analysis and Design,” University of Stuttgart, 2019.
  Abstract
  Web-based single sign-on (SSO) systems enable Web sites, so-called relying parties (RPs), to outsource user authentication to other entities, so-called identity providers (IdPs). Such systems are widely deployed in the Web, e.g., Facebook Login or Google Sign-in. RPs do not need to maintain authentication data of their users, and users can log in at RPs in a convenient way. Fundamental to SSO is security: The SSO protocol must not permit an attacker to impersonate anyone else, nor must it allow a false identity to be imposed on anyone. If this is not the case, attacks are possible that have devastating effects on the security of RPs and their users. While aiming at security, most SSO systems, however, neglect privacy. IdPs can track their users as they (by design) learn at which RP a user logs in. This lack of privacy allows IdPs to create extensive user profiles and might cause some users not to use SSO at all. Moreover, IdPs are enabled to decide ad-hoc whether they allow a user to log in at a specific RP. Therefore, privacy-preserving systems, which do not reveal to IdPs to which RP a user would like to log in or has logged in, are highly desirable in many situations. The design of such systems, however, is very challenging because privacy can easily be compromised. So far, only one SSO system has been proposed with this kind of privacy in mind: Mozilla's BrowserID (a.k.a. Mozilla Persona). In this thesis, we use the Web Infrastructure Model (WIM) to analyze the security of SSO protocols. The WIM is the most comprehensive formal model of the Web infrastructure to date, which applies to a wide range of Web applications and standards. We also extend the WIM to be able to analyze privacy. We use the extended WIM to, for the first time, carry out a systematic and rigorous formal analysis of privacy for Web SSO systems. Using our approach, we analyze the Web SSO system BrowserID. As a result of this first rigorous analysis of an SSO system in the Web infrastructure, we find severe attacks. These attacks not only affect the security of BrowserID but also show that BrowserID's unique privacy claim does not hold. We propose fixes for BrowserID and prove that the fixed system provides security. Regarding privacy, we show that BrowserID, unfortunately, is broken beyond repair. Inspired by BrowserID's goal, we propose the first privacy-preserving Web SSO system, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). SPRESSO is easy to use, decentralized and based solely on native Web features. We design SPRESSO within the WIM right from the start and prove that SPRESSO satisfies strong security and privacy guarantees.
  BibTeX
  @phdthesis{Schmitz-PhDThesis-2019, abstract = {Web-based single sign-on (SSO) systems enable Web sites, so-called relying parties (RPs), to outsource user authentication to other entities, so-called identity providers (IdPs). Such systems are widely deployed in the Web, e.g., Facebook Login or Google Sign-in. RPs do not need to maintain authentication data of their users, and users can log in at RPs in a convenient way. Fundamental to SSO is security: The SSO protocol must not permit an attacker to impersonate anyone else, nor must it allow a false identity to be imposed on anyone. If this is not the case, attacks are possible that have devastating effects on the security of RPs and their users. While aiming at security, most SSO systems, however, neglect privacy. IdPs can track their users as they (by design) learn at which RP a user logs in. This lack of privacy allows IdPs to create extensive user profiles and might cause some users not to use SSO at all. Moreover, IdPs are enabled to decide ad-hoc whether they allow a user to log in at a specific RP. Therefore, privacy-preserving systems, which do not reveal to IdPs to which RP a user would like to log in or has logged in, are highly desirable in many situations. The design of such systems, however, is very challenging because privacy can easily be compromised. So far, only one SSO system has been proposed with this kind of privacy in mind: Mozilla's BrowserID (a.k.a. Mozilla Persona). In this thesis, we use the Web Infrastructure Model (WIM) to analyze the security of SSO protocols. The WIM is the most comprehensive formal model of the Web infrastructure to date, which applies to a wide range of Web applications and standards. We also extend the WIM to be able to analyze privacy. We use the extended WIM to, for the first time, carry out a systematic and rigorous formal analysis of privacy for Web SSO systems. Using our approach, we analyze the Web SSO system BrowserID. As a result of this first rigorous analysis of an SSO system in the Web infrastructure, we find severe attacks. These attacks not only affect the security of BrowserID but also show that BrowserID's unique privacy claim does not hold. We propose fixes for BrowserID and prove that the fixed system provides security. Regarding privacy, we show that BrowserID, unfortunately, is broken beyond repair. Inspired by BrowserID's goal, we propose the first privacy-preserving Web SSO system, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). SPRESSO is easy to use, decentralized and based solely on native Web features. We design SPRESSO within the WIM right from the start and prove that SPRESSO satisfies strong security and privacy guarantees.}, author = {Schmitz, Guido}, publisher = {University of Stuttgart}, title = {{Privacy-Preserving Web Single Sign-On: Formal Security Analysis and Design}}, url = {https://publ.sec.uni-stuttgart.de/schmitz-phdthesis-2019.pdf}, year = 2019 }
  Link
  https://publ.sec.uni-stuttgart.de/schmitz-phdthesis-2019.pdf
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), IEEE Computer Society, 2019, pp. 1054–1072.
  Abstract
  Forced by regulations and industry demand, banks worldwide are working to open their customers' online banking accounts to third-party services via web-based APIs. By using these so-called Open Banking APIs, third-party companies, such as FinTechs, are able to read information about and initiate payments from their users' bank accounts. Such access to financial data and resources needs to meet particularly high security requirements to protect customers. One of the most promising standards in this segment is the OpenID Financial-grade API (FAPI), currently under development in an open process by the OpenID Foundation and backed by large industry partners. The FAPI is a profile of OAuth 2.0 designed for high-risk scenarios and aiming to be secure against very strong attackers. To achieve this level of security, the FAPI employs a range of mechanisms that have been developed to harden OAuth 2.0, such as Code and Token Binding (including mTLS and OAUTB), JWS Client Assertions, and Proof Key for Code Exchange. In this paper, we perform a rigorous, systematic formal analysis of the security of the FAPI, based on an existing comprehensive model of the web infrastructure - the Web Infrastructure Model (WIM) proposed by Fett, Küsters, and Schmitz. To this end, we first develop a precise model of the FAPI in the WIM, including different profiles for read-only and read-write access, different flows, different types of clients, and different combinations of security features, capturing the complex interactions in a web-based environment. We then use our model of the FAPI to precisely define central security properties. In an attempt to prove these properties, we uncover partly severe attacks, breaking authentication, authorization, and session integrity properties. We develop mitigations against these attacks and finally are able to formally prove the security of a fixed version of the FAPI. Although financial applications are high-stakes environments, this work is the first to formally analyze and, importantly, verify an Open Banking security profile. By itself, this analysis is an important contribution to the development of the FAPI since it helps to define exact security properties and attacker models, and to avoid severe security risks before the first implementations of the standard go live. Of independent interest, we also uncover weaknesses in the aforementioned security mechanisms for hardening OAuth 2.0. We illustrate that these mechanisms do not necessarily achieve the security properties they have been designed for.
  BibTeX
  @inproceedings{FettHosseyniKuesters-FAPI-SP-2019, abstract = {Forced by regulations and industry demand, banks worldwide are working to open their customers' online banking accounts to third-party services via web-based APIs. By using these so-called Open Banking APIs, third-party companies, such as FinTechs, are able to read information about and initiate payments from their users' bank accounts. Such access to financial data and resources needs to meet particularly high security requirements to protect customers. One of the most promising standards in this segment is the OpenID Financial-grade API (FAPI), currently under development in an open process by the OpenID Foundation and backed by large industry partners. The FAPI is a profile of OAuth 2.0 designed for high-risk scenarios and aiming to be secure against very strong attackers. To achieve this level of security, the FAPI employs a range of mechanisms that have been developed to harden OAuth 2.0, such as Code and Token Binding (including mTLS and OAUTB), JWS Client Assertions, and Proof Key for Code Exchange. In this paper, we perform a rigorous, systematic formal analysis of the security of the FAPI, based on an existing comprehensive model of the web infrastructure - the Web Infrastructure Model (WIM) proposed by Fett, K{\"u}sters, and Schmitz. To this end, we first develop a precise model of the FAPI in the WIM, including different profiles for read-only and read-write access, different flows, different types of clients, and different combinations of security features, capturing the complex interactions in a web-based environment. We then use our model of the FAPI to precisely define central security properties. In an attempt to prove these properties, we uncover partly severe attacks, breaking authentication, authorization, and session integrity properties. We develop mitigations against these attacks and finally are able to formally prove the security of a fixed version of the FAPI. Although financial applications are high-stakes environments, this work is the first to formally analyze and, importantly, verify an Open Banking security profile. By itself, this analysis is an important contribution to the development of the FAPI since it helps to define exact security properties and attacker models, and to avoid severe security risks before the first implementations of the standard go live. Of independent interest, we also uncover weaknesses in the aforementioned security mechanisms for hardening OAuth 2.0. We illustrate that these mechanisms do not necessarily achieve the security properties they have been designed for.}, author = {Fett, Daniel and Hosseyni, Pedram and K{\"u}sters, Ralf}, booktitle = {{2019 IEEE Symposium on Security and Privacy (S{\&}P 2019)}}, month = {5}, pages = {1054-1072}, publisher = {IEEE Computer Society}, title = {{An Extensive Formal Security Analysis of the OpenID Financial-grade API}}, url = {https://publ.sec.uni-stuttgart.de/fetthosseynikuesters-fapi-sp-2019.pdf}, volume = 1, year = 2019 }
  Link
  https://publ.sec.uni-stuttgart.de/fetthosseynikuesters-fapi-sp-2019.pdf
3. Daniel Fett, Pedram Hosseyni, and Ralf Küsters, “An Extensive Formal Security Analysis of the OpenID Financial-grade API,” arXiv, arXiv:1901.11520, 2019. Available at http://arxiv.org/abs/1901.11520.
  Abstract
  Forced by regulations and industry demand, banks worldwide are working to open their customers' online banking accounts to third-party services via web-based APIs. By using these so-called Open Banking APIs, third-party companies, such as FinTechs, are able to read information about and initiate payments from their users' bank accounts. Such access to financial data and resources needs to meet particularly high security requirements to protect customers. One of the most promising standards in this segment is the OpenID Financial-grade API (FAPI), currently under development in an open process by the OpenID Foundation and backed by large industry partners. The FAPI is a profile of OAuth 2.0 designed for high-risk scenarios and aiming to be secure against very strong attackers. To achieve this level of security, the FAPI employs a range of mechanisms that have been developed to harden OAuth 2.0, such as Code and Token Binding (including mTLS and OAUTB), JWS Client Assertions, and Proof Key for Code Exchange. In this paper, we perform a rigorous, systematic formal analysis of the security of the FAPI, based on an existing comprehensive model of the web infrastructure - the Web Infrastructure Model (WIM) proposed by Fett, Küsters, and Schmitz. To this end, we first develop a precise model of the FAPI in the WIM, including different profiles for read-only and read-write access, different flows, different types of clients, and different combinations of security features, capturing the complex interactions in a web-based environment. We then use our model of the FAPI to precisely define central security properties. In an attempt to prove these properties, we uncover partly severe attacks, breaking authentication, authorization, and session integrity properties. We develop mitigations against these attacks and finally are able to formally prove the security of a fixed version of the FAPI. Although financial applications are high-stakes environments, this work is the first to formally analyze and, importantly, verify an Open Banking security profile. By itself, this analysis is an important contribution to the development of the FAPI since it helps to define exact security properties and attacker models, and to avoid severe security risks before the first implementations of the standard go live. Of independent interest, we also uncover weaknesses in the aforementioned security mechanisms for hardening OAuth 2.0. We illustrate that these mechanisms do not necessarily achieve the security properties they have been designed for.
  BibTeX
  @techreport{FettHosseyniKuesters-TR-FAPI-2018, abstract = {Forced by regulations and industry demand, banks worldwide are working to open their customers' online banking accounts to third-party services via web-based APIs. By using these so-called Open Banking APIs, third-party companies, such as FinTechs, are able to read information about and initiate payments from their users' bank accounts. Such access to financial data and resources needs to meet particularly high security requirements to protect customers. One of the most promising standards in this segment is the OpenID Financial-grade API (FAPI), currently under development in an open process by the OpenID Foundation and backed by large industry partners. The FAPI is a profile of OAuth 2.0 designed for high-risk scenarios and aiming to be secure against very strong attackers. To achieve this level of security, the FAPI employs a range of mechanisms that have been developed to harden OAuth 2.0, such as Code and Token Binding (including mTLS and OAUTB), JWS Client Assertions, and Proof Key for Code Exchange. In this paper, we perform a rigorous, systematic formal analysis of the security of the FAPI, based on an existing comprehensive model of the web infrastructure - the Web Infrastructure Model (WIM) proposed by Fett, K{\"u}sters, and Schmitz. To this end, we first develop a precise model of the FAPI in the WIM, including different profiles for read-only and read-write access, different flows, different types of clients, and different combinations of security features, capturing the complex interactions in a web-based environment. We then use our model of the FAPI to precisely define central security properties. In an attempt to prove these properties, we uncover partly severe attacks, breaking authentication, authorization, and session integrity properties. We develop mitigations against these attacks and finally are able to formally prove the security of a fixed version of the FAPI. Although financial applications are high-stakes environments, this work is the first to formally analyze and, importantly, verify an Open Banking security profile. By itself, this analysis is an important contribution to the development of the FAPI since it helps to define exact security properties and attacker models, and to avoid severe security risks before the first implementations of the standard go live. Of independent interest, we also uncover weaknesses in the aforementioned security mechanisms for hardening OAuth 2.0. We illustrate that these mechanisms do not necessarily achieve the security properties they have been designed for.}, author = {Fett, Daniel and Hosseyni, Pedram and K{\"u}sters, Ralf}, institution = {arXiv}, note = {Available at \url{http://arxiv.org/abs/1901.11520}.}, number = {arXiv:1901.11520}, title = {{An Extensive Formal Security Analysis of the OpenID Financial-grade API}}, url = {https://publ.sec.uni-stuttgart.de/fetthosseynikuesters-tr-fapi-2018.pdf}, year = 2019 }
  Link
  https://publ.sec.uni-stuttgart.de/fetthosseynikuesters-tr-fapi-2018.pdf
2018
1. Daniel Fett, “An Expressive Formal Model of the Web Infrastructure,” 2018. received an award from the ``Vereinigung von Freunden der Universität Stuttgart’’ in 2019.
  Abstract
  The World Wide Web is arguably the most important medium of our time. Billions of users rely on the security of the web each day for tasks such as banking, shopping, and business and private communication. The web is a heterogeneous infrastructure developing at a high pace. The question of whether the web infrastructure or certain web applications are secure is not easy to answer. Standards and applications today are reviewed by experts before they are deployed, but all too often even serious security vulnerabilities are simply overlooked. In this thesis, we propose a formal model for the web infrastructure which enables a rigorous formal analysis of security and privacy in the web. Our model is the most comprehensive and expressive model of the web infrastructure to date. It facilitates 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. As a case study we analyze the security of two important standards for federated authorization and authentication, OAuth 2.0 and OpenID Connect. Standardized by the IETF and OpenID Foundation, respectively, they are among the most widely deployed single sign-on systems in the web. For our analysis, we develop detailed formal models for both systems based on our model of the web infrastructure. These models then allow us to precisely define the security goals of authentication, authorization and session integrity. While proving security with respect to these goals, we found a total of five new attacks on the two single sign-on systems, breaking all of the security goals. In particular OAuth 2.0 had been analyzed many times before; the fact that we were able to find new attacks in OAuth 2.0 demonstrates the potential of rigorous analyses in our web infrastructure model. We develop fixes against the underlying vulnerabilities and are then able to prove the security of OAuth 2.0 and OpenID Connect. Since our results are based on a comprehensive model, our proofs can exclude large classes of attacks against OAuth and OpenID Connect, including yet unknown attack vectors. Our attacks and fixes led to the development of new security recommendations by the standardization organizations.
  BibTeX
  @phdthesis{Fett-PhDThesis-2018, abstract = {The World Wide Web is arguably the most important medium of our time. Billions of users rely on the security of the web each day for tasks such as banking, shopping, and business and private communication. The web is a heterogeneous infrastructure developing at a high pace. The question of whether the web infrastructure or certain web applications are secure is not easy to answer. Standards and applications today are reviewed by experts before they are deployed, but all too often even serious security vulnerabilities are simply overlooked. In this thesis, we propose a formal model for the web infrastructure which enables a rigorous formal analysis of security and privacy in the web. Our model is the most comprehensive and expressive model of the web infrastructure to date. It facilitates 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. As a case study we analyze the security of two important standards for federated authorization and authentication, OAuth 2.0 and OpenID Connect. Standardized by the IETF and OpenID Foundation, respectively, they are among the most widely deployed single sign-on systems in the web. For our analysis, we develop detailed formal models for both systems based on our model of the web infrastructure. These models then allow us to precisely define the security goals of authentication, authorization and session integrity. While proving security with respect to these goals, we found a total of five new attacks on the two single sign-on systems, breaking all of the security goals. In particular OAuth 2.0 had been analyzed many times before; the fact that we were able to find new attacks in OAuth 2.0 demonstrates the potential of rigorous analyses in our web infrastructure model. We develop fixes against the underlying vulnerabilities and are then able to prove the security of OAuth 2.0 and OpenID Connect. Since our results are based on a comprehensive model, our proofs can exclude large classes of attacks against OAuth and OpenID Connect, including yet unknown attack vectors. Our attacks and fixes led to the development of new security recommendations by the standardization organizations.}, author = {Fett, Daniel}, note = {received an award from the ``Vereinigung von Freunden der Universit{\"a}t Stuttgart'' in 2019}, title = {{An Expressive Formal Model of the Web Infrastructure}}, url = {https://publ.sec.uni-stuttgart.de/fett-phdthesis-2018.pdf}, year = 2018 }
  Link
  https://publ.sec.uni-stuttgart.de/fett-phdthesis-2018.pdf
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), IEEE Computer Society, 2017, pp. 189--202.
  Abstract
  Web-based single sign-on (SSO) services such as Google Sign-In and Log In with Paypal are based on the OpenID Connect protocol. This protocol enables so-called relying parties to delegate user authentication to so-called identity providers. OpenID Connect is one of the newest and most widely deployed single sign-on protocols on the web. Despite its importance, it has not received much attention from security researchers so far, and in particular, has not undergone any rigorous security analysis. In this paper, we carry out the first in-depth security analysis of OpenID Connect. To this end, we use a comprehensive generic model of the web to develop a detailed formal model of OpenID Connect. Based on this model, we then precisely formalize and prove central security properties for OpenID Connect, including authentication, authorization, and session integrity properties. In our modeling of OpenID Connect, we employ security measures in order to avoid attacks on OpenID Connect that have been discovered previously and new attack variants that we document for the first time in this paper. Based on these security measures, we propose security guidelines for implementors of OpenID Connect. Our formal analysis demonstrates that these guidelines are in fact effective and sufficient.
  BibTeX
  @inproceedings{FettKuestersSchmitz-CSF-2017, abstract = {Web-based single sign-on (SSO) services such as Google Sign-In and Log In with Paypal are based on the OpenID Connect protocol. This protocol enables so-called relying parties to delegate user authentication to so-called identity providers. OpenID Connect is one of the newest and most widely deployed single sign-on protocols on the web. Despite its importance, it has not received much attention from security researchers so far, and in particular, has not undergone any rigorous security analysis. In this paper, we carry out the first in-depth security analysis of OpenID Connect. To this end, we use a comprehensive generic model of the web to develop a detailed formal model of OpenID Connect. Based on this model, we then precisely formalize and prove central security properties for OpenID Connect, including authentication, authorization, and session integrity properties. In our modeling of OpenID Connect, we employ security measures in order to avoid attacks on OpenID Connect that have been discovered previously and new attack variants that we document for the first time in this paper. Based on these security measures, we propose security guidelines for implementors of OpenID Connect. Our formal analysis demonstrates that these guidelines are in fact effective and sufficient.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, booktitle = {{IEEE} 30th Computer Security Foundations Symposium ({CSF} 2017)}, doi = {10.1109/CSF.2017.20}, pages = {189--202}, publisher = {IEEE Computer Society}, title = {{The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-csf-2017.pdf}, year = 2017 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-csf-2017.pdf
  DOI
  10.1109/CSF.2017.20
2. Daniel Fett, Ralf Küsters, and Guido Schmitz, “The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines,” arXiv, arXiv:1704.08539, 2017. Available at http://arxiv.org/abs/1704.08539.
  Abstract
  Web-based single sign-on (SSO) services such as Google Sign-In and Log In with Paypal are based on the OpenID Connect protocol. This protocol enables so-called relying parties to delegate user authentication to so-called identity providers. OpenID Connect is one of the newest and most widely deployed single sign-on protocols on the web. Despite its importance, it has not received much attention from security researchers so far, and in particular, has not undergone any rigorous security analysis. In this paper, we carry out the first in-depth security analysis of OpenID Connect. To this end, we use a comprehensive generic model of the web to develop a detailed formal model of OpenID Connect. Based on this model, we then precisely formalize and prove central security properties for OpenID Connect, including authentication, authorization, and session integrity properties. In our modeling of OpenID Connect, we employ security measures in order to avoid attacks on OpenID Connect that have been discovered previously and new attack variants that we document for the first time in this paper. Based on these security measures, we propose security guidelines for implementors of OpenID Connect. Our formal analysis demonstrates that these guidelines are in fact effective and sufficient.
  BibTeX
  @techreport{FettKuestersSchmitz-TR-OIDC-2017, abstract = {Web-based single sign-on (SSO) services such as Google Sign-In and Log In with Paypal are based on the OpenID Connect protocol. This protocol enables so-called relying parties to delegate user authentication to so-called identity providers. OpenID Connect is one of the newest and most widely deployed single sign-on protocols on the web. Despite its importance, it has not received much attention from security researchers so far, and in particular, has not undergone any rigorous security analysis. In this paper, we carry out the first in-depth security analysis of OpenID Connect. To this end, we use a comprehensive generic model of the web to develop a detailed formal model of OpenID Connect. Based on this model, we then precisely formalize and prove central security properties for OpenID Connect, including authentication, authorization, and session integrity properties. In our modeling of OpenID Connect, we employ security measures in order to avoid attacks on OpenID Connect that have been discovered previously and new attack variants that we document for the first time in this paper. Based on these security measures, we propose security guidelines for implementors of OpenID Connect. Our formal analysis demonstrates that these guidelines are in fact effective and sufficient.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, institution = {arXiv}, note = {Available at \url{http://arxiv.org/abs/1704.08539}.}, number = {arXiv:1704.08539}, title = {{The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-tr-oidc-2017.pdf}, year = 2017 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-tr-oidc-2017.pdf
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), ACM, 2016, pp. 1204--1215.
  Abstract
  The OAuth 2.0 protocol is one of the most widely deployed authorization/single sign-on (SSO) protocols and also serves as the foundation for the new SSO standard OpenID Connect. Despite the popularity of OAuth, so far analysis efforts were mostly targeted at finding bugs in specific implementations and were based on formal models which abstract from many web features or did not provide a formal treatment at all. In this paper, we carry out the first extensive formal analysis of the OAuth 2.0 standard in an expressive web model. Our analysis aims at establishing strong authorization, authentication, and session integrity guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth grant types (authorization code grant, implicit grant, resource owner password credentials grant, and the client credentials grant) are covered. They may even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties, identity providers, and browsers are considered as well. Our modeling and analysis of the OAuth 2.0 standard assumes that security recommendations and best practices are followed, in order to avoid obvious and known attacks. When proving the security of OAuth in our model, we discovered four attacks which break the security of OAuth. The vulnerabilities can be exploited in practice and are present also in OpenID Connect. We propose fixes for the identified vulnerabilities, and then, for the first time, actually prove the security of OAuth in an expressive web model. In particular, we show that the fixed version of OAuth (with security recommendations and best practices in place) provides the authorization, authentication, and session integrity properties we specify.
  BibTeX
  @inproceedings{FettKuestersSchmitz-CCS-2016, abstract = {The OAuth 2.0 protocol is one of the most widely deployed authorization/single sign-on (SSO) protocols and also serves as the foundation for the new SSO standard OpenID Connect. Despite the popularity of OAuth, so far analysis efforts were mostly targeted at finding bugs in specific implementations and were based on formal models which abstract from many web features or did not provide a formal treatment at all. In this paper, we carry out the first extensive formal analysis of the OAuth 2.0 standard in an expressive web model. Our analysis aims at establishing strong authorization, authentication, and session integrity guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth grant types (authorization code grant, implicit grant, resource owner password credentials grant, and the client credentials grant) are covered. They may even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties, identity providers, and browsers are considered as well. Our modeling and analysis of the OAuth 2.0 standard assumes that security recommendations and best practices are followed, in order to avoid obvious and known attacks. When proving the security of OAuth in our model, we discovered four attacks which break the security of OAuth. The vulnerabilities can be exploited in practice and are present also in OpenID Connect. We propose fixes for the identified vulnerabilities, and then, for the first time, actually prove the security of OAuth in an expressive web model. In particular, we show that the fixed version of OAuth (with security recommendations and best practices in place) provides the authorization, authentication, and session integrity properties we specify.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, booktitle = {{Proceedings of the 23rd {ACM} {SIGSAC} Conference on Computer and Communications Security (CCS 2016)}}, doi = {10.1145/2976749.2978385}, pages = {1204--1215}, publisher = {ACM}, title = {{A Comprehensive Formal Security Analysis of OAuth 2.0}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-ccs-2016.pdf}, year = 2016 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-ccs-2016.pdf
  DOI
  10.1145/2976749.2978385
2. Daniel Fett, Ralf Küsters, and Guido Schmitz, “A Comprehensive Formal Security Analysis of OAuth 2.0,” arXiv, arXiv:1601.01229, 2016. Available at http://arxiv.org/abs/1601.01229.
  Abstract
  The OAuth 2.0 protocol is one of the most widely deployed authorization/single sign-on (SSO) protocols and also serves as the foundation for the new SSO standard OpenID Connect. Despite the popularity of OAuth, so far analysis efforts were mostly targeted at finding bugs in specific implementations and were based on formal models which abstract from many web features or did not provide a formal treatment at all. In this paper, we carry out the first extensive formal analysis of the OAuth 2.0 standard in an expressive web model. Our analysis aims at establishing strong authorization, authentication, and session integrity guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth grant types (authorization code grant, implicit grant, resource owner password credentials grant, and the client credentials grant) are covered. They may even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties, identity providers, and browsers are considered as well. Our modeling and analysis of the OAuth 2.0 standard assumes that security recommendations and best practices are followed, in order to avoid obvious and known attacks. When proving the security of OAuth in our model, we discovered four attacks which break the security of OAuth. The vulnerabilities can be exploited in practice and are present also in OpenID Connect. We propose fixes for the identified vulnerabilities, and then, for the first time, actually prove the security of OAuth in an expressive web model. In particular, we show that the fixed version of OAuth (with security recommendations and best practices in place) provides the authorization, authentication, and session integrity properties we specify.
  BibTeX
  @techreport{FettKuestersSchmitz-TR-OAuth-2016, abstract = {The OAuth 2.0 protocol is one of the most widely deployed authorization/single sign-on (SSO) protocols and also serves as the foundation for the new SSO standard OpenID Connect. Despite the popularity of OAuth, so far analysis efforts were mostly targeted at finding bugs in specific implementations and were based on formal models which abstract from many web features or did not provide a formal treatment at all. In this paper, we carry out the first extensive formal analysis of the OAuth 2.0 standard in an expressive web model. Our analysis aims at establishing strong authorization, authentication, and session integrity guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth grant types (authorization code grant, implicit grant, resource owner password credentials grant, and the client credentials grant) are covered. They may even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties, identity providers, and browsers are considered as well. Our modeling and analysis of the OAuth 2.0 standard assumes that security recommendations and best practices are followed, in order to avoid obvious and known attacks. When proving the security of OAuth in our model, we discovered four attacks which break the security of OAuth. The vulnerabilities can be exploited in practice and are present also in OpenID Connect. We propose fixes for the identified vulnerabilities, and then, for the first time, actually prove the security of OAuth in an expressive web model. In particular, we show that the fixed version of OAuth (with security recommendations and best practices in place) provides the authorization, authentication, and session integrity properties we specify.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, institution = {arXiv}, note = {Available at \url{http://arxiv.org/abs/1601.01229}.}, number = {arXiv:1601.01229}, title = {{A Comprehensive Formal Security Analysis of OAuth 2.0}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-tr-oauth-2016.pdf}, year = 2016 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-tr-oauth-2016.pdf
2015
1. Daniel Fett, Ralf Küsters, and Guido Schmitz, “SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web,” arXiv, arXiv:1508.01719, 2015. Available at http://arxiv.org/abs/1508.01719.
  Abstract
  Single sign-on (SSO) systems, such as OpenID and OAuth, allow web sites, so-called relying parties (RPs), to delegate user authentication to identity providers (IdPs), such as Facebook or Google. These systems are very popular, as they provide a convenient means for users to log in at RPs and move much of the burden of user authentication from RPs to IdPs. There is, however, a downside to current systems, as they do not respect users' privacy: IdPs learn at which RP a user logs in. With one exception, namely Mozilla's BrowserID system (a.k.a. Mozilla Persona), current SSO systems were not even designed with user privacy in mind. Unfortunately, recently discovered attacks, which exploit design flaws of BrowserID, show that BrowserID does not provide user privacy either. In this paper, we therefore propose the first privacy-respecting SSO system for the web, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). The system is easy to use, decentralized, and platform independent. It is based solely on standard HTML5 and web features and uses no browser extensions, plug-ins, or other executables. Existing SSO systems and the numerous attacks on such systems illustrate that the design of secure SSO systems is highly non-trivial. We therefore also carry out a formal analysis of SPRESSO based on an expressive model of the web in order to formally prove that SPRESSO enjoys strong authentication and privacy properties.
  BibTeX
  @techreport{FettKuestersSchmitz-TR-spresso-2015, abstract = {Single sign-on (SSO) systems, such as OpenID and OAuth, allow web sites, so-called relying parties (RPs), to delegate user authentication to identity providers (IdPs), such as Facebook or Google. These systems are very popular, as they provide a convenient means for users to log in at RPs and move much of the burden of user authentication from RPs to IdPs. There is, however, a downside to current systems, as they do not respect users' privacy: IdPs learn at which RP a user logs in. With one exception, namely Mozilla's BrowserID system (a.k.a. Mozilla Persona), current SSO systems were not even designed with user privacy in mind. Unfortunately, recently discovered attacks, which exploit design flaws of BrowserID, show that BrowserID does not provide user privacy either. In this paper, we therefore propose the first privacy-respecting SSO system for the web, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). The system is easy to use, decentralized, and platform independent. It is based solely on standard HTML5 and web features and uses no browser extensions, plug-ins, or other executables. Existing SSO systems and the numerous attacks on such systems illustrate that the design of secure SSO systems is highly non-trivial. We therefore also carry out a formal analysis of SPRESSO based on an expressive model of the web in order to formally prove that SPRESSO enjoys strong authentication and privacy properties.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, institution = {arXiv}, note = {Available at \url{http://arxiv.org/abs/1508.01719}.}, number = {arXiv:1508.01719}, title = {{SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-tr-spresso-2015.pdf}, year = 2015 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-tr-spresso-2015.pdf
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), ACM, 2015, pp. 1358--1369.
  Abstract
  Single sign-on (SSO) systems, such as OpenID and OAuth, allow web sites, so-called relying parties (RPs), to delegate user authentication to identity providers (IdPs), such as Facebook or Google. These systems are very popular, as they provide a convenient means for users to log in at RPs and move much of the burden of user authentication from RPs to IdPs. There is, however, a downside to current systems, as they do not respect users' privacy: IdPs learn at which RP a user logs in. With one exception, namely Mozilla's BrowserID system (a.k.a. Mozilla Persona), current SSO systems were not even designed with user privacy in mind. Unfortunately, recently discovered attacks, which exploit design flaws of BrowserID, show that BrowserID does not provide user privacy either. In this paper, we therefore propose the first privacy-respecting SSO system for the web, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). The system is easy to use, decentralized, and platform independent. It is based solely on standard HTML5 and web features and uses no browser extensions, plug-ins, or other executables. Existing SSO systems and the numerous attacks on such systems illustrate that the design of secure SSO systems is highly non-trivial. We therefore also carry out a formal analysis of SPRESSO based on an expressive model of the web in order to formally prove that SPRESSO enjoys strong authentication and privacy properties.
  BibTeX
  @inproceedings{FettKuestersSchmitz-CCS-spresso-2015, abstract = {Single sign-on (SSO) systems, such as OpenID and OAuth, allow web sites, so-called relying parties (RPs), to delegate user authentication to identity providers (IdPs), such as Facebook or Google. These systems are very popular, as they provide a convenient means for users to log in at RPs and move much of the burden of user authentication from RPs to IdPs. There is, however, a downside to current systems, as they do not respect users' privacy: IdPs learn at which RP a user logs in. With one exception, namely Mozilla's BrowserID system (a.k.a. Mozilla Persona), current SSO systems were not even designed with user privacy in mind. Unfortunately, recently discovered attacks, which exploit design flaws of BrowserID, show that BrowserID does not provide user privacy either. In this paper, we therefore propose the first privacy-respecting SSO system for the web, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). The system is easy to use, decentralized, and platform independent. It is based solely on standard HTML5 and web features and uses no browser extensions, plug-ins, or other executables. Existing SSO systems and the numerous attacks on such systems illustrate that the design of secure SSO systems is highly non-trivial. We therefore also carry out a formal analysis of SPRESSO based on an expressive model of the web in order to formally prove that SPRESSO enjoys strong authentication and privacy properties.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, booktitle = {{Proceedings of the 22nd {ACM} {SIGSAC} Conference on Computer and Communications Security (CCS 2015)}}, doi = {10.1145/2810103.2813726}, pages = {1358--1369}, publisher = {{ACM}}, title = {{SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-ccs-spresso-2015.pdf}, year = 2015 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-ccs-spresso-2015.pdf
  DOI
  10.1145/2810103.2813726
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, Springer, 2015, pp. 43--65.
  Abstract
  BrowserID is a complex, real-world Single Sign-On (SSO) System for web applications recently developed by Mozilla. It employs new HTML5 features (such as web messaging and web storage) and cryptographic assertions to provide decentralized login, with the intent to respect users' privacy. It can operate in a primary and a secondary identity provider mode. While in the primary mode BrowserID runs with arbitrary identity providers, in the secondary mode there is one identity provider only, namely Mozilla's default identity provider. We recently proposed an expressive general model for the web infrastructure and, based on this web model, analyzed the security of the secondary identity provider mode of BrowserID. The analysis revealed several severe vulnerabilities, which have been fixed by Mozilla. In this paper, we complement our prior work by analyzing the even more complex primary identity provider mode of BrowserID. We do not only study authentication properties as before, but also privacy properties. During our analysis we discovered new and practical attacks that do not apply to the secondary mode: an identity injection attack, which violates a central authentication property of SSO systems, and attacks that break the privacy promise of BrowserID and which do not seem to be fixable without a major redesign of the system. Interestingly, some of our attacks on privacy make use of a browser side channel that, to the best of our knowledge, has not gained a lot of attention so far. For the authentication bug, we propose a fix and formally prove in a slight extension of our general web model that the fixed system satisfies all the authentication requirements we consider. This constitutes the most complex formal analysis of a web application based on an expressive model of the web infrastructure so far. As another contribution, we identify and prove important security properties of generic web features in the extended web model to facilitate future analysis efforts of web standards and web applications.
  BibTeX
  @inproceedings{FettKuestersSchmitz-ESORICS-2015, abstract = {BrowserID is a complex, real-world Single Sign-On (SSO) System for web applications recently developed by Mozilla. It employs new HTML5 features (such as web messaging and web storage) and cryptographic assertions to provide decentralized login, with the intent to respect users' privacy. It can operate in a primary and a secondary identity provider mode. While in the primary mode BrowserID runs with arbitrary identity providers, in the secondary mode there is one identity provider only, namely Mozilla's default identity provider. We recently proposed an expressive general model for the web infrastructure and, based on this web model, analyzed the security of the secondary identity provider mode of BrowserID. The analysis revealed several severe vulnerabilities, which have been fixed by Mozilla. In this paper, we complement our prior work by analyzing the even more complex primary identity provider mode of BrowserID. We do not only study authentication properties as before, but also privacy properties. During our analysis we discovered new and practical attacks that do not apply to the secondary mode: an identity injection attack, which violates a central authentication property of SSO systems, and attacks that break the privacy promise of BrowserID and which do not seem to be fixable without a major redesign of the system. Interestingly, some of our attacks on privacy make use of a browser side channel that, to the best of our knowledge, has not gained a lot of attention so far. For the authentication bug, we propose a fix and formally prove in a slight extension of our general web model that the fixed system satisfies all the authentication requirements we consider. This constitutes the most complex formal analysis of a web application based on an expressive model of the web infrastructure so far. As another contribution, we identify and prove important security properties of generic web features in the extended web model to facilitate future analysis efforts of web standards and web applications.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, booktitle = {{Computer Security - {ESORICS} 2015 - 20th European Symposium on Research in Computer Security, Vienna, Austria, September 21-25, 2015, Proceedings, Part {I}}}, doi = {10.1007/978-3-319-24174-6_3}, pages = {43--65}, publisher = {Springer}, title = {{Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-esorics-2015.pdf}, year = 2015 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-esorics-2015.pdf
  DOI
  10.1007/978-3-319-24174-6_3
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, arXiv:1411.7210v2, 2015. Available at http://arxiv.org/abs/1411.7210v2.
  Abstract
  BrowserID is a complex, real-world Single Sign-On (SSO) System for web applications recently developed by Mozilla. It employs new HTML5 features (such as web messaging and web storage) and cryptographic assertions to provide decentralized login, with the intent to respect users' privacy. It can operate in a primary and a secondary identity provider mode. While in the primary mode BrowserID runs with arbitrary identity providers (IdPs), in the secondary mode there is one IdP only, namely Mozilla's default IdP. We recently proposed an expressive general model for the web infrastructure and, based on this web model, analyzed the security of the secondary IdP mode of BrowserID. The analysis revealed several severe vulnerabilities. In this paper, we complement our prior work by analyzing the even more complex primary IdP mode of BrowserID. We do not only study authentication properties as before, but also privacy properties. During our analysis we discovered new and practical attacks that do not apply to the secondary mode: an identity injection attack, which violates a central authentication property of SSO systems, and attacks that break an important privacy promise of BrowserID and which do not seem to be fixable without a major redesign of the system. Some of our attacks on privacy make use of a browser side channel that has not gained a lot of attention so far. For the authentication bug, we propose a fix and formally prove in a slight extension of our general web model that the fixed system satisfies all the requirements we consider. This constitutes the most complex formal analysis of a web application based on an expressive model of the web infrastructure so far. As another contribution, we identify and prove important security properties of generic web features in the extended web model to facilitate future analysis efforts of web standards and web applications.
  BibTeX
  @techreport{FettKuestersSchmitz-arXiv.1411.7210v2-2015, abstract = {BrowserID is a complex, real-world Single Sign-On (SSO) System for web applications recently developed by Mozilla. It employs new HTML5 features (such as web messaging and web storage) and cryptographic assertions to provide decentralized login, with the intent to respect users' privacy. It can operate in a primary and a secondary identity provider mode. While in the primary mode BrowserID runs with arbitrary identity providers (IdPs), in the secondary mode there is one IdP only, namely Mozilla's default IdP. We recently proposed an expressive general model for the web infrastructure and, based on this web model, analyzed the security of the secondary IdP mode of BrowserID. The analysis revealed several severe vulnerabilities. In this paper, we complement our prior work by analyzing the even more complex primary IdP mode of BrowserID. We do not only study authentication properties as before, but also privacy properties. During our analysis we discovered new and practical attacks that do not apply to the secondary mode: an identity injection attack, which violates a central authentication property of SSO systems, and attacks that break an important privacy promise of BrowserID and which do not seem to be fixable without a major redesign of the system. Some of our attacks on privacy make use of a browser side channel that has not gained a lot of attention so far. For the authentication bug, we propose a fix and formally prove in a slight extension of our general web model that the fixed system satisfies all the requirements we consider. This constitutes the most complex formal analysis of a web application based on an expressive model of the web infrastructure so far. As another contribution, we identify and prove important security properties of generic web features in the extended web model to facilitate future analysis efforts of web standards and web applications.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, institution = {arXiv}, note = {Available at \url{http://arxiv.org/abs/1411.7210v2}.}, number = {arXiv:1411.7210v2}, title = {{Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-arxiv.1411.7210v2-2015.pdf}, year = 2015 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-arxiv.1411.7210v2-2015.pdf
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, arXiv:1403.1866, 2014. Available at http://arxiv.org/abs/1403.1866.
  Abstract
  The web constitutes a complex infrastructure and as demonstrated by numerous attacks, rigorous analysis of standards and web applications is indispensable. Inspired by successful prior work, in particular the work by Akhawe et al. as well as Bansal et al., in this work we propose a formal model for the web infrastructure. While unlike prior works, which aim at automatic analysis, our model so far is not directly amenable to automation, it is much more comprehensive and accurate with respect to the standards and specifications. As such, it can serve as a solid basis for the analysis of a broad range of standards and applications. As a case study and another important contribution of our work, we use our model to carry out the first rigorous analysis of the BrowserID system (a.k.a. Mozilla Persona), a recently developed complex real-world single sign-on system that employs technologies such as AJAX, cross-document messaging, and HTML5 web storage. Our analysis revealed a number of very critical flaws that could not have been captured in prior models. We propose fixes for the flaws, formally state relevant security properties, and prove that the fixed system in a setting with a so-called secondary identity provider satisfies these security properties in our model. The fixes for the most critical flaws have already been adopted by Mozilla and our findings have been rewarded by the Mozilla Security Bug Bounty Program.
  BibTeX
  @techreport{FettKuestersSchmitz-arXiv.1403.1866-2014, abstract = {The web constitutes a complex infrastructure and as demonstrated by numerous attacks, rigorous analysis of standards and web applications is indispensable. Inspired by successful prior work, in particular the work by Akhawe et al. as well as Bansal et al., in this work we propose a formal model for the web infrastructure. While unlike prior works, which aim at automatic analysis, our model so far is not directly amenable to automation, it is much more comprehensive and accurate with respect to the standards and specifications. As such, it can serve as a solid basis for the analysis of a broad range of standards and applications. As a case study and another important contribution of our work, we use our model to carry out the first rigorous analysis of the BrowserID system (a.k.a. Mozilla Persona), a recently developed complex real-world single sign-on system that employs technologies such as AJAX, cross-document messaging, and HTML5 web storage. Our analysis revealed a number of very critical flaws that could not have been captured in prior models. We propose fixes for the flaws, formally state relevant security properties, and prove that the fixed system in a setting with a so-called secondary identity provider satisfies these security properties in our model. The fixes for the most critical flaws have already been adopted by Mozilla and our findings have been rewarded by the Mozilla Security Bug Bounty Program.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, institution = {arXiv}, note = {Available at \url{http://arxiv.org/abs/1403.1866}.}, number = {arXiv:1403.1866}, title = {{An Expressive Model for the Web Infrastructure: Definition and Application to the BrowserID SSO System}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-arxiv.1403.1866-2014.pdf}, year = 2014 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-arxiv.1403.1866-2014.pdf
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), IEEE Computer Society, 2014, pp. 673–688.
  Abstract
  The web constitutes a complex infrastructure and as demonstrated by numerous attacks, rigorous analysis of standards and web applications is indispensable. Inspired by successful prior work, in particular the work by Akhawe et al. as well as Bansal et al., in this work we propose a formal model for the web infrastructure. While unlike prior works, which aim at automatic analysis, our model so far is not directly amenable to automation, it is much more comprehensive and accurate with respect to the standards and specifications. As such, it can serve as a solid basis for the analysis of a broad range of standards and applications. As a case study and another important contribution of our work, we use our model to carry out the first rigorous analysis of the BrowserID system (a.k.a. Mozilla Persona), a recently developed complex real-world single sign-on system that employs technologies such as AJAX, cross-document messaging, and HTML5 web storage. Our analysis revealed a number of very critical flaws that could not have been captured in prior models. We propose fixes for the flaws, formally state relevant security properties, and prove that the fixed system in a setting with a so-called secondary identity provider satisfies these security properties in our model. The fixes for the most critical flaws have already been adopted by Mozilla and our findings have been rewarded by the Mozilla Security Bug Bounty Program.
  BibTeX
  @inproceedings{FettKuestersSchmitz-SP-2014, abstract = {The web constitutes a complex infrastructure and as demonstrated by numerous attacks, rigorous analysis of standards and web applications is indispensable. Inspired by successful prior work, in particular the work by Akhawe et al. as well as Bansal et al., in this work we propose a formal model for the web infrastructure. While unlike prior works, which aim at automatic analysis, our model so far is not directly amenable to automation, it is much more comprehensive and accurate with respect to the standards and specifications. As such, it can serve as a solid basis for the analysis of a broad range of standards and applications. As a case study and another important contribution of our work, we use our model to carry out the first rigorous analysis of the BrowserID system (a.k.a. Mozilla Persona), a recently developed complex real-world single sign-on system that employs technologies such as AJAX, cross-document messaging, and HTML5 web storage. Our analysis revealed a number of very critical flaws that could not have been captured in prior models. We propose fixes for the flaws, formally state relevant security properties, and prove that the fixed system in a setting with a so-called secondary identity provider satisfies these security properties in our model. The fixes for the most critical flaws have already been adopted by Mozilla and our findings have been rewarded by the Mozilla Security Bug Bounty Program.}, author = {Fett, Daniel and K{\"u}sters, Ralf and Schmitz, Guido}, booktitle = {{35th IEEE Symposium on Security and Privacy (S{\&}P 2014)}}, doi = {10.1109/SP.2014.49}, pages = {673-688}, publisher = {IEEE Computer Society}, title = {{An Expressive Model for the Web Infrastructure: Definition and Application to the BrowserID SSO System}}, url = {https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-sp-2014.pdf}, year = 2014 }
  Link
  https://publ.sec.uni-stuttgart.de/fettkuestersschmitz-sp-2014.pdf
  DOI
  10.1109/SP.2014.49

Acknowledgements

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

The Web Infrastructure Model (WIM)

About the WIM

Case Studies and Impact

History

Future Work

Literature and Publications

2024

Abstract

BibTeX

Link

Abstract

BibTeX

Link

2023

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2022

Abstract

BibTeX

Link

DOI

2021

Abstract

BibTeX

Link

2019

Abstract

BibTeX

Link

Abstract

BibTeX

Link

Abstract

BibTeX

Link

2018

Abstract

BibTeX

Link

2017

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2016

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2015

Abstract

BibTeX

Link

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2014

Abstract

BibTeX

Link

Abstract