The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines

TL;DR

This paper provides the first formal security analysis of the OpenID Connect protocol, identifying vulnerabilities and proposing security guidelines to ensure robust web-based single sign-on security.

Contribution

It introduces a comprehensive formal model of OpenID Connect, proves key security properties, and offers effective security guidelines for implementors.

Findings

Formal security properties of OpenID Connect are validated.

Security measures effectively prevent known and new attack variants.

Guidelines improve protocol robustness against attacks.

Abstract

Web-based single sign-on (SSO) services such as Google Sign-In and Log In with Paypal are based on the OpenID Connect protocol. This protocol enables so-called relying parties to delegate user authentication to so-called identity providers. OpenID Connect is one of the newest and most widely deployed single sign-on protocols on the web. Despite its importance, it has not received much attention from security researchers so far, and in particular, has not undergone any rigorous security analysis. In this paper, we carry out the first in-depth security analysis of OpenID Connect. To this end, we use a comprehensive generic model of the web to develop a detailed formal model of OpenID Connect. Based on this model, we then precisely formalize and prove central security properties for OpenID Connect, including authentication, authorization, and session integrity properties. In our modeling of OpenID Connect, we employ security measures in order to avoid attacks on OpenID Connect that have been discovered previously and new attack variants that we document for the first time in this paper. Based on these security measures, we propose security guidelines for implementors of OpenID Connect. Our formal analysis demonstrates that these guidelines are in fact effective and sufficient.