The web constitutes a complex infrastructure, with entities such as DNS servers, web servers, and web browsers interacting and communicating using diverse technologies. In the light of numerous attacks on the web infrastructure and web applications that have been reported and the growing complexity of the web, rigorous and systematic security and privacy analyses of the web infrastructure, web standards, and web applications are essential.
To carry out such analyses, we created the most comprehensive formal model of the web infrastructure to date. This model, called Web Infrastructure Model (WIM), allows us to precisely state and prove security and privacy properties of web standards and applications. Using this holistic approach, we can identify vulnerabilities and develop fixes. Moreover, we can even exclude unknown classes of attacks on the systems we analyze.
We successfully applied the WIM to formally analyze several crucial and high-risk web protocols, including the very popular single sign-on and authorization standards OAuth and OpenID Connect (used, e.g., by Google, Facebook, Microsoft, and Amazon). Our analyses uncovered several severe attacks; we suggested fixes, and for the first time proved security and privacy properties for the fixed standards. Several protocol specifications have been revised according to our proposals. Regarding privacy in single sign-on, our results, however, show that no existing protocol provides this property. To fill this gap, we used the WIM to design a new single sign-on system, SPRESSO (Secure Privacy-Respecting Single Sign-On), which provably provides strong security and privacy guarantees.
In an ongoing project, we are currently mechanizing the WIM, which enables us to extract verified code for usage in practice and eases the re-usage of proofs for future, modular analyses. Our approach builds upon F*, an ecosystem consisting of a functional programming language with a rich dependent type system and an SMT-based theorem prover. We already applied the first version of our new mechanized framework to prove security of the Signal protocol (used, e.g., by WhatsApp and Skype) and the ACME standard (used, e.g., by Let's Encrypt).
Guido Schmitz graduated in Computer Science at the University of Trier (Germany) and obtained his doctorate in 2019 at the University of Stuttgart. He became a lecturer in the Information Security Group at Royal Holloway in December 2021.