A Comprehensive Formal Security Analysis of OAuth 2.0

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