Privacy-preserving web single sign-on : formal security analysis and design

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.

Webbasierte Single-Sign-On-Systeme (SSO) ermöglichen es Webdiensten, so genannten Relying Parties (RPs), Benutzerauthentifizierung an Dritte, so genannte Identity Provider (IdPs), auszulagern. Solche Systeme, z.B. Facebook Login oder Google Sign-In, sind weit verbreitet. RPs müssen weniger kritische Daten speichern, und Benutzer können sich bequem bei RPs anmelden.

Sicherheit ist für SSO essentiell: Es darf nicht möglich sein, sich als jemand anderes auszugeben, noch darf jemandem eine falsche Identität untergeschoben werden können. Andernfalls sind Angriffe möglich, die verheerend für die Sicherheit von RPs und Benutzern sind.

Privatsphäre spielt für die meisten SSO-Systeme leider keine Rolle. IdPs können ihre Benutzer aussphähen, da sie (per Design) erfahren, bei welchem RP sich ein Benutzer anmeldet. Dadurch können IdPs umfangreiche Profile erstellen und einige Benutzer werden von der Verwendung von SSO abgeschreckt. Zudem können IdPs ad-hoc entscheiden, ob sie einem Benutzer erlauben, sich an einem bestimmten RP anzumelden. Für den Schutz der Privatsphähre darf ein IdP nicht sehen können bei welcher RP sich ein Benutzer anmeldet. Bisher gibt es nur ein nennenswertes SSO-System mit diesem Ziel: Mozillas BrowserID (auch bekannt als Mozilla Persona).

Wir verwenden das Web Infrastructure Model (WIM) um die Sicherheit von SSO-Protokollen zu analysieren. Das WIM ist das bisher umfassendste formale Modell der Web-Infrastruktur. Wir erweitern das WIM, um auch Privatsphähreneigenschaften analysieren zu können. Basierend auf dem so erweiterten Modell führen wir die erste systematische und umfassende Analyse im Hinblick auf Privatssphäre in Web SSO durch.

Mit unserem Ansatz analysieren wir BrowserID. Als Ergebnis dieser ersten rigorosen Analyse eines SSO-Systems in der Web-Infrastruktur finden wir schwerwiegende Angriffe. Diese Angriffe kompromittieren nicht nur die Sicherheit von BrowserID, sondern zeigen auch, dass BrowserID keine Privatsphäre bietet. Wir empfehlen Korrekturen für BrowserID und zeigen, dass BrowserID damit sicher ist. In Bezug auf Privatsphäre ist BrowserID leider irreparabel.

Inspiriert von BrowserIDs Ziel entwerfen wir das erste Privatsphäre-schützende Web-SSO-System, genannt SPRESSO (für Secure Privacy-REspecting Single Sign-On). SPRESSO ist leicht zu bedienen, dezentralisiert und nutzt ausschließlich native Web-Bestandteile. Wir entwickeln SPRESSO von Anfang im WIM und beweisen formal, dass SPRESSO starke Sicherheitseigenschaften erfüllt und die Privatsphäre seiner Nutzer schützt.