Privacy-preserving Web single sign-on: Formal security analysis and design

Single sign-on (SSO) systems, such as OpenID and OAuth, allow Web sites to delegate user authentication to third parties, such as Facebook or Google. These systems provide a convenient mechanism for users to log in and ease the burden of user authentication for Web sites. Conversely, by integrating such SSO systems, they become a crucial part of the security of the modern Web. So far, it has been hard to prove if Web standards and protocols actually meet their security goals. SSO systems, in particular, need to satisfy strong security and privacy properties. In this thesis, we develop a new systematic approach to rigorously and formally analyze and verify such strong properties with the Web Infrastructure Model (WIM), the most comprehensive model of the Web infrastructure to date. Our analyses reveal severe vulnerabilities in SSO systems that lead to critical attacks against their security and privacy. We propose fixes and formally verify that our proposals are sufficient to establish security. Our analyses, however, also show that even Mozilla's proposal for a privacy-preserving SSO system does not meet its unique privacy goal. To fill this gap, we use our novel approach to develop a new SSO system, SPRESSO, and formally prove that our system indeed enjoys strong security and privacy properties.