A Comprehensive Formal Security Analysis of OAuth 2.0
A Comprehensive Formal Security Analysis of OAuth 2.0
复制标题
DOI：
10.1145/2976749.2978385
复制
发表时间：
2016-01
期刊：
影响因子：
--
通讯作者：
Daniel Fett;Ralf Küsters;G. Schmitz
中科院分区：
文献类型：
--
作者：
Daniel Fett;Ralf Küsters;G. Schmitz
OAuth 2.0 协议是部署最广泛的授权/单点登录 (SSO) 协议之一，也是新 SSO 标准 OpenID Connect 的基础。尽管 OAuth 很受欢迎，但到目前为止，分析工作主要针对查找特定实现中的错误，并且基于从许多 Web 功能中抽象出来的正式模型，或者根本不提供正式处理。在本文中，我们在富有表现力的 Web 模型中对 OAuth 2.0 标准进行了首次广泛的形式分析。我们的分析旨在建立强大的授权、身份验证和会话完整性保证，为此我们提供了正式的定义。在我们的正式分析中，涵盖了所有四种 OAuth 授予类型（授权代码授予、隐式授予、资源所有者密码凭据授予和客户端凭据授予）。它们甚至可以在相同和不同的依赖方和身份提供商中同时运行，其中也考虑恶意依赖方、身份提供商和浏览器。我们对 OAuth 2.0 标准的建模和分析假设遵循安全建议和最佳实践，以避免明显和已知的攻击。在我们的模型中证明 OAuth 的安全性时，我们发现了四种破坏 OAuth 安全性的攻击。这些漏洞可以在实践中被利用，并且也存在于 OpenID Connect 中。我们针对已识别的漏洞提出修复方案，然后首次在富有表现力的 Web 模型中实际证明 OAuth 的安全性。特别是，我们展示了 OAuth 的固定版本（具有适当的安全建议和最佳实践）提供了我们指定的授权、身份验证和会话完整性属性。
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.