Formal Methods for Federated Identity Management

Status

This project started in the Spring of 2017 and has been successfully completed.

Researchers

Jürg Anderegg (ZKB)
Prof. David Basin (ETH)
Sven Hammann (ETH)
Ralf Sasse (ETH)

Industry partner

ZKB

Description

The Internet provides access to an ever increasing number of services, many of which require its users to have an account with credentials. This is a considerable cognitive burden for users and leads to password reuse and other poor security practices. Federated identity management services offer a way out of this dilemma. Using federated identity management, a user just needs a single account that employs strong protection (e.g., a unique password and a second authentication factor) at an identity provider and can then log in to other services with this account. An example of a widely used protocol to provide such a single sign-on experience for the user is OpenID Connect, based on the OAuth 2.0 standard.

While these protocols offer many advantages, they also pose security and privacy risks. The protocol specifications are complex, encompassing different modes for different scenarios. Various attacks on the protocols have been found in the past, for which countermeasures have been introduced, further increasing complexity. Furthermore, there are privacy issues that have not been fixed due to a lack of secure and functional alternatives. For example, in OpenID Connect, the identity provider learns to which services the user logs in, and the exact time and frequency of these logins. In light of the General Data Protection Regulation (GDPR), fixing such privacy issues should be considered a priority.

We formally model the protocols as well as desired security and privacy properties, and employ state-of-the-art verification tools. In this way, we find problems with existing protocols and design provably correct protocol improvements. These tools verify the protocols with respect to an unbounded number of participants and sessions, and can therefore provide stronger security and privacy guarantees than manual analysis.

We also model different aspects of a user’s internet identity, which encompasses accounts on various websites. For example, a user can have accounts with multiple identity providers, which are then used to log in to different relying parties. To obtain a more comprehensive analysis, we consider a user’s entire account setup. We model all of the user’s accounts, credentials, devices, and their connections. This methodology is presented in the following publication: User Account Access Graphs, to appear in ACM Conference on Computer and Communications Security (CCS), 2019.