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 thefoundation for the new SSO standard OpenID Connect. Despite thepopularity of OAuth, so far analysis efforts were mostly targeted atfinding bugs in specific implementations and were based on formalmodels which abstract from many web features or did not providea formal treatment at all.In this paper, we carry out the first extensive formal analysis ofthe OAuth 2.0 standard in an expressive web model. Our analysis aims at establishing strong authorization, authentication, andsession 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. Theymay even run simultaneously in the same and different relying parties and identity providers, where malicious relying parties, identityproviders, and browsers are considered as well. Our modeling andanalysis of the OAuth 2.0 standard assumes that security recommendations and best practices are followed in order to avoid obviousand known attacks.When proving the security of OAuth in our model, we discoveredfour attacks which break the security of OAuth. The vulnerabilitiescan be exploited in practice and are present also in OpenID Connect.We propose fixes for the identified vulnerabilities, and then, forthe first time, actually prove the security of OAuth in an expressiveweb 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.
The OAuth 2.0 authorization framework  defines a web-basedprotocol that allows a user to grant web sites access to her resources(data or services) at other web sites (authorization). The formerweb sites are called relying parties (RP) and the latter are called identity providers (IdP).1 In practice, OAuth 2.0 is often used forauthentication as well. That is, a user can log in at an RP using heridentity managed by an IdP (single sign-on, SSO).Authorization and SSO solutions have found widespread adoption in the web over the last years, with OAuth 2.0 being one of themost popular frameworks. OAuth 2.0, in the following often simply called OAuth,2 is used by identity providers such as Amazon,Facebook, Google, Microsoft, Yahoo, GitHub, LinkedIn, StackExchange, and Dropbox. This enables billions of users to log in atmillions of RPs or share their data with these , making OAuthone of the most used single sign-on systems on the web.OAuth is also the foundation for the new single sign-on protocolOpenID Connect, which is already in use and actively supportedby PayPal (“Log In with PayPal”), Google, and Microsoft, amongothers. Considering the broad industry support for OpenID Connect,a widespread adoption of OpenID Connect in the next years seemslikely. OpenID Connect builds upon OAuth and provides clearlydefined interfaces for user authentication and additional (optional)features, such as dynamic identity provider discovery and relyingparty registration, signing and encryption of messages, and logout.In OAuth, the interactions between the user and her browser,the RP, and the IdP can be performed in four different flows, orgrant types: authorization code grant, implicit grant, resource ownerpassword credentials grant, and the client credentials grant (we referto these as modes in the following). In addition, all of these modesprovide further options.The goal of this work is to provide an in-depth security analysisof OAuth. Analyzing the security of OAuth is a challenging task,on the one hand due to the various modes and options that OAuthprovides, and on the other hand due to the inherent complexity ofthe web.So far, most analysis efforts regarding the security of OAuth weretargeted towards finding errors in specific implementations [6, 10,25, 33, 34, 36, 38], rather than the comprehensive analysis of thestandard itself. Probably the most detailed formal analysis carriedout on OAuth so far is the one in . However, none of the existinganalysis efforts of OAuth account for all modes of OAuth runningsimultaneously, which may potentially introduce new security risks.In fact, many existing approaches analyze only the authorizationcode mode and the implicit mode of OAuth. Also, importantly,there are no analysis efforts that are based on a comprehensiveformal web model (see below), which, however, is essential to rule1Following the OAuth 2.0 terminology, IdPs are called authorization servers and resource servers, RPs are called clients, andusers are called resource owners. Here, however, we stick to themore common terms mentioned above.2Note that in this document, we consider only OAuth 2.0, whichis very different to its predecessor, OAuth 1.0(a).out security risks that arise when running the protocol in the contextof common web technologies (see Section 6 for a more detaileddiscussion of related work).
Structure of this Paper. In Section 2, we provide a detailed description of OAuth 2.0 using the authorization code mode as anexample. In Section 3, we present the attacks that we found duringour analysis. An overview of the FKS model we build upon in ouranalysis is provided in Section 4, with the formal analysis of OAuthpresented in Section 5. Related work is discussed in Section 6. Weconclude in Section 7. Full details, including how the attacks can beapplied to OpenID Connect, further details on our model of OAuth,and our security proof, can be found in our technical report .
2. OAUTH 2.0
In this section, we provide a description of the OAuth authorization code mode, with the other three modes explained only briefly.In our technical report , we provide a detailed description of theremaining three modes (grant types).OAuth was first intended for authorization, i.e., users authorizeRPs to access user data (called protected resources) at IdPs. Forexample, a user can use OAuth to authorize services such as IFTTT3to access her (private) timeline on Facebook. In this case, IFTTT isthe RP and Facebook the IdP.Roughly speaking, in the most common modes, OAuth worksas follows: If a user wants to authorize an RP to access some ofthe user’s data at an IdP, the RP redirects the user (i.e., the user’sbrowser) to the IdP, where the user authenticates and agrees to grantthe RP access to some of her user data at the IdP. Then, along withsome token (an authorization code or an access token) issued by theIdP, the user is redirected back to the RP. The RP can then use thetoken as a credential at the IdP to access the user’s data at the IdP.OAuth is also commonly used for authentication, although it wasnot designed with authentication in mind. A user can, for example,use her Facebook account, with Facebook being the IdP, to log in atthe social network Pinterest (the RP). Typically, in order to log in,the user authorizes the RP to access a unique user identifier at theIdP. The RP then retrieves this identifier and considers this user tobe logged in.3IFTTT (If This Then That) is a web service which can be usedto automate actions: IFTTT is triggered by user-defined events (e.g.,Twitter messages) and carries out user-defined tasks (e.g., postingon the user’s Facebook wall) Before an RP can interact with an IdP, the RP needs to be registered at the IdP. The details of the registration process are out of thescope of the OAuth protocol. In practice, this process is usually amanual task. During the registration process, the IdP assigns credentials to the RP: a public OAuth client id and (optionally) a clientsecret. (Recall that in the terminology of the OAuth standard theterm “client” stands for RP.) The RP may later use the client secret(if issued) to authenticate to the IdP.Also, an RP registers one or more redirection endpoint URIs(located at the RP) at an IdP. As we will see below, in some OAuthmodes, the IdP redirects the user’s browser to one of these URIs.Note that (depending on the implementation of an IdP) an RP mayalso register a pattern as a redirect URI and then specify the exactredirect URI during the OAuth run.In all modes, OAuth provides several options, such as those mentioned above. For brevity of presentation (and in contrast to ouranalysis), in the following descriptions, we consider only a specificset of options. For example, we assume that an RP always providesa redirect URI and shares an OAuth client secret with the IdP.
Authorization Code Mode. When the user tries to authorize anRP to access her data at an IdP or to log in at an RP, the RP firstredirects the user’s browser to the IdP. The user then authenticatesto the IdP, e.g., by providing her user name and password, andfinally is redirected back to the RP along with an authorizationcode generated by the IdP. The RP can now contact the IdP withthis authorization code (along with the client id and client secret)and receive an access token, which the RP in turn can use as acredential to access the user’s protected resources at the IdP.Step-by-Step Protocol Flow. In what follows, we describe the protocol flow of the authorization code mode step-by-step (see alsoFigure 1). First, the user starts the OAuth flow, e.g., by clickingon a button to select an IdP, resulting in request 1 being sent to theRP. The RP selects one of its redirection endpoint URIs redirect_uri(which will be used later in 7 ) and a value state (which will serve asa token to prevent CSRF attacks). The RP then redirects the browserto the so-called authorization endpoint URI at the IdP in 2 and 3with its client_id, redirect_uri, and state appended as parameters tothe URI. The IdP then prompts the user to provide her usernameand password in 4 . The user’s browser sends this information tothe IdP in 5 . If the credentials are correct, the IdP creates a noncecode (the authorization code) and redirects the user’s browser toRP’s redirection endpoint URI redirect_uri in 6 and 7 with codeand state appended as parameters to the URI. If state is the sameas above, the RP contacts the IdP in 8 and provides code, client_id,client_secret, and redirect_uri. Then the IdP checks whether thisinformation is correct, i.e., it checks that code was issued for the RPidentified by client_id, that client_secret is the secret for client_id,that redirect_uri coincides with the one in Step 2 , and that codehas not been redeemed before. If these checks are successful, theIdP issues an access token access_token in 9 . Now, the RP canuse access_token to access the user’s protected resources at the IdP(authorization) or log in the user (authentication), as described next.When OAuth is used for authorization, the RP uses the accesstoken to view or manipulate the protected resource at the IdP (illustrated in Steps 10 and 11 ).For authentication, the RP fetches a user id (which uniquelyidentifies the user at the IdP) using the access token, Steps 12 and 13 .The RP then issues a session cookie to the user’s browser as shownin 14 .4Tracking User Intention. Note that in order for an RP which supports multiple IdPs to process Step 7 , the RP must know whichIdP a user wanted to use for authorization. There are two differentapproaches to this used in practice: First, the RP can use differentredirection URIs to distinguish different IdPs. We call this naïveuser intention tracking. Second, the RP can store the user intentionin a session after Step 1 and use this information later. We call thisexplicit user intention tracking. The same applies to the implicitmode of OAuth presented below.
Resource Owner Password Credentials Mode. In this mode, theuser gives her credentials for an IdP directly to an RP. The RP canthen authenticate to the IdP on the user’s behalf and retrieve an access token. This mode is intended for highly-trusted RPs, such asthe operating system of the user’s device or highly-privileged applications, or if the previous two modes are not possible to perform(e.g., for applications without a web browser).
Client Credentials Mode. In contrast to the modes shown above,this mode works without the user’s interaction. Instead, it is startedby an RP in order to fetch an access token to access the resourcesof RP at an IdP. For example, Facebook allows RPs to use the clientcredentials mode to obtain an access token to access reports of theiradvertisements’ performance.
As mentioned in the introduction, while trying to prove the security of OAuth based on the FKS web model and our OAuth model,we found four attacks on OAuth, which we call 307 redirect attack,IdP mix-up attack, state leak attack, and naïve RP session integrityattack, respectively. In this section, we provide detailed descriptionsof these attacks along with easily implementable fixes. Our formalanalysis of OAuth (see Section 5) then shows that these fixes areindeed sufficient to establish the security of OAuth. The attacks alsoapply to OpenID Connect (see Section 3.5). Figure 2 provides anoverview of where the attacks apply. We have verified our attackson actual implementations of OAuth and OpenID Connect and reported the attacks to the respective working groups who confirmedthe attacks (see Section 3.6).
3.1 307 Redirect Attack
In this attack, which breaks our authorization and authenticationproperties (see Section 5.2), the attacker (running a malicious RP)learns the user’s credentials when the user logs in at an IdP that usesthe wrong HTTP redirection status code. While the attack itself isbased on a simple error, to the best of our knowledge, this is thefirst description of an attack of this kind.
Assumptions. The main assumptions are that (1) the IdP that isused for the login chooses the 307 HTTP status code when redirecting the user’s browser back to the RP (Step 6 in Figure 1), and(2) the IdP redirects the user immediately after the user entered hercredentials (i.e., in the response to the HTTP POST request thatcontains the form data sent by the user’s browser).Assumption (1). This assumption is reasonable because neither theOAuth standard  nor the OAuth security considerations (nor the OpenID Connect standard ) specify the exact methodof how to redirect. The OAuth standard rather explicitly permitsany HTTP redirect:While the examples in this specification show the useof the HTTP 302 status code, any other method available via the user-agent to accomplish this redirectionis allowed and is considered to be an implementationdetail.5The response from the IdP in Step 13 includes the RP’s OAuthclient id, which is checked by the RP when authenticating a user(cf. RFC7662 ). This check prevents re-use of access tokensacross RPs in the OAuth implicit mode, as explained in . Thischeck is not needed for authorization.Assumption (2). This assumption is reasonable as many examplesfor redirects immediately after entering the user credentials canbe found in practice, for example at github.com (where, however,assumption (1) is not satisfied.)
Attack. When a user uses the authorization code or implicit modeof OAuth to log in at a malicious RP, then she is redirected to theIdP and prompted to enter her credentials. The IdP then receivesthese credentials from the user’s browser in a POST request. Itchecks the credentials and redirects the user’s browser to the RP’sredirection endpoint in the response to the POST request. Sincethe 307 status code is used for this redirection, the user’s browserwill send a POST request to RP that contains all form data from theprevious request, including the user credentials. Since the RP is runby the attacker, he can use these credentials to impersonate the user.Fix. Contrary to the current wording in the OAuth standard, theexact method of the redirect is not an implementation detail butessential for the security of OAuth. In the HTTP standard ,only the 303 redirect is defined unambiguously to drop the bodyof an HTTP POST request. Therefore, the OAuth standard shouldrequire 303 redirects for the steps mentioned above in order to fixthis problem.
3.2 IdP Mix-Up Attack
In this attack, which breaks our authorization and authentication properties (see Section 5.2), the attacker confuses an RP aboutwhich IdP the user chose at the beginning of the login/authorizationprocess in order to acquire an authentication code or access tokenwhich can be used to impersonate the user or access user data.This attack applies to the authorization code mode and the implicit mode of OAuth when explicit user intention tracking6 is usedby the RP. To launch the attack, the attacker manipulates the firstrequest of the user such that the RP thinks that the user wants to usean identity managed by an IdP of the attacker (AIdP) while the userinstead wishes to use her identity managed by an honest IdP (HIdP).As a result, the RP sends the authorization code or the access tokenissued by HIdP to the attacker. The attacker then can use this information to login at the RP under the user’s identity (managed byHIdP) or access the user’s protected resources at HIdP.We here present the attack in the authorization code mode. Inthe implicit mode, the attack is very similar and is shown in detailin .
Assumptions. For the IdP mix-up attack to work, we need threeassumptions that we further discuss below: (1) the presence of anetwork attacker who can manipulate the request in which the usersends her identity to the RP as well as the corresponding responseto this request (see Steps 1 and 2 in Figure 1), (2) an RP whichallows users to log in with identities provided by (some) HIdP andidentities provided by AIdP, and (3) an RP that uses explicit userintention tracking and issues the same redirection URI to all IdPs.7We emphasize that we do not assume that the user sends any secret(such as passwords) over an unencrypted channel.Assumption (1). It would be unrealistic to assume that a networkattacker can never manipulate Steps 1 and 2 in Figure 1.First, these messages are sent between the user and the RP, i.e.,the attacker does not need to intercept server-to-server communication. He could, e.g., use ARP spoofing in a wifi network to mountthe attack.6Recall the meaning of “user intention tracking” from Section 2.7Alternatively, the attack would work if the RP issues differentredirection URIs to different IdPs, but treats them as the same URI. Second, the need for HTTPS for these steps is not obvious tousers or RPs, and the use of HTTPS is not suggested by the OAuthsecurity recommendations, since the user only selects an IdP at thispoint; credentials are not transferred.Third, even if an RP intends to use HTTPS also for the first request (as in our model), it has to protect itself against TLS strippingby adding the RP domain to a browser preloaded Strict TransportSecurity (STS) list . Other mitigations, such as the STS header,can be circumvented (see ), and do not work on the very firstconnection between the user’s browser and RP. For example, whena user enters the address of an RP into her browser, browsers bydefault try unencrypted connections. It is therefore unrealistic toassume that all RPs are always protected against TLS stripping.Our formal analysis presented in Section 5 shows that OAuth canbe operated securely even if no HTTPS is used for the initial request(given that our fix, presented below, is applied).Assumption (2). RPs may use different IdPs, some of which mightbe malicious, and hence, OAuth should provide security in thiscase. Using a technique called dynamic client registration, OAuthRPs can even allow the ad-hoc use of any IdP, including maliciousones. This is particularly relevant in OpenID Connect, where thistechnique was first implemented.Assumption (3). Typically, RPs that use explicit user intention tracking do not register different redirection URIs for different IdPs, asin this case the RP records the IdP a user wants to authenticatewith. In particular, for RPs that allow for dynamic registration, using the same URI is an obvious implementation choice. This is forexample the case in the OAuth/OpenID Connect implementationsmod_auth_openidc and pyoidc (see below).
Attack on Authorization Code Mode.
We now describe the IdPMix-Up attack on the OAuth authorization code mode. As mentioned, a very similar attack also applies to the implicit mode. Bothattacks also work if IdP supports just one of these two modes.The IdP mix-up attack for the authorization code mode is depicted in Figure 3. Just as in a regular flow, the attack starts whenthe user selects that she wants to log in using HIdP (Step 1 in Figure 3). Now, the attacker intercepts the request intended for theRP and modifies the content of this request by replacing HIdP byAIdP.8 The response of the RP 3 (containing a redirect to AIdP)is then again intercepted and modified by the attacker such that itredirects the user to HIdP 4 . The attacker also replaces the OAuthclient id of the RP at AIdP with the client id of the RP at HIdP(which is public information). (Note that we assume that from thispoint on, in accordance with the OAuth security recommendations,the communication between the user’s browser and HIdP and theRP is encrypted by using HTTPS, and thus, cannot be inspected oraltered by the attacker.) The user then authenticates to HIdP and isredirected back to the RP 8 . The RP thinks, due to Step 2 of theattack, that the nonce code contained in this redirect was issued byAIdP, rather than HIdP. The RP therefore now tries to redeem thisnonce for an access token at AIdP 10 , rather than HIdP. This leakscode to the attacker.Breaking Authorization. If HIdP has not issued an OAuth clientsecret to RP during registration, the attacker can now redeem codefor an access token at HIdP (in 11 and 12 ).9 This access tokenallows the attacker to access protected resources of the user at HIdP.This breaks the authorization property (see Section 5.2). We notethat at this point, the attacker might even provide false information8At this point, the attacker could also read the session id forthe user’s session at RP. Our attack, however, is not based on thispossibility and works even if the RP changes this session id as soonas the user is logged in and the connection is protected by HTTPS(a best practice for session management).9In the case that RP has to provide a client secret, this wouldnot work in this mode (see also Figure 2). Recall that in this mode,client secrets are optional.about the user or her protected resources to the RP: he could issuea self-created access token which RP would then use to access suchinformation at the attacker.Breaking Authentication. To break the authentication property (seeSection 5.2) and impersonate the honest user, the attacker, afterobtaining code in Step 10 , starts a new login process (using his ownbrowser) at the RP. He selects HIdP as the IdP for this login processand receives a redirect to HIdP, which he ignores. This redirectcontains a cookie for a new login session and a fresh state parameter.The attacker now sends code to the RP imitating a real login (usingthe cookie and fresh state value from the previous response). TheRP then retrieves an access token at HIdP using code and uses thisaccess token to fetch the (honest) user’s id. Being convinced thatthe attacker owns the honest user’s account, the RP issues a sessioncookie for this account to the attacker. As a result, the attackeris logged in at the RP under the honest user’s id. (Note that theattacker does not learn an access token in this case.)
Variant. There is also a variant of the IdP mix-up attack that onlyrequires a web attacker (which does not intercept and manipulatenetwork messages). In this variant, the user wants to log in withAIdP, but is redirected by AIdP to log in at HIdP; a fact a vigilantuser might detect.In detail, the first four steps in Figure 3 are replaced by the following steps: First, the user starts a new OAuth flow with RP usingAIdP. She is then redirected by RP to AIdP’s authorization endpoint. Now, instead of prompting the user for her password, AIdPredirects the user to HIdP’s authorization endpoint. (Note that, asabove, in this step, the attacker uses the state value he received fromthe browser plus the client id of RP at HIdP.) From here on, theattack proceeds exactly as in Step 5 in Figure 3.
Related Attacks. An attack in the same class, cross social-networkrequest forgery, was outlined by Bansal, Bhargavan, Delignat-Lavaud, and Maffeis in . It applies to RPs with naïve user intentiontracking (rather than explicit user intention tracking assumed in ourIdP mix-up attack above) in combination with IdPs, such as Facebook, that only loosely check the redirect URI.10 Our IdP mix-upattack works even if an IdP strictly checks redirect URIs. While theattack in  is described in the context of concrete social networkimplementations, our findings show that this class of attacks is notmerely an implementation error, but a more general problem in theOAuth standard. This was confirmed by the IETF OAuth Working Group, who, as mentioned, are in the process of amending theOAuth standard according to our fixes (see Section 3.6).Another attack with a similar outcome, called Malicious Endpoints Attack, leveraging the OpenID Connect Discovery mechanism and therefore limited to OpenID Connect, was describedin . This attack assumes a CSRF vulnerability on the RP’s side.Fix. A fundamental problem in the authorization code and implicitmodes of the OAuth standard is a lack of reliable information inthe redirect in Steps 6 and 7 in Figure 1 (even if HTTPS is used).The RP does not receive information from where the redirect wasinitiated (when explicit user intention tracking is used) or receivesinformation that can easily be spoofed (when naïve user intentiontracking is used with IdPs such as Facebook). Hence, the RP cannotcheck whether the information contained in the redirect stems fromthe IdP that was indicated in Step 1 .Our fix therefore is to include the identity of the IdP in the redirect URI in some form that cannot be influenced by the attacker, e.g.,using a new URI parameter. Each IdP should add such a parameter10Facebook, by default, only checks the origin of redirect URIs.to the redirect URI.11 The RP can then check that the parametercontains the identity of the IdP it expects to receive the responsefrom. (This could be used with either naïve or explicit user intention tracking, but to mitigate the naïve RP session integrity attackdescribed below, we advise to use explicit user intention trackingonly, see below.)We show in Section 5 that this fix is indeed sufficient to mitigatethe IdP mix-up attack (as well as the attacks pointed out in [6, 27]).
3.3 State Leak Attack
Using the state leak attack, an attacker can force a browser tobe logged in under the attacker’s name at an RP or force an RP touse a resource of the attacker instead of a resource of the user. Thisattack, which breaks our session integrity property (see Section 5.2),enables what is often called session swapping or login CSRF .
Attack. After the user has authenticated to the IdP in the authorization code mode, the user is redirected to RP (Step 7 in Figure 1).This request contains state and code as parameters. The responseto this request (Step 14 ) can be a page containing a link to the attacker’s website or some resource located at the attacker’s website.When the user clicks the link or the resource is loaded, the user’sbrowser sends a request to the attacker. This request contains a Referer header with the full URI of the page the user was redirected to,which in this case contains state and code.As the state value is supposed to protect the browser’s sessionagainst CSRF attacks, the attacker can now use the leaked statevalue to perform a CSRF attack against the victim. For example, hecan redirect the victim’s browser to the RP’s redirection endpoint(again) and by this, overwrite the previously performed authorization. The user will then be logged in as the attacker.Given the history of OAuth, leaks of sensitive data through thereferrer header are not surprising. For example, the fact that the authorization code can leak through the Referer header was describedas an attack (in a similar setting) in . Since the authorizationcode is single-use only , it might already be redeemed by thetime it is received by the attacker. State, however, is not limited tosingle use, making this attack easier to exploit in practice. Stealingthe state value through the Referer header to break session integrityhas not been reported as an attack before, as was confirmed by theIETF OAuth Working Group.
State Leak at IdPs. A variant of this attack exists if the login pageat an IdP contains links to external resources. If the user visitsthis page to authenticate at the IdP and the browser follows linksto external resources, the state is transferred in the Referer header.This variant is applicable to the authorization code mode and theimplicit mode.Fix. We suggest to limit state to a single use and to use the recentlyintroduced referrer policies  to avoid leakage of the state (orcode) to the attacker. Using referrer policies, a web server caninstruct a web browser to (partially or completely) suppress theReferer header when the browser follows links in or loads resourcesfor some web page. The Referer header can be blocked entirely, orit can, for example, be stripped down to the origin of the URI of theweb page. Referrer policies are supported by all modern browsers.Our OAuth model includes this fix (such that only the origin ispermitted in the Referer header for links on web pages of RPs/IdPs)and our security proof shows its effectiveness (see Section 5). The11The OAuth Working Group indeed created a draft for anRFC  that includes this fix, where this parameter is called iss(issuer).fix also protects the authorization code from leaking as in the attackdescribed in .
3.4 Naïve RP Session Integrity Attack
This attack again breaks the session integrity property for RPs,where here we assume an RP that uses naïve user intention tracking.12 (Note that we may still assume that the OAuth state parameteris used, i.e., RP is not necessarily stateless.)
Attack. First, an attacker starts a session with HIdP (an honestIdP) to obtain an authorization code or access token for his ownaccount. Next, when a user wants to log in at some RP using AIdP(an IdP controlled by the attacker), AIdP redirects the user back tothe redirection URI of HIdP at RP. AIdP attaches to this redirectionURI the state issued by RP, and the code or token obtained fromHIdP. Now, since RP performs naïve user intention tracking only,the RP then believes that the user logged in at HIdP. Hence, theuser is logged in at RP using the attacker’s identity at HIdP or theRP accesses the attacker’s resources at HIdP believing that theseresources are owned by the user.Fix. The fix against the IdP mix-up attack (described above) doesnot work in this case: Since RP does not track where the user wantedto log in, it has to rely on parameters in the redirection URI whichthe attacker can easily spoof. Instead, we propose to always useexplicit user intention tracking.
3.5 Implications to OpenID Connect
OpenID Connect  is a standard for authentication built on topof the OAuth protocol. Among others, OpenID Connect is used byPayPal, Google, and Microsoft.All four attacks can be applied to OpenID Connect as well. Wehere outline OpenID Connect and how the attacks apply to thisprotocol. A detailed description can be found in .OpenID Connect extends OAuth in several ways, e.g., by additional security measures. OpenID Connect defines an authorizationcode mode, an implicit mode, and a hybrid mode. The former twoare based on the corresponding OAuth modes and the latter is acombination of the two modes.307 Redirect, State Leak, Naïve RP Session Integrity Attacks. Allthree attacks apply to OpenID Connect in exactly the same way asdescribed above. The vulnerable steps are identical.IdP Mix-Up Attack. In OpenID Connect, the mix-up attack appliesto the authorization code mode and the hybrid mode. In the authorization code mode, the attack is very similar to the one on theOAuth authorization code mode. In the hybrid mode, the attack ismore complicated as additional security measures have to be circumvented by the attacker. In particular, it must be ensured that theRP does not detect that the issuer of the id token, a signed cryptographic document used in OpenID Connect, is not the honest IdP.Interestingly, in the hybrid mode, depending on an implementationdetail of the RP, either authorization or authentication is broken (orboth if no client secret is used).
3.6 Verification and Disclosure
We verified the IdP mix-up and 307 redirect attacks on the Apacheweb server module mod_auth_openidc, an implementation of anOpenID Connect (and therefore also OAuth) RP. We also verifiedthe IdP mix-up attack on the python implementation pyoidc. We ver-12Recall the meaning of “naïve user intention tracking” fromSection 2.ified the state leak attack on the current version of the Facebook PHPSDK and the naïve RP session integrity attack on nytimes.com.13We reported all attacks to the OAuth and OpenID Connect working groups who confirmed the attacks. The OAuth working groupinvited us to present our findings to them and prepared a draft for anRFC that mitigates the IdP mix-up attack (using the fix describedin Section 3.2) . Fixes regarding the other attacks are currentlyunder discussion. We also notified nytimes.com, Facebook, and thedevelopers of mod_auth_openidc and pyoidc.
4. FKS MODEL
We now present our security analysis of OAuth (with the fixesmentioned in Section 3 applied). We first present our model ofOAuth. We then formalize the security properties and state themain theorem, namely the security of OAuth w.r.t. these properties.We provide full details of the model and our proof in the technicalreport .
As mentioned above, our model for OAuth is based on the FKSmodel outlined in Section 4. For the analysis, we extended themodel to include HTTP Basic Authentication  and ReferrerPolicies  (the Referer header itself was already part of themodel). We developed the OAuth model to adhere to RFC6749,the OAuth 2.0 standard, and follow the security considerations described in .Design. Our comprehensive model of OAuth includes all configuration options of OAuth and makes as few assumptions as possiblein order to strengthen our security results:OAuth Modes. Every RP and IdP may run any of the four OAuthmodes, even simultaneously.Corruption. RPs, IdPs, and browsers can be corrupted by the attacker at any time.Redirection URIs. RP chooses redirection URIs explicitly or theIdP selects a redirection URI that was registered before. Redirection URIs can contain patterns. This covers all cases specified inthe OAuth standard. We allow that IdPs do not strictly check theredirection URIs, and instead apply loose checking, i.e., only theorigin is checked (this is the default for Facebook, for example).This only strengthens the security guarantees we prove.Client Secrets. Just as in the OAuth standard, RPs can, for a certainIdP, have a secret or not have a secret in our model.Usage of HTTP and HTTPS. Users may visit HTTP and HTTPSURIs (e.g., for RPs) and parties are not required to use StrictTransport-Security (STS), although we still recommend STS inpractice (for example, to reduce the risk of password eavesdropping). Again, this only strengthens our results.General User Interaction. As usual in the FKS model, the user canat any time navigate backwards or forward in her browser history,navigate to any web page, open multiple windows, start simultaneous login flows using different or the same IdPs, etc. Web pages atRPs can contain regular links to arbitrary external web sites.Authentication at IdP. User authentication at the IdP, which is outof the scope of OAuth, is performed using username and password.Session Mechanism at RP. OAuth does not prescribe a specific session mechanism to be used at an RP. Our model therefore includesa standard cookie-based session mechanism (as suggested in ).
Concepts Used in Our Model. In our model and the security properties, we use the following concepts:Protected Resources. Closely following RFC6749 , OAuth protected resources are an abstract concept for any resource an RPcould use at an IdP after successful authorization. For example, ifFacebook gives access to the friends list of a user to an RP, thiswould be considered a protected resource. In our model, there is amapping from (IdP, RP, identity) to nonces (which model protectedresources). In this mapping, the identity part can be ?, modeling aresource that is acquired in the client credentials mode and thus notbound to a user.Service Tokens. When OAuth is used for authentication, we assume that after successful login, the RP sends a service token to thebrowser. The intuition is that with this service token a user can usethe services of the RP. The service token consists of a nonce, theuser’s identifier, and the domain of the IdP which was used in thelogin process. The service token is a generic model for any sessionmechanism the RP could use to track the user’s login status (e.g.,a cookie). We note that the actual session mechanism used by theRP after a successful login is out of the scope of OAuth, which iswhy we use the generic concept of a service token. In our model,the service token is delivered by an RP to a browser as a cookie.Trusted RPs. In our model, among others, a browser can choose tolaunch the resource owner password credentials mode with any RP,causing this RP to know the password of the user. RPs, however,can become corrupted and thus leak the password to the attacker.Therefore, to define the security properties, we define the conceptof trusted RPs. Intuitively, this is a set of RPs a user entrusts withher password. In particular, whether an RP is trusted depends onthe user. In our security properties, when we state that an adversaryshould not be able to impersonate a user u in a run, we wouldassume that all trusted RPs of u have not become corrupted in thisrun.
OAuth Web System with a Network Attacker. We model OAuthas a class of web systems (in the sense of Section 4) that can containan unbounded finite number of RPs, IdPs, and browsers. We call aweb system OWSn an OAuth web system with a network attacker ifit is of the form described in what follows.Outline. The system consists of a network attacker, a finite set ofweb browsers, a finite set of web servers for the RPs, and a finiteset of web servers for the IdPs. Recall that in OWSn, since we havea network attacker, we do not need to consider web attackers (asour network attacker subsumes all web attackers). The set of scriptsconsists of the three scripts script_rp_index, script_rp_implicit, andscript_idp_form. We now briefly sketch RPs, IdPs, and the scripts,with full details provided in our technical report .Relying Parties. Each RP is a web server modeled as an atomic DYprocess following the description in Section 2, including all OAuthmodes, as well as the fixes and mitigations discussed before. TheRP can either (at any time) launch a client credentials mode flow orwait for users to start any of the other flows. RP manages two kindsof sessions: The login sessions, which are used only during the userlogin phase, and the service sessions (modeled by a service tokenas described above). When receiving a special message, an RP canbecome corrupted and then behaves like an attacker process.Identity Providers. Each IdP is a web server modeled as an atomicDY process following the description in Section 2, again includingall OAuth modes, as well as the fixes and mitigations discussedbefore. Users can authenticate to an IdP with their credentials. Justas RPs, IdPs can become corrupted at any time.Scripts. The scripts which run in a user’s browser are defined asfollows: The script script_rp_index is loaded from an RP into auser’s browser when the user visits the RP’s web site. It startsthe authorization or login process. The script script_rp_implicit isloaded into the user’s browser from an RP during an implicit modeflow to retrieve the data from the URI fragment. It extracts theaccess token and state from the fragment part of its own URI. Thescript then sends this information in the body of an HTTPS POSTrequest to the RP. The script script_idp_form is loaded from an IdPinto the user’s browser for user authentication at the IdP.
OAuth Web System with Web Attackers. In addition to OWSn,we also consider a class of web systems where the network attackeris replaced by an unbounded finite set of web attackers. We denotesuch a system by OWSw and call it an OAuth web system with webattackers, Such web systems are used to analyze session integrity,see below.
Limitations of Our OAuth Model. While our model of OAuth isvery comprehensive, a few aspects of OAuth were not taken intoconsideration in our analysis:We do not model expiration of access tokens and session ids.Also, IdPs may issue so-called refresh tokens in Step 9 of Figure 1.In practice, an RP may use such a (long-living) refresh token toobtain a new (short-lived) access token. In our model, we overapproximate this by not expiring access tokens. We also do not modelrevocation of access tokens and user log out.OAuth IdPs support controlling the scope of resources made available to an RP. For example, a Facebook user can grant a third partythe right to read her user profile but deny access to her friends list.The scope is a property of the access token, but handled internallyby the IdP with its implementation, details, and semantics highlydependent on the IdP. We therefore model that RPs always get fullaccess to the user’s data at the IdP.In practice, IdPs can send error messages (mostly static strings)to RPs. We do not model these.Limitations of the underlying FKS model are discussed in .
5.2 Security Properties
Based on the formal OAuth model described above, we now formulate central security properties of OAuth, namely authorization,authentication, and session integrity (see our technical report for the full formal definitions).
Authorization. Intuitively, authorization for OWSn means that anattacker should not be able to obtain or use a protected resourceavailable to some honest RP at an IdP for some user unless, roughlyspeaking, the user’s browser or the IdP is corrupted.More formally, we say that OWSn is secure w.r.t. authorization ifthe following holds true: if at any point in a run of OWSn an attackercan obtain a protected resource available to some honest RP r at anIdP i for some user u, then the IdP i is corrupt or, if u 6= ?, we havethat the browser of u or at least one of the trusted RPs of u must becorrupted. Recall that if u = ?, then the resource was acquired inthe client credentials mode, and hence, is not bound to a user.
Authentication. Intuitively, authentication for OWSn means thatan attacker should not be able to login at an (honest) RP under theidentity of a user unless, roughly speaking, the IdP involved or theuser’s browser is corrupted. As explained above, being logged in atan RP under some user identity means to have obtained a servicetoken for this identity from the RP.More formally, we say that OWSn is secure w.r.t. authenticationif the following holds true: if at any point in a run of OWSn anattacker can obtain the service token that was issued by an honestRP using some IdP i for a user u, then the IdP i, the browser of u, orat least one of the trusted RPs of u must be corrupted.
Main Theorem. We prove the following theorem (see  for theproof):Theorem 1. Let OWSn be an OAuth web system with a network attacker, then OWSn is secure w.r.t. authorization and secure w.r.t. authentication. Let OWSw be an OAuth web system with web attackers, then OWSw is secure w.r.t. session integrity for authorizationand authentication.Note that this trivially implies that authentication and authorization properties are satisfied also if web attackers are considered.
5.3 Discussion of Results
6. RELATED WORK
We focus on work closely related to OAuth 2.0 or formal securityanalysis of web standards and web applications.The work closest to our work is the already mentioned work byBansal, Bhargavan, Delignat-Lavaud, and Maffeis . Bansal etal. analyze the security of OAuth using the applied pi-calculus andthe WebSpi library, along with the protocol analysis tool ProVerif.They model various settings of OAuth 2.0, often assuming the presence of common web implementation flaws resulting in, for example, CSRF and open redirectors in RPs and IdPs. They identifypreviously unknown attacks on the OAuth implementations of Facebook, Yahoo, Twitter, and many other websites. Compared to ourwork, the WebSpi model used in  is less expressive and comprehensive (see also the discussion in ), and the models of OAuththey employ are more limited.16 As pointed out by Bansal et al.,the main focus of their work is to discover attacks on OAuth, ratherthan proving security. They have some positive results, which, however, are based on their more limited model. In addition, in orderto prove these results further restrictions are assumed, e.g., theyconsider only one IdP per RP and all IdPs are assumed to be honest.Wang et al.  present a systematic approach to find implicit assumptions in SDKs (e.g., the Facebook PHP SDK) used for authentication and authorization, including SDKs that implement OAuth 2.0.In , Pai et al. analyze the security of OAuth in a very limitedmodel that does not incorporate generic web features. They showthat using their approach, based on the Alloy finite-state modelchecker, known weaknesses can be found. The same tool is usedby Kumar  in a formal analysis of the older OAuth 1.0 protocol(which, as mentioned, is very different to OAuth 2.0).Chari, Jutla, and Roy  analyze the security of the authorizationcode mode in the universally composability model, again withoutconsidering web features, such as semantics of HTTP status codes,details of cookies, or window structures inside a browser.Besides these formal approaches, empirical studies were conducted on deployed OAuth implementations. In , Sun andBeznosov analyze the security of three IdPs and 96 RPs. In ,Li and Mitchell study the security of 10 IdPs and 60 RPs basedin China. In , Yang et al. perform an automated analysis of 4OAuth IdPs and 500 RPs. Shernan et al.  evaluate the lack ofCSRF protection in various OAuth deployments. In [10,33], practical evaluations on the security of OAuth implementations of mobileapps are performed.16For example, only two OAuth modes are considered, the modelis monotonic (e.g., cookies can only be added, but not deleted ormodified), fixed bounded number of cookies per request, no precisehandling of windows, documents, and iframes, no web messaging,omission of headers, such as origin. We note that while OAuth doesnot make use of all web features, taking such features into accountis important to make positive security results more meaningful.In , Mladenov et al. perform an informal analysis of OpenIDConnect. They present several attacks related to discovery and dynamic client registration, which are extensions of OpenID Connect;see also the discussion in Section 3.2 (related attacks) concerningtheir malicious endpoint attack.Note that many of the works listed here led to improved security recommendations for OAuth as listed in RFC6749  andRFC6819 . These are already taken into account in our modeland analysis of OAuth.More generally, there have been only very few analysis effortsfor web applications and standards based on formal web models sofar. Work outside of the context of OAuth includes [2–5,14–16,23].
In this paper, we carried out the first extensive formal analysis of OAuth 2.0 based on a comprehensive and expressive webmodel. Our analysis, which aimed at the standard itself, rather thanspecific OAuth implementations and deployments, comprises allmodes (grant types) of OAuth and available options and also takesmalicious RPs and IdPs as well as corrupted browsers/users intoaccount. The generic web model underlying our model of OAuthand its analysis is the most comprehensive web model to date.Our in-depth analysis revealed four attacks on OAuth as well asOpenID connect, which builds on OAuth. We verified the attacks,proposed fixes, and reported the attacks and our fixes to the working groups for OAuth and OpenID Connect. The working groupsconfirmed the attacks. Fixes to the standard and recommendationsare currently under discussion or already incorporated in a draft fora new RFC .With the fixes applied, we were able to prove strong authorization,authentication, and session integrity properties for OAuth 2.0. Oursecurity analysis assumes that OAuth security recommendationsand certain best practices are followed. We show that otherwise thesecurity of OAuth cannot be guaranteed. By this, we also provideclear guidelines for implementations. The fact that OAuth is one ofthe most widely deployed authorization and authentication systemsin the web and the basis for other protocols makes our analysisparticularly relevant.As for future work, our formal analysis of OAuth offers a goodstarting point for the formal analysis of OpenID Connect, and hence,such an analysis is an obvious next step for our research.
This work was partially supported by Deutsche Forschungsgemeinschaft (DFG) through Grant KU 1434/10-1.
 M. Abadi and C. Fournet. Mobile Values, New Names, andSecure Communication. In POPL 2001, pages 104–115.ACM Press, 2001. D. Akhawe, A. Barth, P. E. Lam, J. Mitchell, and D. Song.Towards a Formal Foundation of Web Security. In CSF 2010,pages 290–304. IEEE Computer Society, 2010. A. Armando, R. Carbone, L. Compagna, J. Cuéllar,G. Pellegrino, and A. Sorniotti. An authentication flaw inbrowser-based Single Sign-On protocols: Impact andremediations. Computers & Security, 33:41–58, 2013.Elsevier, 2013. A. Armando, R. Carbone, L. Compagna, J. Cuéllar, and M. L.Tobarra. Formal Analysis of SAML 2.0 Web Browser SingleSign-on: Breaking the SAML-based Single Sign-on forGoogle Apps. In FMSE 2008, pages 1–10. ACM, 2008. C. Bansal, K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis.Keys to the Cloud: Formal Analysis and Concrete Attacks onEncrypted Web Storage. In POST 2013, volume 7796 ofLNCS, pages 126–146. Springer, 2013. C. Bansal, K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis.Discovering Concrete Attacks on Website Authorization byFormal Analysis. Journal of Computer Security,22(4):601–657, 2014. IOS Press, 2014. A. Barth, C. Jackson, and J. C. Mitchell. Robust defenses forcross-site request forgery. In CCS 2008, pages 75–88. ACM,2008. J. Bradley, T. Lodderstedt, and H. Zandbelt. Encoding claimsin the OAuth 2 state parameter using a JWT –draft-bradley-oauth-jwt-encoded-state-05. IETF. Dec. 2015.https://tools.ietf.org/html/draft-bradley-oauth-jwt-encoded-state-05. S. Chari, C. S. Jutla, and A. Roy. Universally ComposableSecurity Analysis of OAuth v2.0. IACR Cryptology ePrintArchive, 2011:526, 2011. E. Y. Chen, Y. Pei, S. Chen, Y. Tian, R. Kotcher, and P. Tague.OAuth Demystified for Mobile Application Developers. InCCS 2014, pages 892–903, 2014. Chromium Project. HSTS Preload Submission.https://hstspreload.appspot.com/. Cross-Origin Resource Sharing - W3C Recommendation 16January 2014.http://www.w3.org/TR/2014/REC-cors-20140116/. J. Eisinger and E. Stark. Referrer Policy – Editor’s Draft, 28March 2016. W3C. Mar. 2016.https://w3c.github.io/webappsec-referrer-policy/. D. Fett, R. Küsters, and G. Schmitz. An Expressive Model forthe Web Infrastructure: Definition and Application to theBrowserID SSO System. In S&P 2014, pages 673–688. IEEEComputer Society, 2014. D. Fett, R. Küsters, and G. Schmitz. Analyzing theBrowserID SSO System with Primary Identity ProvidersUsing an Expressive Model of the Web. In ESORICS 2015,volume 9326 of LNCS, pages 43–65. Springer, 2015. D. Fett, R. Küsters, and G. Schmitz. SPRESSO: A Secure,Privacy-Respecting Single Sign-On System for the Web. InCCS 2015, pages 1358–1369. ACM, 2015. D. Fett, R. Küsters, and G. Schmitz. A ComprehensiveFormal Security Analysis of OAuth 2.0. Technical ReportarXiv:1601.01229, arXiv, 2016. Available athttp://arxiv.org/abs/1601.01229. R. Fielding (ed.) and J. Reschke (ed.). RFC7231 – HypertextTransfer Protocol (HTTP/1.1): Semantics and Content. IETF.Jun. 2014. https://tools.ietf.org/html/rfc7231. J. Franks, P. Hallam-Baker, J. Hostetler, S. Lawrence,P. Leach, A. Luotonen, and L. Stewart. RFC2617 – HTTPAuthentication: Basic and Digest Access Authentication.IETF. Jun. 1999. https://tools.ietf.org/html/rfc2617. D. Hardt (ed.). RFC6749 – The OAuth 2.0 AuthorizationFramework. IETF. Oct. 2012.https://tools.ietf.org/html/rfc6749. E. Homakov. How I hacked Github again, 7 February 2014.http://homakov.blogspot.de/2014/02/how-i-hacked-github-again.html. M. Jones, J. Bradley, and N. Sakimura. OAuth 2.0 Mix-UpMitigation – draft-ietf-oauth-mix-up-mitigation-01. IETF. Jul.2016. https://tools.ietf.org/html/draft-ietf-oauth-mix-up-mitigation-01. F. Kerschbaum. Simple Cross-Site Attack Prevention. InSecureComm 2007, pages 464–472. IEEE Computer Society,2007. A. Kumar. Using automated model analysis for reasoningabout security of web protocols. In ACSAC 2012. ACM,2012. W. Li and C. J. Mitchell. Security issues in OAuth 2.0 SSOimplementations. In ISC 2014, volume 8783 of LNCS, pages529–541, 2014. Springer, 2014. T. Lodderstedt (ed.), M. McGloin, and P. Hunt. RFC6819 –OAuth 2.0 Threat Model and Security Considerations. IETF.Jan. 2013. https://tools.ietf.org/html/rfc6819. V. Mladenov, C. Mainka, J. Krautwald, F. Feldmann, andJ. Schwenk. On the security of modern Single Sign-OnProtocols: Second-Order Vulnerabilities in OpenID Connect.CoRR, abs/1508.04324v2, 2016. Open Web Application Security Project (OWASP). Sessionfixation. https://www.owasp.org/index.php/Session_Fixation. S. Pai, Y. Sharma, S. Kumar, R. M. Pai, and S. Singh. FormalVerification of OAuth 2.0 Using Alloy Framework. In CSNT2011, pages 655–659. IEEE, 2011. J. Richer (ed.). RFC7662 – OAuth 2.0 Token Introspection.IETF. Oct. 2015. https://tools.ietf.org/html/rfc7662. N. Sakimura, J. Bradley, M. Jones, B. de Medeiros, andC. Mortimore. OpenID Connect Core 1.0 incorporating errataset 1. OpenID Foundation. Nov. 8, 2014.http://openid.net/specs/openid-connect-core-1_0.html. J. Selvi. Bypassing HTTP Strict Transport Security. InBlackhat (Europe) 2014, 2014. M. Shehab and F. Mohsen. Towards Enhancing the Securityof OAuth Implementations in Smart Phones. In IEEE MS2014. IEEE, 2014. E. Shernan, H. Carter, D. Tian, P. Traynor, and K. R. B.Butler. More Guidelines Than Rules: CSRF Vulnerabilitiesfrom Noncompliant OAuth 2.0 Implementations. In DIMVA2015, volume 9148 of LNCS, pages 239–260. Springer, 2015. SimilarTech. Facebook Connect Market Share and WebUsage Statistics. Last visited Nov. 7, 2015. https://www.similartech.com/technologies/facebook-connect. S.-T. Sun and K. Beznosov. The Devil is in the(Implementation) Details: An Empirical Analysis of OAuthSSO Systems. In CCS 2012, pages 378–390. ACM, 2012. R. Wang, Y. Zhou, S. Chen, S. Qadeer, D. Evans, andY. Gurevich. Explicating SDKs: Uncovering AssumptionsUnderlying Secure Authentication and Authorization. InUSENIX Security 2013, pages 399–314. USENIXAssociation, 2013. R. Yang, G. Li, W. C. Lau, K. Zhang, and P. Hu. Model-basedSecurity Testing: An Empirical Study on OAuth 2.0Implementations. In AsiaCCS 2016, pages 651–662. ACM,2016. X. Zheng, J. Jiang, J. Liang, H. Duan, S. Chen, T. Wan, andN. Weaver. Cookies Lack Integrity: Real-World Implications.In USENIX Security 2015), pages 707–721, 2015. USENIXAssociation, 2015.