A Comprehensive Formal Security Analysis of OAuth 2.0

Abstract

The OAuth 2.0 protocol is one of the most widely deployed authorization/single sign-on (SSO) protocols and also serves as the foundation for the new SSO standard OpenID Connect. Despite the popularity of OAuth, so far analysis efforts were mostly targeted at finding bugs in specific implementations and were based on formal models which abstract from many web features or did not provide a formal treatment at all. In this paper, we carry out the first extensive formal analysis of the OAuth 2.0 standard in an expressive web model. Our analysis aims at establishing strong authorization, authentication, and session integrity guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth grant types (authorization code grant, implicit grant, resource owner password credentials grant, and the client credentials grant) are covered. They may even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties, identity providers, and browsers are considered as well. Our modeling and analysis of the OAuth 2.0 standard assumes that security recommendations and best practices are followed, in order to avoid obvious and known attacks. When proving the security of OAuth in our model, we discovered four attacks which break the security of OAuth. The vulnerabilities can be exploited in practice and are present also in OpenID Connect. We propose fixes for the identified vulnerabilities, and then, for the first time, actually prove the security of OAuth in an expressive web model. In particular, we show that the fixed version of OAuth (with security recommendations and best practices in place) provides the authorization, authentication, and session integrity properties we specify.

An abridged version appears in CCS 2016. Parts of this work extend the web model presented in arXiv:1411.7210, arXiv:1403.1866 and arXiv:1508.01719

References in corpus (2)

• On the security of modern Single Sign-On Protocols: Second-Order Vulnerabilities in OpenID Connect
• SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web

Cited by in corpus (8)

• EL PASSO: Privacy-preserving, Asynchronous Single Sign-On
• Decoupled-IFTTT: Constraining Privilege in Trigger-Action Platforms for the Internet of Things
• UPPRESSO: Untraceable and Unlinkable Privacy-PREserving Single Sign-On Services
• Mitigating CSRF attacks on OAuth 2.0 and OpenID Connect
• OAuthGuard: Protecting User Security and Privacy with OAuth 2.0 and OpenID Connect
• Verifying Security Protocols using Dynamic Strategies
• Technical Report on Deploying a highly secured OpenStack Cloud Infrastructure using BradStack as a Case Study
• Exploring Privacy Implications in OAuth Deployments