Position within the page tree

Start
Institute
Team
Würtele, Tim

Tim Würtele

M.Sc.

Ph.D. Student
Institute of Information Security

Contact

+49 711 685 88468
Email

Universitaetsstrasse 38
70569 Stuttgart
Germany
Room: 2.434

Publications

2024
1. Pedram Hosseyni, Ralf Küsters, and Tim Würtele, “Formal Security Analysis of the OpenID FAPI 2.0 Family of Protocols: Accompanying a Standardization Process,” Cryptology ePrint Archive, Technical Report 2024/1540, 2024.
  Abstract
  FAPI 2.0 is a suite of Web protocols developed by the OpenID Foundation's FAPI Working Group (FAPI WG) for third-party data sharing and digital identity in high-risk environments. Even though the specifications are not completely finished, several important entities have started to adopt the FAPI 2.0 protocols, including Norway's national HelseID, Australia's Consumer Data Standards, as well as private companies like Authlete and Australia-based connectID; the predecessor FAPI 1.0 is in widespread use with millions of users. The FAPI WG asked us to accompany the standardization of the FAPI 2.0 protocols with a formal security analysis to proactively identify vulnerabilities before widespread deployment and to provide formal security guarantees for the standards. In this paper, we report on our analysis and findings. Our analysis is based on a detailed model of the Web infrastructure, the so-called Web Infrastructure Model (WIM), which we extend to be able to carry out our analysis of the FAPI 2.0 protocols including important extensions like FAPI-CIBA. Based on the (extended) WIM and formalizations of the security goals and attacker model laid out in the FAPI 2.0 specifications, we provide a formal model of the protocols and carry out a formal security analysis, revealing several attacks. We have worked with the FAPI WG to fix the protocols, resulting in several amendments to the specifications. With these changes in place, we have adjusted our protocol model and formally proved that the security properties hold true under the strong attacker model defined by the FAPI WG.
  BibTeX
  @techreport{HosseyniKuestersWuertele-IACR-2024-1540, abstract = {FAPI 2.0 is a suite of Web protocols developed by the OpenID Foundation's FAPI Working Group (FAPI WG) for third-party data sharing and digital identity in high-risk environments. Even though the specifications are not completely finished, several important entities have started to adopt the FAPI 2.0 protocols, including Norway's national HelseID, Australia's Consumer Data Standards, as well as private companies like Authlete and Australia-based connectID; the predecessor FAPI 1.0 is in widespread use with millions of users. The FAPI WG asked us to accompany the standardization of the FAPI 2.0 protocols with a formal security analysis to proactively identify vulnerabilities before widespread deployment and to provide formal security guarantees for the standards. In this paper, we report on our analysis and findings. Our analysis is based on a detailed model of the Web infrastructure, the so-called Web Infrastructure Model (WIM), which we extend to be able to carry out our analysis of the FAPI 2.0 protocols including important extensions like FAPI-CIBA. Based on the (extended) WIM and formalizations of the security goals and attacker model laid out in the FAPI 2.0 specifications, we provide a formal model of the protocols and carry out a formal security analysis, revealing several attacks. We have worked with the FAPI WG to fix the protocols, resulting in several amendments to the specifications. With these changes in place, we have adjusted our protocol model and formally proved that the security properties hold true 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/1540}, title = {{Formal Security Analysis of the OpenID FAPI 2.0 Family of Protocols: Accompanying a Standardization Process}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/hosseynikuesterswuertele-iacr-2024-1540.pdf}, year = 2024 }
  Link
  https://publ.sec.uni-stuttgart.de/hosseynikuesterswuertele-iacr-2024-1540.pdf
2. Pedram Hosseyni, Ralf Küsters, and Tim Würtele, “Formal Security Analysis of the OpenID FAPI 2.0 Family of Protocols: Accompanying a Standardization Process,” ACM Transactions on Privacy and Security, vol. 28, no. 1, pp. 1--36, 2024.
  Abstract
  FAPI 2.0 is a suite of Web protocols developed by the OpenID Foundation's FAPI Working Group (FAPI WG) for third-party data sharing and digital identity in high-risk environments. Even though the specifications are not completely finished, several important entities have started to adopt the FAPI 2.0 protocols, including Norway's national HelseID, Australia's Consumer Data Standards, as well as private companies like Authlete and Australia-based connectID; the predecessor FAPI 1.0 is in widespread use with millions of users. The FAPI WG asked us to accompany the standardization of the FAPI 2.0 protocols with a formal security analysis to proactively identify vulnerabilities before widespread deployment and to provide formal security guarantees for the standards. In this paper, we report on our analysis and findings. Our analysis is based on a detailed model of the Web infrastructure, the so-called Web Infrastructure Model (WIM), which we extend to be able to carry out our analysis of the FAPI 2.0 protocols including important extensions like FAPI-CIBA. Based on the (extended) WIM and formalizations of the security goals and attacker model laid out in the FAPI 2.0 specifications, we provide a formal model of the protocols and carry out a formal security analysis, revealing several attacks. We have worked with the FAPI WG to fix the protocols, resulting in several amendments to the specifications. With these changes in place, we have adjusted our protocol model and formally proved that the security properties hold true under the strong attacker model defined by the FAPI WG.
  BibTeX
  @article{HosseyniKuestersWuertele-TOPS-2024, abstract = {FAPI 2.0 is a suite of Web protocols developed by the OpenID Foundation's FAPI Working Group (FAPI WG) for third-party data sharing and digital identity in high-risk environments. Even though the specifications are not completely finished, several important entities have started to adopt the FAPI 2.0 protocols, including Norway's national HelseID, Australia's Consumer Data Standards, as well as private companies like Authlete and Australia-based connectID; the predecessor FAPI 1.0 is in widespread use with millions of users. The FAPI WG asked us to accompany the standardization of the FAPI 2.0 protocols with a formal security analysis to proactively identify vulnerabilities before widespread deployment and to provide formal security guarantees for the standards. In this paper, we report on our analysis and findings. Our analysis is based on a detailed model of the Web infrastructure, the so-called Web Infrastructure Model (WIM), which we extend to be able to carry out our analysis of the FAPI 2.0 protocols including important extensions like FAPI-CIBA. Based on the (extended) WIM and formalizations of the security goals and attacker model laid out in the FAPI 2.0 specifications, we provide a formal model of the protocols and carry out a formal security analysis, revealing several attacks. We have worked with the FAPI WG to fix the protocols, resulting in several amendments to the specifications. With these changes in place, we have adjusted our protocol model and formally proved that the security properties hold true under the strong attacker model defined by the FAPI WG.}, author = {Hosseyni, Pedram and K{\"u}sters, Ralf and W{\"u}rtele, Tim}, doi = {10.1145/3699716}, journal = {{ACM Transactions on Privacy and Security}}, number = 1, pages = {1--36}, title = {{Formal Security Analysis of the OpenID FAPI 2.0 Family of Protocols: Accompanying a Standardization Process}}, volume = 28, year = 2024 }
  DOI
  10.1145/3699716
3. 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
4. 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, pp. 589--604.
  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)}}, doi = {10.1109/CSF61375.2024.00002}, pages = {589--604}, 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
  DOI
  10.1109/CSF61375.2024.00002
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
3. Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, and Tim Würtele, “Layered Symbolic Security Analysis in DY*,” in 28th European Symposium on Research in Computer Security (ESORICS 2023), Springer, 2023, pp. 3--21.
  Abstract
  While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY* protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F* modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY* with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest.
  BibTeX
  @inproceedings{Bhargavanetal-ESORICS-2023, abstract = {While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY* protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F* modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY* with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest.}, author = {Bhargavan, Karthikeyan and Bichhawat, Abhishek and Hosseyni, Pedram and K{\"u}sters, Ralf and Pruiksma, Klaas and Schmitz, Guido 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_1}, pages = {3--21}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{Layered Symbolic Security Analysis in DY*}}, url = {https://publ.sec.uni-stuttgart.de/bhargavanetal-iacr-2023-1329.pdf}, volume = 14346, year = 2023 }
  Link
  https://publ.sec.uni-stuttgart.de/bhargavanetal-iacr-2023-1329.pdf
  DOI
  10.1007/978-3-031-51479-1_1
4. Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, and Tim Würtele, “Layered Symbolic Security Analysis in DY*,” Cryptology ePrint Archive, Technical Report 2023/1329, 2023.
  Abstract
  While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY* protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F* modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY* with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest.
  BibTeX
  @techreport{Bhargavanetal-IACR-2023-1329, abstract = {While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY* protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F* modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY* with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest.}, author = {Bhargavan, Karthikeyan and Bichhawat, Abhishek and Hosseyni, Pedram and K{\"u}sters, Ralf and Pruiksma, Klaas and Schmitz, Guido and Waldmann, Clara and W{\"u}rtele, Tim}, institution = {Cryptology ePrint Archive}, number = {2023/1329}, title = {{Layered Symbolic Security Analysis in DY*}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/bhargavanetal-iacr-2023-1329.pdf}, year = 2023 }
  Link
  https://publ.sec.uni-stuttgart.de/bhargavanetal-iacr-2023-1329.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. Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele, “An In-Depth Symbolic Security Analysis of the ACME Standard,” Cryptology ePrint Archive, Technical Report 2021/1457, 2021.
  Abstract
  The ACME certificate issuance and management protocol, standardized as IETF RFC 8555, is an essential element of the web public key infrastructure (PKI). It has been used by Let's Encrypt and other certification authorities to issue over a billion certificates, and a majority of HTTPS connections are now secured with certificates issued through ACME. Despite its importance, however, the security of ACME has not been studied at the same level of depth as other protocol standards like TLS 1.3 or OAuth. Prior formal analyses of ACME only considered the cryptographic core of early draft versions of ACME, ignoring many security-critical low-level details that play a major role in the 100 page RFC, such as recursive data structures, long-running sessions with asynchronous sub-protocols, and the issuance for certificates that cover multiple domains.We present the first in-depth formal security analysis of the ACME standard. Our model of ACME is executable and comprehensive, with a level of detail that lets our ACME client interoperate with other ACME servers. We prove the security of this model using a recent symbolic protocol analysis framework called DY⋆, which in turn is based on the F⋆ programming language. Our analysis accounts for all prior attacks on ACME in the literature, including both cryptographic attacks and low-level attacks on stateful protocol execution. To analyze ACME, we extend DY* with authenticated channels, key substitution attacks, and a concrete execution framework, which are of independent interest. Our security analysis of ACME totaling over 16,000 lines of code is one of the largest proof developments for a cryptographic protocol standard in the literature, and it serves to provide formal security assurances for a crucial component of web security.
  BibTeX
  @techreport{BhargavanBichhavatDoHosseyniKuestersSchmitzWuertele-IACR-2021-1457, abstract = {The ACME certificate issuance and management protocol, standardized as IETF RFC 8555, is an essential element of the web public key infrastructure (PKI). It has been used by Let's Encrypt and other certification authorities to issue over a billion certificates, and a majority of HTTPS connections are now secured with certificates issued through ACME. Despite its importance, however, the security of ACME has not been studied at the same level of depth as other protocol standards like TLS 1.3 or OAuth. Prior formal analyses of ACME only considered the cryptographic core of early draft versions of ACME, ignoring many security-critical low-level details that play a major role in the 100 page RFC, such as recursive data structures, long-running sessions with asynchronous sub-protocols, and the issuance for certificates that cover multiple domains.We present the first in-depth formal security analysis of the ACME standard. Our model of ACME is executable and comprehensive, with a level of detail that lets our ACME client interoperate with other ACME servers. We prove the security of this model using a recent symbolic protocol analysis framework called DY⋆, which in turn is based on the F⋆ programming language. Our analysis accounts for all prior attacks on ACME in the literature, including both cryptographic attacks and low-level attacks on stateful protocol execution. To analyze ACME, we extend DY* with authenticated channels, key substitution attacks, and a concrete execution framework, which are of independent interest. Our security analysis of ACME totaling over 16,000 lines of code is one of the largest proof developments for a cryptographic protocol standard in the literature, and it serves to provide formal security assurances for a crucial component of web security.}, author = {Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc Huy and Hosseyni, Pedram and K{\"u}sters, Ralf and Schmitz, Guido and W{\"u}rtele, Tim}, institution = {Cryptology ePrint Archive}, number = {2021/1457}, title = {{An In-Depth Symbolic Security Analysis of the ACME Standard}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-iacr-2021-1457.pdf}, year = 2021 }
  Link
  https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-iacr-2021-1457.pdf
2. Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele, “A Tutorial-Style Introduction to DY*,” in Protocols, Strands, and Logic: Essays Dedicated to Joshua Guttman on the Occasion of His 66.66 Birthday., D. Dougherty, J. Meseguer, S. A. Mödersheim, and P. Rowe (Eds.). Springer, 2021, pp. 77--97.
  Abstract
  DY* is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F* programming language. Unlike automated symbolic provers, DY* accounts for advanced protocol features like unbounded loops and mutable recursive data structures as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Protocols modeled in DY* can be executed, and hence, tested, and they can even interoperate with real-world counterparts. DY* extends a long line of research on using dependent type systems but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. With this, one can uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. In this paper, we provide a tutorial-style introduction to DY*: We illustrate how to model and prove the security of the ISO-DH protocol, a simple key exchange protocol based on Diffie-Hellman.
  BibTeX
  @incollection{BhargavanBichhavatDoHosseyniKuestersSchmitzWuertele-Guttmanfest-2021, abstract = {DY* is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F* programming language. Unlike automated symbolic provers, DY* accounts for advanced protocol features like unbounded loops and mutable recursive data structures as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Protocols modeled in DY* can be executed, and hence, tested, and they can even interoperate with real-world counterparts. DY* extends a long line of research on using dependent type systems but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. With this, one can uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. In this paper, we provide a tutorial-style introduction to DY*: We illustrate how to model and prove the security of the ISO-DH protocol, a simple key exchange protocol based on Diffie-Hellman.}, author = {Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc Huy and Hosseyni, Pedram and K{\"u}sters, Ralf and Schmitz, Guido and W{\"u}rtele, Tim}, booktitle = {{Protocols, Strands, and Logic: Essays Dedicated to Joshua Guttman on the Occasion of His 66.66 Birthday.}}, doi = {10.1007/978-3-030-91631-2_4}, editor = {Dougherty, Daniel and Meseguer, Jos{\'e} and M{\"o}dersheim, Sebastian Alexander and Rowe, Paul}, pages = {77--97}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{A Tutorial-Style Introduction to DY*}}, url = {https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-guttmanfest-2021.pdf}, volume = 13066, year = 2021 }
  Link
  https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-guttmanfest-2021.pdf
  DOI
  10.1007/978-3-030-91631-2_4
3. 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
4. Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele, “An In-Depth Symbolic Security Analysis of the ACME Standard,” in ACM Conference on Computer and Communications Security (CCS 2021), ACM, 2021, pp. 2601–2617.
  Abstract
  The ACME certificate issuance and management protocol, standardized as IETF RFC 8555, is an essential element of the web public key infrastructure (PKI). It has been used by Let's Encrypt and other certification authorities to issue over a billion certificates, and a majority of HTTPS connections are now secured with certificates issued through ACME. Despite its importance, however, the security of ACME has not been studied at the same level of depth as other protocol standards like TLS 1.3 or OAuth. Prior formal analyses of ACME only considered the cryptographic core of early draft versions of ACME, ignoring many security-critical low-level details that play a major role in the 100 page RFC, such as recursive data structures, long-running sessions with asynchronous sub-protocols, and the issuance for certificates that cover multiple domains.We present the first in-depth formal security analysis of the ACME standard. Our model of ACME is executable and comprehensive, with a level of detail that lets our ACME client interoperate with other ACME servers. We prove the security of this model using a recent symbolic protocol analysis framework called DY⋆, which in turn is based on the F⋆ programming language. Our analysis accounts for all prior attacks on ACME in the literature, including both cryptographic attacks and low-level attacks on stateful protocol execution. To analyze ACME, we extend DY* with authenticated channels, key substitution attacks, and a concrete execution framework, which are of independent interest. Our security analysis of ACME totaling over 16,000 lines of code is one of the largest proof developments for a cryptographic protocol standard in the literature, and it serves to provide formal security assurances for a crucial component of web security.
  BibTeX
  @inproceedings{BhargavanBichhavatDoHosseyniKuestersSchmitzWuertele-CCS-2021, abstract = {The ACME certificate issuance and management protocol, standardized as IETF RFC 8555, is an essential element of the web public key infrastructure (PKI). It has been used by Let's Encrypt and other certification authorities to issue over a billion certificates, and a majority of HTTPS connections are now secured with certificates issued through ACME. Despite its importance, however, the security of ACME has not been studied at the same level of depth as other protocol standards like TLS 1.3 or OAuth. Prior formal analyses of ACME only considered the cryptographic core of early draft versions of ACME, ignoring many security-critical low-level details that play a major role in the 100 page RFC, such as recursive data structures, long-running sessions with asynchronous sub-protocols, and the issuance for certificates that cover multiple domains.We present the first in-depth formal security analysis of the ACME standard. Our model of ACME is executable and comprehensive, with a level of detail that lets our ACME client interoperate with other ACME servers. We prove the security of this model using a recent symbolic protocol analysis framework called DY⋆, which in turn is based on the F⋆ programming language. Our analysis accounts for all prior attacks on ACME in the literature, including both cryptographic attacks and low-level attacks on stateful protocol execution. To analyze ACME, we extend DY* with authenticated channels, key substitution attacks, and a concrete execution framework, which are of independent interest. Our security analysis of ACME totaling over 16,000 lines of code is one of the largest proof developments for a cryptographic protocol standard in the literature, and it serves to provide formal security assurances for a crucial component of web security.}, author = {Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc Huy and Hosseyni, Pedram and K{\"u}sters, Ralf and Schmitz, Guido and W{\"u}rtele, Tim}, booktitle = {{ACM Conference on Computer and Communications Security (CCS 2021)}}, doi = {10.1145/3460120.3484588}, pages = {2601-2617}, publisher = {{ACM}}, title = {{An In-Depth Symbolic Security Analysis of the ACME Standard}}, url = {https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-ccs-2021.pdf}, year = 2021 }
  Link
  https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-ccs-2021.pdf
  DOI
  10.1145/3460120.3484588
5. Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele, “DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code,” in IEEE European Symposium on Security and Privacy (EuroS&P 2021), IEEE, 2021, pp. 523–542.
  Abstract
  We present DY*, a new formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F* programming language. Unlike automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Our work extends a long line of research on using dependent type systems for this task, but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. This approach enables us to uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. DY* is built as a library of F* modules that includes a model of low-level protocol execution, a Dolev-Yao symbolic attacker, and generic security abstractions and lemmas, all verified using F*. The library exposes a high-level API that facilitates succinct security proofs for protocol code. We demonstrate the effectiveness of this approach through a detailed symbolic security analysis of the Signal protocol that is based on an interoperable implementation of the protocol from prior work, and is the first mechanized proof of Signal to account for forward and post-compromise security over an unbounded number of protocol rounds.
  BibTeX
  @inproceedings{BhargavanBichhavatDoHosseyniKuestersSchmitzWuertele-EuroSP-2021, abstract = {We present DY*, a new formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F* programming language. Unlike automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Our work extends a long line of research on using dependent type systems for this task, but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. This approach enables us to uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. DY* is built as a library of F* modules that includes a model of low-level protocol execution, a Dolev-Yao symbolic attacker, and generic security abstractions and lemmas, all verified using F*. The library exposes a high-level API that facilitates succinct security proofs for protocol code. We demonstrate the effectiveness of this approach through a detailed symbolic security analysis of the Signal protocol that is based on an interoperable implementation of the protocol from prior work, and is the first mechanized proof of Signal to account for forward and post-compromise security over an unbounded number of protocol rounds.}, author = {Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc Huy and Hosseyni, Pedram and K{\"u}sters, Ralf and Schmitz, Guido and W{\"u}rtele, Tim}, booktitle = {{IEEE European Symposium on Security and Privacy (EuroS{\&}P 2021)}}, doi = {10.1109/EuroSP51992.2021.00042}, pages = {523-542}, publisher = {IEEE}, title = {{DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code}}, url = {https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-eurosp-2021.pdf}, year = 2021 }
  Link
  https://publ.sec.uni-stuttgart.de/bhargavanbichhavatdohosseynikuestersschmitzwuertele-eurosp-2021.pdf
  DOI
  10.1109/EuroSP51992.2021.00042
2016
1. Tilman Dingler, Corinna Giebler, Ulf Kunze, Tim Würtele, Niels Henze, and Albrecht Schmidt, “Memory displays: investigating the effects of learning in the periphery,” in Proceedings of the 5th ACM International Symposium on Pervasive Displays, PerDis 2016, Oulu, Finland, June 20 - 22, 2016, ACM, 2016, pp. 118--123.
  - Abstract
  - BibTeX
  Abstract
  In our knowledge society knowledge acquisition is vital, but often there is a lack of time and resources. Ubiquitous technologies allow us to place learning cues into homes and work environments and thus invite people to consume information in in the periphery or while passing by. In this work we set out to understand the effects of using peripheral displays in people's homes to show content for knowledge acquisition. We explore different aspects about display placement, content, and application scenarios. In a user study with 15 students preparing for a university exam across 3 weeks we compared the effects of an active learning platform with passive learning through peripheral displays. Our main findings are of qualitative nature and allow us to map out a series of design and usage implications for using peripheral displays to help users commit content to long-term memory.
  BibTeX
  @inproceedings{DinglerGieblerKunzeWurteleHenzeSchmidt-PERDIS-2016, abstract = {In our knowledge society knowledge acquisition is vital, but often there is a lack of time and resources. Ubiquitous technologies allow us to place learning cues into homes and work environments and thus invite people to consume information in in the periphery or while passing by. In this work we set out to understand the effects of using peripheral displays in people's homes to show content for knowledge acquisition. We explore different aspects about display placement, content, and application scenarios. In a user study with 15 students preparing for a university exam across 3 weeks we compared the effects of an active learning platform with passive learning through peripheral displays. Our main findings are of qualitative nature and allow us to map out a series of design and usage implications for using peripheral displays to help users commit content to long-term memory.}, author = {Dingler, Tilman and Giebler, Corinna and Kunze, Ulf and W{\"{u}}rtele, Tim and Henze, Niels and Schmidt, Albrecht}, booktitle = {{Proceedings of the 5th {ACM} International Symposium on Pervasive Displays, PerDis 2016, Oulu, Finland, June 20 - 22, 2016}}, pages = {118--123}, publisher = {{ACM}}, title = {{Memory displays: investigating the effects of learning in the periphery}}, year = 2016 }

PGP Public Key Fingerprint: 6097 087B 72CB 764F 05F3 37E8 BE3E 3CFD FF13 FAD1

Are you a student and want to write a thesis / carry out a project at the SEC?

Please see our notes on theses and projects!

Tim Würtele

Contact

Publications

2024

Abstract

BibTeX

Link

Abstract

BibTeX

DOI

Abstract

BibTeX

Link

Abstract

BibTeX

Link

DOI

2023

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2022

Abstract

BibTeX

Link

DOI

2021

Abstract

BibTeX

Link

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

DOI

2016

Abstract

BibTeX

PGP Public Key Fingerprint:​ ​6097 087B 72CB 764F 05F3 37E8 BE3E 3CFD FF13 FAD1

Are you a student and want to write a thesis / carry out a project at the SEC?

Here you can reach us

Audience

Formalities

Services

Organization

PGP Public Key Fingerprint: 6097 087B 72CB 764F 05F3 37E8 BE3E 3CFD FF13 FAD1