Chetan Bansal

Karthikeyan Bhargavan

Antoine Delignat-Lavaud

Sergio Maffeis

Discovering Concrete Attacks on Website Authorization by Formal Analysis

Keywords: single sign-on, OAuth, web protocol, cross-site request forgery, ProVerif, WebSpi authentification unique, OAuth, protocole internet, cross-site request forgery, ProVerif, WebSpi function | '{' ( @identifier ':' expression ', ')* '}'

Social sign-on and social sharing are becoming an ever more popular feature of web applications. This success is largely due to the APIs and support offered by prominent social networks, such as Facebook, Twitter, and Google, on the basis of new open standards such as the OAuth 2.0 authorization protocol. A formal analysis of these protocols must account for malicious websites and common web application vulnerabilities, such as cross-site request forgery and open redirectors. We model several configurations of the OAuth 2.0 protocol in the applied picalculus and verify them using ProVerif. Our models rely on WebSpi, a new library for modeling web applications and web-based attackers that is designed to help discover concrete attacks on websites. Our approach is validated by finding dozens of previously unknown vulnerabilities in popular websites such as Yahoo and WordPress, when they connect to social networks such as Twitter and Facebook.

Introduction

A growing number of websites now seek to use social networks to personalize each user's browsing experience. For example, using the social sign-on, social sharing, and social integration APIs provided by Facebook, a website can read and write social data about its visitors, without requiring them to establish a dedicated personal profile. Access to these APIs is mediated by an authorization protocol that ensures that only websites that a user has explicitly authorized may access her social data.

Web authorization protocols. After years of ad hoc authentication and authorization mechanisms for web APIs, a series of standards have emerged. SAML [START_REF] Cantor | Assertions and protocols for the oasis security assertion markup language[END_REF] and other XML-based security protocols are primarily used for SOAP-based API access, for example, on Amazon and Microsoft Azure. OpenID [START_REF] Recordon | OpenID 2 . 0 : A Platform for User-Centric Identity Management[END_REF] is used for light-weight user authentication, for example, on Google and PayPal. OAuth [START_REF] Hammer-Lahav | The OAuth 1.0 Protocol[END_REF][START_REF] Hardt | The OAuth 2.0 Authorization Framework[END_REF] is used for REST-based API access to social APIs, for example, on Twitter and Facebook.

It is no longer uncommon to see websites supporting a variety of login options using different social networks. A consensus seems to be emerging around the use of some variation or combination of the OpenID and OAuth protocols, and OAuth 2.0 [START_REF] Hardt | The OAuth 2.0 Authorization Framework[END_REF] is currently the most widely supported protocol for API authorization, especially for REST, AJAX, and JSON-based websites. It is currently supported by Google, Facebook, Microsoft, and LinkedIn among others. OpenID Connect [START_REF][END_REF] is a proposal to build the next version of OpenID on top of OAuth 2.0, hence unifying API-based authentication and authorization in a single framework.

The main novelty of OpenID and OAuth over traditional authentication and authorization protocols is that they do not require custom software: they are designed to be embedded in standard websites and executed by standard web browsers. All protocol messages are encoded as HTTP requests and responses and the protocol is mediated by the user's browser, so that the user may authorize or deny access to her data through a familiar interface. A typical implementation consists of server-side PHP or Python scripts running on each website and a client-side HTML and JavaScript component that communicates with these servers to execute the protocol.

Formal analysis against web attacks The security of web authorization protocols relies both on the design of the websites that deploy them and on browser-based mechanisms like cookies and JavaScript. Hence, in addition to the traditional network attacker who may hijack insecure HTTP connections, such protocols are also exposed to a new class of web attackers who may exploit website vulnerabilities such as Cross-Site Scripting (XSS), Cross-Site Request Forgery (CSRF), and open redirectors (OR) to partially compromise the client or server scripts running these protocols. Such web vulnerabilities are widely prevalent even on popular websites and have proved hard to eliminate [START_REF]OWASP Top Ten Project[END_REF]. Evaluating the robustness of new security mechanisms such as web authorization against web attackers requires a precise model of browsers, servers, and interactions between them.

Inria

Previous works on the formal analysis of single sign-on protocols [START_REF] Pfitzmann | Analysis of liberty single-sign-on with enabled clients[END_REF][START_REF] Pfitzmann | Federated identity-management protocols[END_REF][START_REF] Hansen | Using static analysis to validate the saml single sign-on protocol[END_REF][START_REF] Bhargavan | Verified implementations of the information card federated identity-management protocol[END_REF][START_REF] Armando | Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps[END_REF], account for network attackers (e.g. as formalized by Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF]) but do not model web attacks at the level of cookies and JavaScript. Web authorization protocols have also been subject to careful human analysis [START_REF] Lodderstedt | OAuth 2.0 Threat Model and Security Considerations[END_REF][START_REF] Corella | Security Analysis of Double Redirection Protocols[END_REF], which can detect some potential vulnerabilities. However, most practical vulnerabilities depend on specific deployment configurations that are too difficult to analyze systematically by hand. Automatic tools such as Alloy [START_REF] Jackson | Alloy: A logical modelling language[END_REF], AVISPA [START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF] and ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF] have proved to be effective in the formal analysis of security protocols and to find network-based attacks. Can they also be used to automatically analyze web security mechanisms and find concrete web attacks?

Akhawe et al. [START_REF] Akhawe | Towards a formal foundation of web security[END_REF] use Alloy to develop a general model of web components and use a SAT solver to find vulnerabilities in new security mechanisms including a Kerberos-based single signon solution. In this paper, inspired by [START_REF] Akhawe | Towards a formal foundation of web security[END_REF], we define an automated framework to find web authorization vulnerabilities in a systematic way. We show how a protocol designer can extract models for various compositions of web security mechanisms and verify them against different attacker models, until she reaches a design that satisfies her specific security goals.

Our approach. We model various configurations of the OAuth 2.0 protocol in the applied picalculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF][START_REF] Abadi | Private authentication[END_REF] and analyze them using ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF]. Our models rely on a generic library, WebSpi, that defines the basic components (users, browsers, HTTP servers) needed to model web applications and their security policies. In order to express realistic security goals for a web application, we show how to encode distributed authorization policies in the style of [START_REF] Detreville | Binder, a logic-based security language[END_REF][START_REF] Fournet | A type discipline for authorization policies[END_REF][START_REF] Fournet | A type discipline for authorization in distributed systems[END_REF] in ProVerif. The library also defines an operational web attacker model so that attacks discovered by ProVerif can be mapped to concrete website actions closely corresponding to the actual PHP implementation of an exploit. The model developer can fine-tune the analysis by enabling and disabling different classes of attacks. The effectiveness of our approach is testified by the discovery of several previously unknown vulnerabilities involving some of the most popular web sites, including Facebook, Yahoo, and Twitter. We reported these problems and helped fixing them.

We present a model extraction tool that generates applied pi-calculus models from website components written using carefully-chosen subsets of PHP and JavaScript. Model extraction frees the web security analyst from the more mundane (but error-prone) activity of encoding protocols in ProVerif syntax, allowing her to focus on the results of the analysis instead. As an example, we demonstrate an implementation of OAuth's user-agent flow that can be analyzed by our toolset; attacks found by ProVerif can then be mapped back to concrete attacks on our implementation. We advocate the use of our automated analysis framework when designing and prototyping the security-critical core of a new application. Once verified, this core can be easily extended into a complete website.

Contributions. The main contributions of this paper are the WebSpi library (Section 4), a formal analysis of OAuth 2.0 using WebSpi and ProVerif (Section 5), a description of new concrete website attacks found and confirmed by our formal analysis, and a model extraction tool for PHP websites (Section 6). A shorter version of this paper was published in CSF 2012 [START_REF] Bansal | Discovering concrete attacks on website authorization by formal analysis[END_REF]; a new technical contribution in this paper is the model extraction framework of Section 6. Full ProVerif scripts, including the WebSpi library, the OAuth 2.0 model, and formal attacks, are available online [START_REF] Bansal | WebSpi and web application models[END_REF].

Social Sign-On and Social Sharing

Social sign-on (or social login) is the use of a social network to login to a third-party website, without having to register at the website. It is a service provided by many social networks and authentication servers, using protocols such as OpenID (e.g. Google) and OAuth (e.g. Facebook). For clarity, we henceforth adopt OAuth terminology: a user who owns some data is called a resource owner, a website that holds user data and offers API access to it is called a resource server, and a third party that wishes to access this data is called a client or an app.

Motivating Example: Authenticated Website Comments

Consider WordPress.com, a website that hosts hundreds of thousands of active blogs with millions of visitors every day. A visitor may comment on a blog post only after authenticating herself as a WordPress, Facebook, or Twitter user (Figure 1-L).

When a visitor Alice clicks on "Log in with Facebook", an authorization protocol is set into motion where Alice is the resource owner, Facebook the resource server, and WordPress the client. Alice's browser is redirected to Facebook.com which pops up a window asking to allow WordPress.com to access her Facebook profile (Figure 1-R). WordPress.com would like access to Alice's basic information, in particular her name and email address, as proof of identity.

If Alice authorizes this access, she is sent back to WordPress.com with an API access token that lets WordPress.com read her email address from Facebook and log her in, completing the social sign-on protocol. All subsequent actions that Alice performs at WordPress.com, such as commenting on a blog, are associated with her Facebook identity. Some client websites also implement social sharing: reading and writing data on the resource owner's social network. For example, on CitySearch.com, a guide with restaurant and hotel recommendations, any review or comment written by a logged-in Facebook user is instantly cross-posted on her profile feed ('Wall') and shared with all her friends. Some websites go even further: Yahoo.com acts as both client and resource server to provide deep social integration where the user's social information flows both ways, and may be used to enhance her experience on a variety of online services, such as web search and email.

Security goals

Let us first consider the informal security goals of the social sign-on interaction described above, from the viewpoint of Alice, WordPress and Facebook.

Alice wants to ensure that her comments will appear under her own name; nobody else can publish comments in her name; no unauthorized website should gain access to her name Inria and email address; even authorized websites should only have access to the information she decided to share.

WordPress wants to ensure that the user trying to log in and post comments as Alice, is indeed Alice.

Facebook wants to ensure that both the resource owner and client are who they say they are, and that it only releases data when authorized by the resource owner.

These security goals are fairly standard for three-party authentication and authorization frameworks, and in order to achieve them the protocol relies on two secrets: Alice's password at Facebook and the access token issued by Facebook to WordPress.

What makes social sign-on more interesting than traditional authentication protocols is the need to enforce these goals under normal web conditions. For example, Alice may use the same browser to log-in on WordPress and, in another tab, visit an untrusted website, possibly over an insecure Wi-Fi network. In such a scenario, threats to Alice's security goals include: network attackers who can intercept and inject clear-text HTTP messages between Alice and WordPress; malicious users who can try to fool Facebook or WordPress by pretending to be Alice; and malicious websites who can try to fool Facebook or Alice by pretending to be WordPress. A web attacker may use any combination of these three attack vectors.

Web-based attacks

Network attacks are well understood, and can be mitigated by the systematic use of HTTPS [START_REF] Rescorla | HTTP Over TLS[END_REF], or more sophisticated cryptographic mechanisms. Many websites, such as Facebook (at the time of writing), do not even seek to protect against network attackers for normal browsing, allowing users to access their data over HTTP. They are more concerned about website-and browserbased attacks, such as Cross-Site Scripting (XSS), SQL Injection, Cross-Site Request Forgery (CSRF) and Open Redirectors [START_REF]OWASP Top Ten Project[END_REF].

For example, various flavors of CSRF are common on the web. When a user logs into a website, the server typically generates a fresh, unguessable, session identifier and returns it to the browser as a cookie. All subsequent requests from the browser to the website include this cookie, so that the website associates the new request with the logged-in session. However, if the website relies only on this cookie to authorize security-sensitive operations on behalf of the user, it is vulnerable to CSRF. A malicious website may fool the user's browser into sending a (cross-site) request to the vulnerable website (by using JavaScript, HTTP redirect, or by inviting the user to click on a link). The browser will then automatically forward the user's session cookie with this forged request, implicitly authorizing it without the knowledge of the user, and potentially compromising her security. A special case is called login CSRF : when a website's login form itself has a CSRF vulnerability, a malicious website can fool a user's browser into silently logging in to the website under the attacker's credentials, so that future user actions are credited to the attacker's account. A typical countermeasure for CSRF is to require every security-sensitive request to include a session-specific nonce that would be difficult for a malicious website to forge. This nonce can be embedded in the target URL or within a hidden form field. However, such mechanisms are still not widely deployed and CSRF attacks remain prevalent on the web, even on respected websites.

Social CSRF attacks

We now describe one of the new attacks we found in our formal analysis of OAuth in Section 5. This example shows how a CSRF attack on low-value client website (CitySearch.com) can be translated into an attack on its high-value resource server (Facebook.com).

Suppose Alice clicks on the social login form on CitySearch to log in with her Facebook account. So, CitySearch obtains an API access token for Alice's Facebook profile. If Alice then wants to review a restaurant on CitySearch, she is presented with a form that also asks her if she would like her review to be posted on Facebook (Figure 2-L).

When she submits this form, the review is posted to CitySearch as a standard HTTP POST request (Figure 2-R); CitySearch subsequently reposts it on Alice's Facebook profile (after attaching its API access token) on the server side.

We found that the review form above is susceptible to a standard CSRF attack; the contents of the POST request do not contain any nonce, except for the cookie, which is automatically attached by the browser. So, if Alice were to go to an untrusted website while logged into CitySearch, that website could post a review in Alice's name on CitySearch (and hence, also on Alice's Facebook profile.)

Moreover, CitySearch's social login form is also susceptible to an automatic login CSRF attack. So, if Alice has previously used social login on CitySearch, any website that Alice visits could submit this form to silently log in Alice on CitySearch via Facebook. Alice is not asked for permission since Facebook typically only asks a user for authorization the first time she logs into a new client.

Combining the two attacks, we built a demonstrative malicious website that, when visited by a user who has previously used Facebook login on CitySearch, can automatically log her into CitySearch and post arbitrary reviews in her name both on CitySearch and Facebook. This is neither a regular CSRF attack on Facebook nor a login CSRF attack on CitySearch (since the user signs in under her own name). Instead, the attacker uses CitySearch as a proxy to mount an indirect CSRF attack on Facebook, treating the API access token like a session cookie. We call this class of attacks Social CSRF.

Attack amplification

To understand the novelty of Social CSRF attacks, it is instructive to compare Alice's security before and after she used social sign-on on CitySearch. Before, Alice's reviews were subject to a CSRF attack, but only if she visited a malicious site at the same time as when she was logged into CitySearch. No website could log Alice automatically into CitySearch since it would require Alice's password. Moreover, no website would have been able to post a message on Alice's Facebook wall without her permission, because Facebook implements strong CSRF protections.

Inria

But now, even if Alice uses social login once on CitySearch and never visits the site again, a website attacker will always be able to modify both Alice's Facebook wall and her CitySearch reviews.

Empirically, we find that social CSRF attacks are widespread, probably because websites have been encouraged to hastily integrate social login and social sharing without due consideration of their security implications. Social CSRFs pose a serious threat both to resource servers and clients, because these attacks can be amplified both ways. On one hand, as we have seen, a CSRF vulnerability in any Facebook client becomes a CSRF on Facebook. On the other hand, a login CSRF attack that we discovered on twitter.com (see Section 4), becomes a login CSRF vulnerability on all of its client websites.

Towards a Systematic Discovery of Web-Based Attacks

The CitySearch vulnerability described above composes two different CSRF attacks, involves three websites and a browser, and consists of at least nine HTTP(S) connections. It does not depend on the details of the underlying authorization protocol, but the other vulnerabilities in Section 5 rely on specific weaknesses in OAuth 2.0 configurations. We found such attacks by a systematic formal analysis, and we believe at least some would have escaped a human protocol review.

Modeling web-based attackers offers new challenges compared to the attackers traditionally considered in formal cryptographic protocol analysis. For example, in a model that enables the attacker to control the network, websites such as CitySearch and Facebook are trivially insecure as most user data is sent over insecure HTTP. With such strong attacker models, we are unlikely to discover subtle web attacks such as CSRF. Conversely, a model that treats the browser and the user as one entity will miss CSRF attacks completely, since they rely on the browser performing actions not intended by the user. In Section 4, we present a web security library that includes a precise model of the browser as well as an attacker model that can be fine-tuned, enabling the discovery of new and interesting web attacks.

OAuth 2.0: Browser-based API Authorization

The goal of the OAuth 2.0 protocol [START_REF] Hardt | The OAuth 2.0 Authorization Framework[END_REF] is to enable third party clients to obtain limited access, on behalf of a resource owner, to the API of a resource server. The protocol involves five parties: a resource server that allows access to its resources over the web on receiving an access token issued by a trusted authorization server ; a resource owner who owns data on the resource server, has login credentials at the authorization server, and uses a user-agent (browser) to access the web; a client website, that needs to access data at the resource server, and whose application credentials are registered at the authorization server. In the example of Section 2, Facebook is both the authorization server and resource server; we find that this is the most common configuration.

The first version of OAuth [START_REF] Hammer-Lahav | The OAuth 1.0 Protocol[END_REF] was designed to unify previous authorization mechanisms implemented by Twitter, Flickr, and Google. However, it was criticized as being website-centric, inflexible, and too complex. In particular, the cryptographic mechanisms used to protect authorization requests and responses were deemed too difficult for website developers to implement (correctly).

OAuth 2.0 is designed to address these shortcomings. The protocol specification defines several different flows or protocol configurations, two of which directly apply to website applications. The protocol itself requires no cryptographic mechanisms whatsoever and instead relies on transport layer security (HTTPS). Hence, it claims to be lightweight and flexible, and has fast emerged as the API authorization protocol of choice, supported by Microsoft, Google and Facebook, among others. We next describe the two website flows of OAuth 2.0, their security goals, and their typical implementations.

User-Agent Flow

The User-Agent flow, also called Implicit Grant flow, is meant to be used by client applications that can run JavaScript on the resource owner's user-agent. For example, it may be used by regular websites or by browser plugins. The authorization flow, adapted from the specification, is depicted in Figure 3.

Let the resource server be located at the URL RS and its authorization server be located at AS. Let the resource owner RO have a username u and password p at AS. Let the client be located at URL C and have an application identifier id at AS. The message flow and relevant security events of the user-agent flow are as follows:

1. Login(RO,b,sid,AS,u): RO using browser b starts a login session sid at AS using credentials u,p.

2. SocialLogin(RO,b,sid',C,AS,RS): RO using b starts a social sign-on session sid' at C using AS for RS.

3. TokenRequest(C,b,AS,id,perms): C redirects b to AS requesting a token for id with access rights perms.

4. Authorize(RO,b,sid,C,perms): AS looks up id and asks RO for authorization; RO using browser b in session sid at AS authorizes C with perms.

5.

TokenResponse(AS,b,C,token): AS redirects b back to C with an access token. These steps may be followed by any number of API calls from the client to the resource server, on behalf of the resource owner. Each step in this flow consists of (at least) one HTTP requestresponse exchange. The specification requires that the AS must and the C should implement these exchanges over HTTPS. In the rest of this paper, we assume that all OAuth exchanges occur over HTTPS unless specified otherwise.

As an example of the user-agent protocol flow, consider the social sign-on interaction between websites like Pinterest and Facebook; the TokenRequest(C,b,AS,id,perms) step is typically implemented as an HTTPS redirect from Pinterest to a URI of the form: https://www.facebook.com/ dialog/permissions.request?app_id=id&perms=email. The TokenResponse is also an HTTPS redirect back to Pinterest, of the form: https://pinterest.com/#access_token=token. Note that the access token is passed as a fragment URI. JavaScript running on behalf of the client can extract the token and then pass it to the client when necessary. In practice, these HTTP exchanges are implemented by a JavaScript SDK provided by Facebook and embedded into Pinterest, hence messages may have additional Facebook-specific parameters, but generally follow this pattern.

Authorization Code Flow

The Authorization Code flow (Figure 4), also called Explicit Grant flow or Web Server flow, can be used by client websites wishing to implement a deeper social integration with the resource server by using server-side API calls. It requires that the client must have a security association with the authorization server, using for example a shared secret. Moreover, it requires that the access token be retrieved on the server-side by the client. The motivation for this is two-fold: (i) it allows the authorization server to authenticate the client's token request using a secret that only the client and the server know. In contrast, the authorization server in the user-agent flow has no way to ensure that the client in fact wanted a token to be issued, it simply sends a token to the client's HTTPS endpoint; (ii) it prevents the access token from passing through the browser, and hence ensures that only the client application may access the resource server directly. In contrast, the access token in the user-agent flow may be leaked in the Referer header, browser history, or by malicious third-party JavaScript running on the client.

The authorization flow is depicted in Figure 3. Let the client at URL C have both an application identifier id and a secret sec pre-registered at AS. The difference between the web server and user-agent flows begins after the SocialLogin step, and ends before the APIRequest step: 3. CodeRequest(C,b,AS,id,perms): C redirects b to AS requesting authorization for id with perms.

4. Authorize(RO,b,sid,C,perms): AS looks up id and asks RO for authorization; RO using browser b in session sid at AS authorizes C with perms.

5.

CodeResponse(AS,b,C,code): AS redirects b back to C with an authorization code.

5.1) APITokenRequest(C,AS,code,id,sec): C makes an API request for an access token to AS with code, id, and sec.

5.2)

APITokenResponse(AS,C,token): AS checks id and sec, verifies the code and returns a token to C.

Additional Protocol Parameters

In addition to the basic protocol flows outlined above, OAuth 2.0 enables several other optional features. Our models capture the following:

Redirection URI. Whenever a client sends a message to the authorization server, it may optionally provide a redirect uri parameter, where it wants the response to be sent. In particular, the TokenRequest and CodeRequest messages above may include this parameter, and if they do, then the corresponding APITokenRequest must also include it. The client may thus ask for the authorization server to redirect the browser to the same page (or state) from which the authorization request was issued. Since the security of OAuth crucially depends on the URI where codes and tokens are sent, the specification strongly advises that clients must register all their potential redirection URIs beforehand at the authorization server. If not, it predicts attacks where a malicious website may be able to acquire codes or tokens and break the security of the protocol. Indeed, our analysis found such attacks both in our model and in real websites. We call such attacks Token Redirection attacks.

State Parameter. After the TokenRequest or CodeRequest steps above, the client waits for the authorization server to send a response. The client has no way of authenticating this response, so a malicious website can fool the resource owner into sending the client a different authorization code or access token (belonging to a different user). This is a variation of the standard website login CSRF attack that we call a Social Login CSRF attack. To prevent this attack, the OAuth specification recommends that clients generate a nonce that is strongly bound to the resource owner's session at the client (say, by hashing a cookie). It should then pass this nonce as an additional state parameter in the CodeRequest or TokenRequest messages. The authorization server simply returns this parameter in its response, and by checking that the two match, the client can verify that the returned token or code is meant for the current session. After incorporating the above parameters, the following protocol steps are modified as shown:

TokenRequest(C,b,AS,id,perms,state,redirect uri) TokenResponse(AS,b,redirect uri,state,token) CodeRequest(C,b,AS,id,perms,state,redirect uri) CodeResponse(AS,b,redirect uri,state,code) APITokenRequest(C,AS,code,id,sec,redirect uri) APITokenResponse(AS,C,token)

Our analysis does not cover other features of OAuth, such as refresh tokens, token and code expiry, the right use of permissions, or the other protocol flows described in the specification. We leave these features for future work. The OAuth specification [START_REF] Hardt | The OAuth 2.0 Authorization Framework[END_REF] and a companion document describing its threat model [START_REF] Lodderstedt | OAuth 2.0 Threat Model and Security Considerations[END_REF] together provide an exhaustive list of potential threats to the protocol. We consider a subset of these threats in our formal analysis.

The ultimate aim of the attackers we consider is to steal or modify the private information of an honest resource owner, for example by fooling honest or buggy clients, authorization servers, or resource owners into divulging this information. To this end, we consider: network based attackers who can sniff, intercept, and inject messages into insecure HTTP traffic; malicious clients, resource owners, and authorization servers; malicious websites that honest resource owners may browse to; and honest clients with specific web vulnerabilities, such as CSRF attacks, or redirectors that may forward HTTP requests to malicious websites.

We do not explicitly consider attacks on the browser or operating system of honest participants; instead, we treat such participants as compromised, that is, as fully controlled by an attacker. We assume that honest resource owners choose strong passwords and use secure web browsers. We assume that honest authorization servers have no web vulnerabilities, instead we focus on vulnerabilities in client websites.

Security Goals for OAuth 2.0

We describe the security goals for each participant by defining Datalog-like authorization policies [START_REF] Detreville | Binder, a logic-based security language[END_REF] that must be satisfied at different stages of the protocol. The policy A : B,C is read as "A if B and C".

The resource owner RO (using browser b) in a session sid' with a client C has successfully completed the social sign-on with authorization server AS (and resource server RS) if it intended to sign into the client, if it agreed to authorize the client, and if the client and resource owner agree upon the user's social identity (u) for the current session (sid'): The authorization server must ensure that a token is issued only to authorized clients. Its policy for the user-agent flow says that a TokenResponse can only be sent to C if the resource owner has logged in and authorized the client.

TokenResponse(AS,b,C,state,token) :

ValidToken(token,AS,u,perms), Says(RO,Login(RO,b,sid,AS,u)), ValidClient(C,id,redirect uri), Says(RO,Authorize(RO,b,sid,C,perms)).

Note that we do not require a TokenResponse to be only issued in response to a TokenRequest from the client: at this stage, the user-agent flow has not authenticated the client, and so cannot know whether the client intended to request a token.

The correponding policy for the authorization code flow is stronger:

APITokenResponse(AS,C,state,token) :

ValidToken(token,AS,u,perms), Says(RO,Login(RO,b,sid,AS,u)),

ValidClient(C,id,redirect uri), Says(C,TokenRequest(C,b,AS,id,perms,state,redirect uri)), Says(RO,Authorize(RO,b,sid,C,perms)).

From the viewpoint of the resource server, every API call must be issued by an authorized client and accompanied by a token issued by the authorization server.

APIResponse(RS,b,C,token,req,resp) :

ValidToken(token,AS,u,perms), Permitted(perms,req), Says(C,APIRequest(C,RS,token,req)).

Finally, from the viewpoint of the client, the social sign-on has completed successfully if it has correctly identified the resource owner currently visiting its page, and obtained an access token for the API accesses it requires.

SocialLoginAccept(C,sid',u,AS,RS) :

Says(RO,SocialLogin(RO,b,sid',C,AS,RS)), Says(AS,TokenResponse(AS,b,C,token)), Says(RS,APIResponse(RS,C,token,getId(),u)).

The WebSpi library and its usage

Various calculi, starting from the spi-calculus [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF], have been remarkably successful as modeling languages for cryptographic protocols, thanks also to the emergence of automated verification tools that can analyze large protocol models. Following in this tradition, we model web security mechanisms in an applied pi-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF][START_REF] Abadi | Private authentication[END_REF], and verify them using ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF]. We identify a set of idioms that are particularly useful in modeling web applications and web-based attackers, and offer them as a library, called WebSpi, available to other developers of web models.

ProVerif

The ProVerif specification language is a variant of the applied pi-calculus, an operational model of communicating concurrent processes with a flexible sublanguage for describing data structures and functional computation. Below, we summarize the ProVerif specification language and its verification methodology, to the extent used in this paper. We refer the reader to [START_REF] Blanchet | ProVerif: Automatic Cryptographic Protocol Verier, User Manual and Tutorial[END_REF][START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF] for further details on ProVerif.

Messages

Basic types are channels, bitstrings or user-defined. Atomic messages, typically ranged over by a,b,c,h,k,... are tokens of basic types. Messages can be composed by pairing (M,N) or by applying n-ary data constructors and destructors f(M1,...,Mn). Constructors and destructors are particularly useful for cryptography, as described below. Pattern matching is extensively used to parse messages. Messages may be sent on private or public channels or stored in tables. ProVerif constructors are collision-free (one-one) functions and are only reversible if equipped with a corresponding destructor. Hence, MACs and hashes are modeled as irreversible constructors, and asymmetric cryptography is modeled using public and private keys: These and other standard cryptographic operations are part of the ProVerif library. Users can define other primitives when necessary. Such primitives can be used for example to build detailed models of protocols like TLS [START_REF] Bhargavan | Verified cryptographic implementations for tls[END_REF].

Protocol Processes

The syntax of ProVerif's specification language, given below, is mostly standard compared to other process algebra. Messages may be sent and received on channels, or stored and retrieved from tables (which themselves are internally encoded by private channels). Fresh messages (such as nonces) are generated using new. Pattern matching is used to parse messages in let, but also when receiving messages from channels or tables. Predicates p(M) are invoked in conditionals (boolean conditions M=N are a special case). Finally, processes can be run in parallel, and even replicated. The command event e(M1,...,Mn) inserts an event e(M1,...,Mn) in the trace of the process being executed. Such events form the basis of the verification model of ProVerif. A script in fact contains processes and queries of the form

∀M 1 , ...M k . e(M 1 , ...M k ) ⇒ φ
The tool tries to prove that whenever the event e is reachable, the formula φ is true (φ can contain conjunctions or disjunctions).

A common case is that of correspondence assertions [START_REF] Woo | A semantic model for authentication protocols[END_REF], where an event e is split into two sub-events begin e and end e . The goal is to show that if end e is reachable then begin e must have been reached beforehand. The corresponding ProVerif query is query M1:T1,...,Mn:Tn; End(e,M1,...Mn) =⇒Begin(e,M1,...,Mn).

Correspondence queries naturally encode authentication goals, as noted in Section 4.1.5. Syntactic secrecy goals are encoded as reachability queries on the attacker's knowledge.

Distributed security policies

Since their introduction in the context of the spi-calculus [START_REF] Fournet | A type discipline for authorization policies[END_REF], Datalog-like security policies have proven to be an ideal tool to describe enforceable authorization and authentication policies for distributed security protocols. A program statement such as Assume(UserSends(u,m)) adds to a global knowledge base the fact that user u has sent message m. Such a statement should precede the actual code used by the user to send the message, and its purpose it to reflect the operation in the policy world. A program statement such as Expect(ServerAuthorizes(s,u,d)) instead means that at this point in the code, we must be able to prove that the server s is willing to authorize user u to retrieve data d. The main idea is that the Expect triggers a query on the security policy, using the facts known (and assumed) so far. In this paper, we adopt a similar style to express our policies and bind them to protocol code. Using ProVerif's native support for predicates defined by Horn clauses, we embed the assumption of fact e by the code if Assume(e) then P, where Assume is declared as a blocking predicate, so that ProVerif treats Assume(e) as an atomic fact and adds it as a hypothesis in its proof derivations about P. Conversely, the expectation that e holds is written as event Expect(e). Security policies are defined as Horn clauses extending a predicate fact. In particular, the WebSpi library includes the generic clause forall e:Fact; Assume(e) →fact(e) that admits assumed facts, and a generic security query forall e:Fact; event(Expect(e)) =⇒fact(e) that requires every expected predicate to be provable from the policy and previously assumed facts.

Moreover, inspired by Binder [START_REF] Detreville | Binder, a logic-based security language[END_REF][START_REF] Abadi | Towards a declarative language and system for secure networking[END_REF], we encode the standard Says modality axiomatized below: The two rules state that if a fact is true, it can be assumed to be said by any principal, and that if a principal is known to be compromised, denoted by the fact Compromised(p), then it cannot be trusted anymore and is ready to say anything.

Distributed authorization policies have already been used for typed-based verification of protocols in the applied pi-calculus [START_REF] Fournet | A type discipline for authorization in distributed systems[END_REF]. To the best of our knowledge, we are the first to embed them on top of ProVerif predicates, thus driving the verification of realistic case studies.

Inria

Verification

ProVerif translates applied-pi processes into Horn clauses in order to perform automatic verification. The main soundness theorem in [START_REF] Blanchet | Automatic verification of correspondences for security protocols[END_REF] guarantees that if ProVerif says that a query is true for a given script, then it is in fact the case that the query is true on all traces of the applied-pi processes defined in the script in parallel with any other arbitrary attacker processes. If a query is false, ProVerif produces a proof derivation that shows how an attacker may be able to trigger an event that violates the query. In some cases, ProVerif can even extract a step-by-step attack trace.

General cryptographic protocol verification is undecidable, hence ProVerif does not always terminate. ProVerif uses conservative abstractions that let it analyze protocol instances for an unbounded number of participants, sessions, and attackers, but may report false positives. Hence, one needs to validate proof derivations and formal attack traces before accepting them as counterexamples on a model.

WebSpi

WebSpi models consist of users who surf the Internet on web browsers, in order to interact with web applications that are hosted by web servers. A user can use multiple browsers, and a server can host multiple web applications. Figure 5 gives a schematic representation of the model.

Principals, HTTP Protocol, Browsers, and Servers

The agents in our model are called principals. They can play the role of users or owners of web applications. Hence, the same principal may own two different web applications and be the user of a third one. Users hold credentials to authenticate with respect to a specific web application (identified by a host domain and subdomain) in the table credentials. Web applications hold private and public keys to implement TLS secure connections in the table serverIdentities. table credentials(Host,Principal,Id,Credentials). table serverIdentities(Host,Principal,pubkey,privkey,XdrFlag).

These tables are private to the model and represent a pre-existing distribution of secrets (passwords and keys). They are populated by the process CredentialFactory that provides an API for the attacker (explained later) to create an arbitrary population of principals, and compromise some of them.

Browsers and servers communicate using the HTTP(S) protocol over a channel net. Our model of HTTP(S) messages is fairly detailed. For example, the message httpReq(uri(protocol,domainHost(subdomain,domain),path,params), headers(referrer,cookies,notajax()), httpGet())

denotes a regular (non-AJAX) HTTP GET request with cookies. Cookies can be associated to the root "" of a domain or to a specific path, and support HttpOnly and Secure attributes. The standardized, application-independent behavior of browsers and servers, which includes TLS connection and cookie handling, is modeled by the processes HttpClient and HttpServer. These processes incorporate a simple model of anonymous HTTP(S) connections: each request to an HTTPS URI is encrypted with a fresh symmetric key, that is in turn encrypted under the server's public key. The response is encrypted with the same symmetric key.

HTTP Server. The process HttpServer simply handles the TLS connections on behalf of a web application (Section 4.2.2), and is reported below. The HTTP(S) server accepts requests over channel net, from browser b, on behalf of the web application hosted from the destination origin o. If TLS is used, it decodes the message m to obtain the session key k and the actual request httpReq(u,hs,req). If the connection was plain HTTP, reqdec becomes the identity function on m.

Next, the server forwards the request to the corresponding web application on channel httpServerRequest, waiting for a response to encrypt (if necessary) and forward on the net back to b. Since the server may act on behalf of several applications, the token corr is used to correlate the right request/response pairs between the HTTP server process and the various web application processes. Server-side sessions, are maintained by individual web applications and are not visible at this stage.

HTTP Client. The process HttpClient is the core of the WebSpi library. It represent the behavior of a specific browser b, handling raw network requests and TLS encryption, offering to user processes an API for surfing the web, and modeling page origins and persistent state (cookies and local storage).

The browser API sends messages to the local channel internalRequest to a sub-process which handles network messages and TLS in a complementary fashion to the HTTP server process. This module also handles cookies, AJAX and cross-domain requests. The code below shows the final stages of handling an HTTP response. An OK response originated by clicking on a link, submitting a form, or editing the address bar to URI u, leads to the creation of a new page p1, a corresponding update in the page origin table, and a message on the newPage channel of browser b which corresponds to loading the HTML payload dataIn in the new page. An OK response originated by an AJAX call to the same origin oldorig, or to a server accepting cross-domain requests (flag xdr()) instead leaves the old page in place and creates a message on the ajaxResponse channel of b that makes the AJAX payload dataIn available to the page. A Redirection response, which is not allowed for an AJAX request, is handled by issuing a fresh request on the internalRequest channel.

(let httpOk(dataIn) = resp in

The browser API includes commands browserRequest modelling a navigation request originating from the address bar or bookmarks (with an empty Referer header), pageClick modelling a navigation request or form submission from within a page (either caused by the user or by JavaScript), ajaxRequest to initiate an XMLHttpRequest and setCookieStorage to update the non-HttpOnly cookies from JavaScript.

Nondeterministically, the browser may reset the cookies and local storage for a given origin (modeling the user clearing the cookie cache) or release cookies/storage associated to a given origin to any page loaded from the same origin. 1 The second case is modeled by the code below. Cookies are indexed by origin and by path (where slash() stands for the empty path).

Predefined processes. For convenience, the WebSpi library contains a number of predefined processes that implement useful patterns of behaviour on the web. To cite some representative examples, the HttpRedirector process provides a simple, predefined redirection service. The process WebSurfer models a generic user principal who is willing to browse the web to any public URL. Process UntrustedApp implements a simple web application that can be compromised by the attacker, and is useful to test the robustness of a protocol with respect to compromise of third parties.

Modeling web applications using WebSpi

To model a web application using WebSpi, one typically writes three processes: 1 In the case of cookies, we give access also to pages loaded from a sub-origin (we check for =originhost(o)), since a page from sub.example.com can upcast its origin to example.com, and read the corresponding cookies.

RR n°8287

a server-side (PHP-like) process representing the website, which interfaces with HttpServer to handle network communications; a client-side (JavaScript-like) process representing the web page, which interfaces with the browsing API exposed by HttpClient; a user process representing the behavior of a human who uses a browser to access the web application, clicking on links, filling forms and so on.

In some simple cases, the second and third process may be combined. In addition to messaging over HTTP(S), client and server-side processes may perform for example cryptographic or database operations.

Example: login application

As an example, we show how to model and analyze the core functionality of a typical website login application, which is a building block of the OAuth models considered in this paper.

Login user process. Assume that user p, who controls browser b, has requested the login page of the web application at h. The process LoginUSerAgent below waits for the response on the newPage(b) channel, which b uses to forward the parsed HTTP response. We model a careful user, that checks that the protocol used is HTTPS and that the page came from the correct host h, avoiding phishing attacks. (We consider careless users to be compromised, that is under the control of the attacker.) If the page contains a form, the user retrieves her credentials and enters them in the loginFormReply which is embedded in a POST message to be forwarded to the browser on channel pageClick. If the credentials were the right ones for the user, the server will reply a second time (triggering a new instance of LoginUSerAgent) with a loginSuccess page, and the user is participating in a valid session. )).

Both the statements assume(Login(p,b,h,uId)) and Expect(ValidSession(p,b,h)) are part of the security specification. The former states that the user p intends to log in as the user uId at the web application h, using the browser b. The latter indicates that at this stage the user demands to be logged in to the right website.

Login server process. We model the server-side login application as follows: The server receives parsed web requests from HttpServer on channel httpServerRequest, which is shared between all server-side applications. It first checks that the request was addressed to the login application over HTTPS. It then parses the headers to extract the session cookie, and parses the request body to obtain the login form containing uId and pwd. It retrieves the credentials of the user uId and checks the validity of the password pwd to authenticate the user. If these checks succeed, the application registers a new server session for the user by the command insert serverSessions(h,sid,uId); if any check fails, it silently rejects the request; otherwise it returns a page loginSuccess().

Before registering the session, the policy event Expect(LoginAuthorized(sp,h,uId,sid)) is triggered to signal the user uId has logged in with the session sid on h.

Security goals. The security goals for the login protocol are written as policies that define when the predicates LoginAuthorized and ValidSession hold. For clarity, we write policies in Datalog style (in ProVerif syntax, they are written right-to-left as clauses that extend the fact predicate).

From the viewpoint of the server, the login protocol has a simple authentication goal: a user should be logged in only if the user intended to log in to that server in the first place. We can intuitively write this goal as a policy for LoginAuthorized: LoginAuthorized(sp,h,uId,sid) :

Server(sp,h), User(up,uId,h), Says(up,Login(up,b,h,uId))

where up and sp are respectively the user and server principals. The last line of the policy accounts for the possibility that the user may have been compromised (that is, her password may be known to that adversary.)

From the viewpoint of the browser, login has successfully completed if the server has logged the user in and both the browser and the server agree on the identity of the user:

ValidSession(up,b,h) :

Server(sp,h), User(up,uId,h), Login(up,b,h,uId), Says(sp,LoginAuthorized(sp,h,uId,sid)).

These policies can be read as the standard correspondence assertions [START_REF] Woo | A semantic model for authentication protocols[END_REF] typically used to specify authentication properties in cryptographic protocols. However, using predicates, we can also encode more intuitive authorization policies that would generally be difficult to encode as ProVerif queries.

A customizable attacker model

We consider a standard symbolic active (Dolev-Yao) attacker who controls all public channels and some principals, but cannot guess secrets or access private channels. Furthermore, the By default, all the channels, tables, and credentials used in WebSpi are private. We define a process AttackerProxy that mediates the attacker's access to these resources, based on a set a configuration flags. The attacker executes a command by sending a message on the public channel admin and if the current configuration allows it, the process executes the command and returns the result (if any) on the public channel result: let AttackerProxy() = in (pub,x:Command); if commandEnabled(x) = true then out(admin,x); in (result,(=x,y:bitstring)); out(pub,y).

The full list of commands that the attacker can send is listed in Table 1. This API is designed to be operational : each command corresponds to a concrete attack that can be mounted on a real web interaction. It includes three categories of attacker capabilities:

Managing principals. The first two commands (enabled by the flag NetworkSetup) allow the attacker to set up an arbitrary population of user and server principals by populating the credentials and serverIdentities tables. If these commands are disabled, the model developer must create his own topology of users and servers. The third and fourth command (enabled by flags MaliciousUsers, MaliciousServers) allow the attacker to obtain the credentials of a selected user or server.

Network attackers. The next two commands (enabled by the flag NetworkAttackers) allow the attacker to intercept and inject arbitrary messages into a connection between any two endpoints. Hence, the attacker can alter the cookies of an HTTP request, but cannot read the (decrypted) content of an HTTPS message.

Malicious websites. The next four commands (enabled by UntrustedWebsites) give the attacker an API to build web applications and deploy them (on top of HttpServer) at a given endpoint, potentially on a honest server. This API gives the attacker fewer capabilities than he would have on a compromised server, but is more realistic, and allows us to discover interesting website-based (PHP) attacks.

Malicious JavaScript. The last two commands (enabled by UntrustedJavaScript) provide the attacker with an API to access features from the browsers' HttpClient, to simulate some of the capabilities of JavaScript code downloaded from untrusted websites.

Inria

From ProVerif results to concrete web attacks

When analyzing a web application model built on top of WebSpi, the model developer may fine-tune the attacker model by setting various flags and then run ProVerif to discover attacks of interest. ProVerif will either prove the model correct (with respect to its security goals), or fail to verify the model, or not terminate.

If verification succeeds, the correctness theorem for ProVerif [START_REF] Blanchet | Automatic verification of correspondences for security protocols[END_REF] guarantees that no attacks exist, at least among the class of attacks considered in the model. We note, however, that this positive result is of limited value, since although WebSpi is quite expressive and extensible, it is not a complete model of the web. For example, it does not cover many browser and server features, such as the treatment of advanced HTTP headers such as Origin and ETag. Hence, our main focus is on discovering attacks, which can be validated in the real world, rather than on providing positive guarantees, which may be violated in practice due to omissions from the model.

When verification fails, ProVerif sometimes produces an attack trace, or else it provides a proof derivation that hints towards a potential attack. Because of the way our attacker model is designed, all attacker actions in traces and derivations appear as concrete commands and responses on the admin and result channels. This makes it possible to filter the ProVerif output to extract formal attacker processes that can sometimes be translated into real-world web attacks.

As an example, we analyze our WebSpi model of the login application against its two security policies, and explore its robustness against different categories of attackers. Our results are summarized at the beginning of Tables 2 and4.

If we only enable network attackers, malicious users, and malicious servers, ProVerif proves the model secure. Suppose we relax the LoginUserAgent process so that naive users may also agree to login over HTTP. ProVerif then finds a network-based password-sniffing attack that breaks both policies.

If we also enable malicious websites, ProVerif finds a standard login CSRF attack. Our login forms, much like the Twitter login form, do not include any unguessable values. So a malicious website that also controls a malicious user Eve can fool an honest user Alice into logging in as Eve. Let us see how we can reconstruct this attack.

In this case, ProVerif produces a proof derivation, but not an attack trace. Such derivations can be very long, since they list all attempted attacks, ending in the successful one, and they explain how the attacker constructed each message. For our example, the derivation has 3568 steps. However, if we select just the messages on the admin and result channels, we end up with a derivation of 89 steps. Most of the steps towards the beginning of this derivation are redundant commands that are easy to identify and discard. Starting from the end, we can optimize the derivation by hand to finally obtain an attack in 7 steps (a time-consuming but rewarding process).

Next, we verify the attack by modeling the malicious website as a ProVerif process that uses the attacker API: let TwitterAttack(twitterLoginUri:Uri,eveAppUri:App, eveId:Id,evePwd:Secret) = (* Alice browses to Eve's website *) out (admin,getServerRequest(eveAppUri)); in (result,(=getServerRequest(eveAppUri), (u:Uri,req:HttpRequest,hs:Params,corr:bitstring)));

(* Eve redirects Alice to login as Eve@Twitter *) out(admin,sendServerResponse(eveAppUri,(u, httpOk(twitterLoginForm(twitterLoginUri,eveId,evePwd)), nullCookiePair(),corr))).

If ProVerif can find the attack again using just this attacker process, disabling all other attackers (by setting attacker mode to passive), then we say that the attack is concrete. Finally, we attempt to execute the attack on a real website. We rewrite the process above as a PHP script and, indeed, we find that a login CSRF attack can be mounted on the Twitter login page. This attack was known to exist, but as we show in the following section, it can be used to build new login CSRF attacks on Twitter clients.

5 Analyzing OAuth 2.0 using ProVerif Following the pattern of the Login example in the previous section, we build models for two protocol configurations of the OAuth protocol using the WebSpi library, and analyze their security properties.

OAuth 2.0 model

We consider an unbounded number of users and servers. Each user is willing to browse any website (whether trusted or malicious) but only sends secret data to trusted sites. Each server may host one or more of the applications described below.

Login: As shown in Section 4, this application consists of a server process LoginApp and a corresponding user-agent process LoginUserAgent that together model form-based login for websites. In our model, both OAuth authorization servers and their client websites host login applications.

Data Server: An application that models resource servers. It includes a server process DataServerApp that offers an API with two functions: getData retrieves all the data for a particular user, and storeData stores new data for a user. We treat getId as a special case of getData where the caller is only interested in the user's identity. Users logged in locally on the resource server (through its LoginApp) may access their data through a browser, and their behavior is modeled by a user-agent process DataServerUserAgent. OAuth clients may remotely access data on behalf of their social login users, by presenting an access token.

OAuth Authorization (UserAgent Flow): A three-party social web application that models the user-agent flow of the OAuth protocol. The process OAuthImplicitServerApp models authorization servers, and the process OAuthUserAgent models resource owners. These processes closely follow the protocol flow described in Section 3. The process OAuthImplicitClientApp models clients that offer social login; it offers a social login form for resource owners to click on to initiate social sign-on. When sign-on is completed, it provides the resource owner with additional forms to get and store data from the resource server. These additional data actions are not explicitly covered by the OAuth protocol, but are a natural consequence of its use.

OAuth Authorization (Authorization Code Flow): A three-party social web application that models the authorization code flow of the OAuth protocol, as described in Section 3. The process OAuthExplicitClientApp models clients and OAuthExplicitServerApp models authorization servers.

We elide details of the ProVerif code for these applications, except to note that they are built on top of the library processes HttpClient and HttpServer, much like the login application, and implement message exchanges as described in the protocol. Each process includes Assume and Expect statements that track the security events of the protocol. For example, the OAuthUserAgent process assumes the predicate SocialLogin(RO,b,sid,C,AS,RS) before sending the social login form to the client; after login is completed it expects the predicate SocialLoginDone(RO,b,sid,C,u,AS,RS). We then encode the security goals of Section 3 as clauses defining such predicates. The full script is available online [START_REF] Bansal | WebSpi and web application models[END_REF].

Inria

Model

Lines

Results of the ProVerif analysis

We analyze the security of different configurations of our OAuth model using ProVerif. Table 2 summarizes our positive verification results. Each line lists a part of the model, the number of lines of ProVerif code, and the time taken to verify them. The most general model for which we were able to obtain positive results verifies OAuth in both explicit and implicit grant modes against network attackers, malicious resource owners and clients, untrusted websites and JavaScript. However, we assume that each client has exactly one authorization server, every authorization server is honest, all exchanges are over HTTPS, and no web vulnerabilities exists on honest servers, that is, clients and authorization servers do not host HTTP redirectors and protect all their forms against login and data CSRF attacks. Under these conditions, ProVerif is unable to find any attacks, even considering an unbounded number of sessions. This should not be interpreted as a definitive proof of security, since we model only a subset of OAuth configurations and our web model is not complete. Under other attacker configurations, ProVerif finds protocol traces that violate the security goals. Table 4 summarizes the attacks found by ProVerif. In each case, we were able to extract attacker processes (as we did for the login application of Section 4). In Appendix A we provide processes for some of these attacks.

These formal attacks led to our discovery of concrete, previously unknown attacks involving Facebook, Twitter, Yahoo, IMDB, Bitly and several other popular websites. We focused on websites on which we quickly found vulnerabilities. Other websites may also be vulnerable to these or related attacks. Table 5 in Appendix A summarizes our website attacks. The rest of this section describes and discusses these attacks.

Going from the formal counterexamples of ProVerif in Table 4 to the concrete website attacks of Table 5 involved several steps. First we analysed the ProVerif traces to extract the short attacker processes of Appendix A, as illustrated in Section 4 for the login application. Then we collected normal web traces using the TamperData extension for Firefox. By running a script on these traces, we collected client and authorization server login URIs, CSRF vulnerable forms, and client application identifiers. Using this data, we wrote website attackers in a combination of PHP and JavaScript and examined an arbitrary selection of OAuth 2.0 clients and authorization servers. Many of these steps can be automated; for example, AUTHSCAN [START_REF] Lei | AUTHSCAN: Automatic extraction of web authentication protocols from implementations[END_REF] shows how to heuristically extract concrete attacks from ProVerif counterexamples produced by WebSpi models.

Social CSRF attacks against OAuth 2.0

To begin with, we note that if any of the exchanges of our OAuth model is allowed over unencrypted HTTP, ProVerif immediately finds a network-based attack that breaks our security goals, either by stealing the password or access token, or by injecting a forged request or re-sponse. In the rest of this paper, we will ignore such well-known attack vectors and look for more interesting attacks. We first consider Social CSRF attacks.

To better understand these attacks, recall the the typical OAuth protocol flow involves four forms where the user interacts with the protocol: the login form at the authorization server, the social login form ("Login with Facebook") at the client, the authorization form at the authorization server, and (potentially) a data entry (comment) form at the client. When the user submits (clicks on) any of these forms, an HTTP GET or POST request is sent to a form action URI, along with the parameters encoded in the form. If, however, there is no CSRF protection at this action URI, e.g. a session-specific secret token in the form parameters, a malicious website may directly send a user to the action URI without the user ever agreeing to submit the form, leading to various kinds of CSRF attacks that may break the user's authentication or authorization goals.

We identify several conditions under which OAuth 2.0 deployments are vulnerable to Social CSRF attacks. In our models, such attacks appear in two forms: either the network attacker injects an HTTP response which redirects the user to a carefully crafted URI, or a malicious website entices the user into clicking on a URL or submit button.

Automatic Login CSRF. Suppose the social login form has no CSRF protection. As described in Section 2, this is true for many OAuth clients, such as CitySearch. Then, a malicious website can effectively bypass the SocialLogin step of the protocol and directly redirect the user's browser to the TokenRequest or CodeRequest step. If the authorization server then silently authorizes the token release, say because the user is logged in and has previously authorized this client, then the protocol can proceed to completion without any interaction with the user. Hence, a malicious website can cause the resource owner to log in to CitySearch (through Facebook) even if she did not wish to. We call this an automatic login CSRF, and it is widespread among OAuth clients (see Table 5).

In our model, ProVerif finds this attack on both OAuth flows, as a violation of the SocialLoginAccept policy on our model. It demonstrates a trace where it is possible for the OAuth client process to execute the event SocialLoginAccept even though this resource owner never previously executed SocialLogin. The trace also violate the user's SocialLoginDone policy. This is an interesting example of how a seemingly innocuous vulnerability in the client website can lead to the failure of the expected security goals of an honest user, who may simply have wished to remain anonymous.

Social Login CSRF through AS Login CSRF. Suppose the login form on the authorization server is not protected against login CSRF. This is the case for Twitter, as described in Section 4.3. In this case, a malicious website can bypass the Login step of the protocol and directly pass his own credentials to the login form's action URI. Hence, the user's browser will be silently logged into the attacker's Twitter account. Furthermore, if the user ever clicks on "Login with Twitter" on any client website, he will be logged into that website also as the attacker, resulting in a social login CSRF attack. All future actions by the user (such as commenting on a blog) will be credited to the attacker's identity. We confirmed this attack on Twitter client websites such as WordPress.

In our model, ProVerif finds a violation of the user's SocialLoginDone policy; the browser completes social sign-on for one user but the client website has accepted the login (SocialLoginAccept) for a different user in the same session. This is an example where a flaw in a single authorization server can be amplified to affect all its clients. Social Login CSRF on stateless clients. Suppose an OAuth client does not implement the optional state parameter. Then it is subject to a second kind of social login CSRF attack, as predicted by the OAuth specification. A malicious user (in concert with a malicious website) can inject his own TokenResponse in place of an honest resource owner's TokenResponse in step 5 of the useragent flow, by redirecting the user to the corresponding URI. (In the authorization code flow, the Inria malicious user injects her CodeResponse instead.) When the client receives this response, it has no way of knowing that it was issued for a different user in response to a different TokenRequest. Many OAuth clients, such as IMDB, do not implement the state parameter and are vulnerable to this attack.

ProVerif again finds a trace that violates SocialLoginDone; the browser and client have inconsistent views on the identity of the logged-in user.

Social Sharing CSRF. Once social sign-on is complete, the client has an access token that it can use to read, and sometimes write, user data on the resource server. Suppose a form that the client uses to accept user data is not protected against CSRF; then this vulnerability may be amplified to a CSRF attack on the resource server. For example, as described in Section 2, the review forms on CitySearch are not protected against regular CSRF attacks, and data entered in these forms is automatically cross-posted on Facebook. Hence, a malicious website can post arbitrary reviews in the name of an honest resource owner, and this form will be stored on Facebook, even though the resource owner never intended to fill in the form, and despite Facebook's own careful CSRF protections.

ProVerif finds this attack on both OAuth flows, as a violation of the APIRequest policy at the client. It demonstrates a trace where a malicious website causes the client process to send a storeData API request, even though the resource owner never asked for any data to be stored.

Token stealing attacks against OAuth 2.0

We identify three conditions under which OAuth 2.0 deployments are vulnerable to access token and authorization code redirection, leading to serious attacks such as unauthorized login on the client and user data theft on the resource server. All of these attacks rely on the existence of an attacker-controlled URIs on the client website, and on the authorization server's willingness to issue authorization codes and access tokens to these URIs. The policy that an authorization server uses to match a given redirect uri to a registered client is implementation-specific. For example, Facebook and Live identify clients by a domain, and are willing to issue tokens to any URI on that domain. This gives clients maximum flexibility in terms of the pages where they can embed social login. Conversely, it substantially increases the attack surface. As we shall see, any untrusted page within this URI range can lead to serious attacks.

Unauthorized Login by Authentication Code Redirection. Suppose a client website hosts an HTTP Redirector that forwards all GET requests to an attacker's website. Then any browser that visits this URI will be forwarded to the attacker's webpage, and the browser will automatically also attach any parameters in the original URI, such as the authorization code, as a parameter to the redirected URI. We found such redirectors on multiple websites, including on WordPress as described below.

Notably, if the HTTP redirector is a valid redirect uri for the authorization server, a malicious website can perform a triple-redirection attack to steal the authorization code: (1) it redirects the user to the authorization server to request a code (CodeRequest) but with the redirect uri set to the HTTP redirector; (2) the authorization server redirects the browser to the redirect uri with the authorization code as parameter (CodeResponse); (3) the redirector sends the browser to the attacker's website with the authorization code as parameter. Once it has obtained the authorization code, the website can impersonate the resource owner at the client website by using social login again but using its own browser. This time, when the client sends a CodeRequest, the malicious browser does not contact the authorization server; instead it returns the stolen authorization code in a CodeResponse. When the client subsequently verifies this code (using APITokenRequest) it will be given the identity of the honest resource owner, not the attacker, completely breaking the authentication goal of social sign-on.

In our model, ProVerif finds this attack as a violation of the SocialLoginAccept policy; the client completes social login for a user even though the user never executed Login with this browser; the browser in fact belongs to the attacker.

To see an example of the attack flow, consider the Facebook client WordPress. Suppose the attacker has a blog on WordPress. For a fee, WordPress allows its members to forward all traffic sent to their blog to an external website. Hence, the attacker can set up an HTTP redirector at eve.wordpress.com. When a resource owner tries to log in to someblog.wordpress.com using Facebook, she is redirected to Facebook and then back with the authorization code to someblog.wordpress.com/connect/?code=C. However, Facebook is willing to redirect this code to any URL of the form *.wordpress.com/* because the domain registered for the WordPress client at Facebook is just wordpress.com. So, to execute our attack, a malicious website redirects the honest resource owner to Facebook with the redirection uri eve.wordpress.com, and the authorization code will be redirected back to the website. We note that this attack is not prevented by using a state parameter at the client, since the real client never sees the authorization code.

Resource Theft by Access Token Redirection. If an OAuth authorization server is willing to enter a user-agent flow with a client that has an HTTP redirector, then an attack similar to the one above becomes possible, except that the malicious website is able to directly obtain the access token instead of the authorization code, again using a triple redirection attack. It can then use this access token to access the resource server APIs to steal an honest resource owner's data.

ProVerif finds this attack as a violation of the APIResponse policy; since the access token has been stolen, the resource owner can no longer reliably authenticate that it is only releasing user data to the authorized client.

For example, we found such an attack on Yahoo, since it offers an HTTP redirector as part of its search functionality. A malicious website can read the Facebook profile of any user who has in the past used social login on Yahoo. It is interesting to note that even though Yahoo itself never engages in the user-agent flow (it only uses authorization codes), Facebook is still willing to enter into a user-agent flow with a website that pretends to be Yahoo, which leads to this attack.

Code and Token Theft by Hosted User Content. A simpler variation of the above authentication code and access token stealing attacks occurs on client websites that host user-controlled content on URIs that can be valid redirect uris at the authorization server. For example, Dropbox allows user content at dl.dropbox.com, and its registered domain at Facebook is just dropbox.com. Hence, any user can upload an HTML file to dl.dropbox.com and by using the URI for this page as redirect uri steal the Facebook access token for any other Dropbox user.

A special case of this attack is a Cross Site Scripting on the client website, whereby an attacker can inject JavaScript into a trusted page. Such a script can steal the access token for the current user from a variety of sources, including by starting a new OAuth user-agent flow with the authorization server.

ProVerif finds these attacks as violations of the APIResponse policy, when we enable UntrustedJavaScript or UntrustedWebsite on the client.

Cross Social-Network Request Forgery. Suppose an OAuth client supports social login with multiple social networks, but it uses the same login endpoint for all networks. This is the case on many websites that use the JanRain or GigYa libraries to manage their social login. So far, we have assumed that all authorization servers are honest, but in this case, if one of the authorization servers is malicious, it can steal an honest resource owner's authorization code and access token at any of the other authorization servers, by confusing the OAuth client about which social network the user is logging in with.

For example, the JanRain website itself supports login with a number of OAuth providers, in-Inria cluding Live, Facebook, LinkedIn, and SalesForce, but uses the same domain login.janrain.com to host all its redirect uris. If any of these providers wanted to steal (say) a JanRain user's Facebook access token (or authorization code), it could redirect the user to Facebook's authorization server but with its own redirect uri on JanRain. When JanRain receives the token (or code) response at this URI, it would assume that the token came from the malicious authorization provider and send back the token (or code) with any subsequent APIRequest (or TokenRequest) to the malicious provider.

In our model, if we enable multiple, potentially malicious, authorization servers, ProVerif finds the above attack as a violation of the APITokenResponse policy on the authorization code flow, and as a violation of APIResponse policy on the user-agent flow.

Discussion

Many of the attacks described in this work were known (or predicted) in theory, but their existence in real websites were usually unknown before we reported them. We notified all the websites mentioned in this paper, and most have since been fixed.

Our attacks rely on weaknesses in OAuth clients or authorization servers, and we find that these do exist in practice. It is worth discussing why this may be the case.

CSRF attacks on websites are widespread and seem to be difficult to eradicate. We found a login CSRF attack on the front page of Twitter, a highly popular website, and it seems this vulnerability has been known for some time, and was not considered serious, except that it may now be used as a login CSRF attack on any Twitter client. Our analysis finds such flaws, and proposes a general rule-of-thumb: that any website action that leads to a social network action should be protected from CSRF.

Open redirectors in client websites are another known problem, although most of the focus on them is to prevent phishing. Our attacks rely more generally on any redirector that may forward an OAuth token to a malicious website. We found three areas of concern. Search engines like Yahoo use redirection URLs for pages that they index. URL shortening services like Bitly necessarily offer a redirection service. Web hosting services such as WordPress offer potentially malicious clients access to their namespace. When integrating such websites with social networks, it becomes imperative to carefully delineate the part of the namespace that will be used for social login and to ensure there are no redirectors allowed in this namespace.

More generally, websites that integrate OAuth 2.0 should use separate subdomains for their security-critical pages that may have access to authorization codes and access tokens. For example, Yahoo now uses login.yahoo.com as a dedicated sub-domain for login-related activities. Pages on this domain can be carefully vetted to be free of web vulnerabilities, even if it may be hard to fully trust the much larger yahoo.com domain.

The incorrect treatment of redirection URIs at authorization servers enables many of our attacks. Contrarily to the OAuth 2.0 specification recommendations, Facebook does not require the registration of the full client redirection URI, possibly in order to support a greater variety of clients, but also because modern browsers only enforce client-side protections at the Origin level. Finding a way to protect tokens from malicious pages in the same domain remains an open problem and the subject of ongoing research.

Finally, a word of comparison between OAuth 2.0 and its competitors. OAuth 2.0 lacks request and response authentication, which leads to several of the issues found in this paper. Still, correct implementations of OAuth 2.0 do not suffer from these attacks. OAuth 1.0 featured both request and response authentication, but it was deemed too difficult to implement for widespread adoption; moreover, it was still vulnerable to session fixation attacks [START_REF] Hammer-Lahav | OAuth Security Advisory: 2009.1 -Session Fixation Attack[END_REF]. OpenID 2.0 features response authentication but not request authentication, which prevents some of the attacks found in this paper but not attacks like OpenID Realm Phishing [START_REF]Phishing Brainstorm[END_REF]. Despite its shortcomings, OAuth 2.0 seems to be gaining traction, and upcoming single sign-on protocols such as OpenID Connect [START_REF][END_REF] are being built on top of it. Formal analyses of such composite protocols are an interesting topic for future work.

Generating WebSpi Models from Concrete Websites

We acknowledge the difficulty for most web programmer to write WebSpi models of their website manually. To address this issue, we propose a framework for extracting user-agent and serverapp processes directly from the security-sensitive part of carefully-written websites. Our model extraction framework, depicted in Figure 6, consists of three components: a subset of PHP equipped with a standard web library and its ProVerif counterpart; a subset of JavaScript equipped with a library for cryptography and secure communications and its ProVerif counterpart; automatic translations from these PHP and JavaScript subsets to the applied pi-calculus.

The generated processes may then be composed with the WebSpi library and automatically verified against the web application security goals. To support our translation, we extended the WebSpi model with a more realistic treatment of JavaScript that allowed multiple processes to share the same heap.

We focus on demonstrating the effectiveness of our translations rather than their soundness. At their core, they follow Milner's famous "functions as processes" encoding of the lambda calculus into the pi calculus [START_REF] Milner | Functions as processes[END_REF]. Similar translations to ours have previously been defined (and proved sound) for F# [START_REF] Bhargavan | Verified interoperable implementations of security protocols[END_REF] and Java [START_REF] Avalle | JavaSPI: A framework for security protocol implementation[END_REF]. Writing a script in this subset is very similar to writing a ProVerif process; the main elements of the translation are given in Table 3.

Inria

PHP

For error handling purposes, many operations such as reading a database, accessing parameters or parsing a template are performed within atomic if statements. Any missing else branch is implicitly treated as else die(""); and translated to an httpError().

Before using session variables, the session cookie must be verified with a call to sessionstart. To simulate the actual behavior of this function, the three checks in the translation of session start have else branches that will create a session cookie (if missing) and redirect the user to the same page (if required, over HTTPS). This behavior is only faithful if cookies are enabled on the client.

Inria

A typical script will first verify that its required parameters (either $ GET or $ POST, or a combination of both) are present, perform access control (based on the user's session), perform some operations based on the input (such as looking up a database) and return either an HTML result, represented by a data constructor that depends on all the dynamic values embedded in the page, or an error message, or a redirection.

In most cases, the parameters of a script come from an HTML form or link. In theory, if instead of using data constructors (sprintf) to represent HTML output, we directly parsed the HTML output to extract all forms, their method, target action and field names, we could generate User Agent processes to model the submission of forms. However, for now, we submit forms in JavaScript, using accesses to the DOM document.forms [i].field, which we translate to reading from a user input channel to construct the parameters of the form submission.

Constants are converted to symbolic names by hashing, to get consistent names between PHP and JavaScript. Similarly, the name of a data constructor depends on the hash of its template. We use sscanf to reconstruct serialized messages between PHP and JavaScript, and translate it to a pattern match on the data constructor for the hashed template. The template may follow a standard serialization format such as JSON.

We also use a library function get table("t", $x, ..., &$y) to perform database queries. This function works exactly like the ProVerif construct get t(=x, ..., y): the variables that are not passed by reference are used to construct the WHERE clause of the SQL query (the column names are retrieved from the table schema), while the variables passed by reference are filled with the result of the query (if multiple rows are selected, the first one is used).

To illustrate the translation on a concrete example, we provide the main section of the ProVerif translation (excluding the preamble and declarations) of the authorization handler from Figure 7 in Figure 8. )),nullCookie(), corr))

Figure 8: ProVerif (partial) translation of the script in Figure 7 Since JavaScript does not natively support features such as sscanf or encryption, we provide them through a library. We distinguish such library functions with a special prefix, to distinguish them from global variables the script may try to access.

Our translation from JavaScript to ProVerif reflects the shared memory model of the browser. A single heap table in the browser stores pairs of locations and values on an origin (rather than page) basis, to reflect the ability of same-origin pages to read each other's variables. Because JavaScript is asynchronous and event driven, we support the translation of functions and closures. We intend each embedded script to correspond to the handler for one event (e.g. the page loading, a form being submitted, a link being clicked). Thus, the embed script library function accepts a script S, a target DOM element d and event name e, which is used to generate the concrete script: d.addEventListener(e, function(){S}).

To illustrate the translation, we give in Figure 9 the login form event submission handler and its user agent process translation. This script simply reads the username and password entered in the login form, computes a login secret based on the username, password and salt and sends the result along with the username as a POST query to the login script. If we wanted to include a CSRF token, it would be set in the data constructor of the login form and accessible to the user agent within the variable d.

Limitations

The main limitation of our approach is the requirement to use the very limited subset of PHP in order to allow automated translation. Thus, this approach is not viable for the analysis of large deployed websites. However, it is useful for designing new web applications. The initial prototype can use our restricted subsets to implement the core features and protocols, which in most cases are relatively simple. The functionality of the application is now modeled in PHP and JavaScript, and can be directly tested. Moreover, thanks to the automated translation the security of the design can be analyzed in WebSpi against various attacker models. Once the core application has been tested and verified, it can be extended using all the features of PHP and JavaScript into a fully featured website.

Another, more technical limitation of the translation is that, since ProVerif uses only symbolic equality, a program such as if(1+1===2) echo "a"; else echo "b"; cannot be faithfully translated. We work around this problem by ensuring compared values rely on a combination Finally, even though model extraction is automatic, it is still up to the programmer to specify his intended security goals and interpret the result of the verification.

Related Work

A number of other works present attacks on single sign-on and web authorization mechanisms like OAuth 2.0 [START_REF] Somorovsky | On breaking saml: Be whoever you want to be[END_REF][START_REF] Wang | Signing me onto your accounts through facebook and google: A traffic-guided security study of commercially deployed single-sign-on web services[END_REF][START_REF] Sun | The devil is in the (implementation) details: an empirical analysis of OAuth SSO systems[END_REF]. These attacks are similar to the ones discovered in our work and provide further evidence for the need for a systematic formal security analysis of such mechanisms that accounts for the precise details of the browser and common web vulnerabilities. In this Section, we review previous work related to formal models of web browsing and formal analysis of web authorization protocols similar to OAuth 2.0.

Formal models of web browsing

Gross et al. [START_REF] Groß | Browser model for security analysis of browser-based protocols[END_REF] model the communication behavior of web browsers as automata and use these state machines to prove the security of a password-based authentication protocol by hand. Their model does not cover cookies or scripts and hence does not cover most of the website attacks discussed in this paper.

Yoshihama et al. [START_REF] Yoshihama | Information-Flow-Based Access Control for Web Browsers[END_REF] present a browser security model that relies on information flow labels to enforce fine-grained access control, focusing on mashups. They describe the browser by means of a big-step operational semantics that models the evaluation of client-side scripts. The model includes multiple browser windows, the DOM, cookies and high-level HTTP requests. Some of the attacks we presented cannot be observed in that model. For example, CSRF attacks are prevented by construction. By contrast, since our goal is to analyze protocols and detect potential flaws, our browser model makes it possible to observe any sequence of events that can be triggered by a combination of web users, client side scripts and server-provided pages, including those leading to security violations.

Motivated by [START_REF] Yoshihama | Information-Flow-Based Access Control for Web Browsers[END_REF], Bohannon and Pierce [START_REF] Bohannon | Featherweight Firefox[END_REF] formalize the core of a web browser as an executable, small-step reactive semantics. The model gives a rather precise description of what happens within a browser, including DOM tags, user actions to navigate windows, and a core scripting language. Our formalization instead abstracts away from browser implementation details and focuses on web pages, client-side scripts and user behavior. Both [START_REF] Yoshihama | Information-Flow-Based Access Control for Web Browsers[END_REF] and [START_REF] Bohannon | Featherweight Firefox[END_REF] focus on the web script security problem, that is how to preserve security for pages composed by scripts from different sources. The model does not encompass features such as HTML forms, redirection and https which are important in our case to describe more general security goals for web applications.

Akhawe et al. [START_REF] Akhawe | Towards a formal foundation of web security[END_REF] propose a general model of web security, which consists of a discussion of important web concepts (browsers, servers and the network), a web threat model (with users and web, network and gadget attackers), and of two general web security goals: preserving existing applications invariants and preserving session integrity. They implement a subset of this general model in the Alloy protocol verifier [START_REF] Jackson | Alloy: A logical modelling language[END_REF]. Alloy lets user specify protocols in a declarative object-modeling syntax, and then verify bounded instances of such protocols by translation to a SAT solver. This formal subset of the web model is used on five different case studies, leading to the re-discovery of two known vulnerability and the discovery of three novel vulnerabilities. Our work was most inspired by [START_REF] Akhawe | Towards a formal foundation of web security[END_REF], with notable differences. We directly express our formal model in the variant of the applied pi-calculus, a formalism ideally suited to describe security protocols in an operational way, that is focusing on a high-level view of the actions performed by the various components of a web application. This approach reflects as closely as possible the intuition of the human designer (or analyzer) of the protocol, and helps us in the systematic reconstruction of attacks from formal traces. This language is also understood by the ProVerif protocol analysis tool, that is able to verify protocol instances of arbitrary size, as opposed to the bounded verification performed in Alloy.

Unbounded verification becomes important for flexible protocols such as OAuth 2.0, that even in the simplest case involve five heterogeneous principals and eight HTTP exchanges. In general, one may even construct OAuth configurations with a chain of authorization servers, say signing-on to a website with a Yahoo account, and signing-on to Yahoo with Facebook. For such extensible protocols, it becomes difficult to find a precise bound on the protocol model that would suffice to discover potential attacks.

More recently, Bai et al. [START_REF] Lei | AUTHSCAN: Automatic extraction of web authentication protocols from implementations[END_REF] present AUTHSCAN, an end-to-end tool to recover (and verify) authentication protocol specifications from their implementations. AUTHSCAN is composed of three modules. The first module extracts a protocol model by testing against an existing implementation. This is the main focus of this work. We do not attempt to extract models form protocol traces, but instead we provide an automated translation when the (PHP) source code is available, and resort to manual model extraction when the source code is not available. The second module, parametric in an attacker model and a set of security properties, verifies the protocol model using either ProVerif, PAT or AVISPA. The authors mostly use ProVerif, with a strict subset of our WebSpi attacker model [START_REF] Bansal | Discovering concrete attacks on website authorization by formal analysis[END_REF]. This is a testament to the usefulness of WebSpi as a general-purpose web-protocol analysis library. The third module aims to confirm attacks discovered by the formal analysis instantiating the attack with the real-world data (IP addresses, credentials) used for testing. We also reconstruct concrete attacks from ProVerif traces, but we leave it to future work to make this process fully automatic. Unfortunately at Inria the time of submission the implementation of AUTHSCAN is still not publicly available2 , so we cannot compare more closely our attack reconstruction techniques.

Formal analysis of web authorization

Early single sign-on protocols, such as Passport, Liberty, Shibboleth, and CardSpace were often formally analyzed [START_REF] Pfitzmann | Analysis of liberty single-sign-on with enabled clients[END_REF][START_REF] Pfitzmann | Federated identity-management protocols[END_REF][START_REF] Hansen | Using static analysis to validate the saml single sign-on protocol[END_REF][START_REF] Bhargavan | Verified implementations of the information card federated identity-management protocol[END_REF][START_REF] Armando | Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps[END_REF], but these analyses mainly covered their cryptographic design against standard network-based adversaries, and do not account for the website attacks (such as CSRF) discussed in this paper.

Pai et al. [START_REF] Pai | Formal Verification of OAuth 2.0 Using Alloy Framework[END_REF] adopt a Knowledge Flow Analysis approach [START_REF] Torlak | Knowledge flow analysis for security protocols[END_REF] to formalize the specification of OAuth 2.0 in predicate logics, a formalism similar to our Datalog-like policies. They directly translate and analyze their logical specification in Alloy, rediscovering a previously known protocol flaw. Our ProVerif models are more operational, closer to a web programmer's intuition. Our analysis with respect to different classes of attackers is able to discover a larger number of potential protocol abuses.

Chari et al. [START_REF] Chari | Universally composable security analysis of oauth v2.0[END_REF] analyze the authorization code mode of OAuth 2.0 in the Universal Composability Security Framework [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF]. They model a slightly revised version of the protocol that assumes that both client and servers use TLS and mandates some additional checks. This model is proven secure by a simulation argument, and is refined into an HTTPS-based implementation.

Miculan and Urban [START_REF] Miculan | Formal analysis of Facebook Connect Single Sign-On authentication protocol[END_REF] model the Facebook Connect protocol for single sign-on using the HLPSL specification language and AVISPA. Due to the lack of a specification of the protocol, which is offered as a service by Facebook, they infer a model of Facebook Connect in HLPSL by observing the messages effectively exchanged during valid protocol runs. Using AVISPA, they identify a replay attack and a masquerade attack for which they propose and verify a fix.

The AUTHSCAN tool [START_REF] Lei | AUTHSCAN: Automatic extraction of web authentication protocols from implementations[END_REF] described above is validated by analyzing single-sign-on web protocols, including Mozilla's BrowserID and Facebook Connect, and discovering several fresh vulnerabilities. In particular, AUTHSCAN finds a vulnerability in Facebook Connect because it infers from observed traces that one particular token-bearing message in not sent over HTTPS, but is instead sent over HTTP. Our analysis did not discover this particular attack because we decided to model Facebook as using HTTPS in all the token-bearing communications. The kind of vulnerabilities we discovered tend to concern flaws in the design of a bug-free implementation, whereas recovering models from traces seems also able to discover lower-level "implementation bugs".

Conclusions

We present a security analysis of the OAuth 2.0 protocol, using ProVerif, extended with the WebSpi library that formalizes web users, applications and attackers. Our analysis establishes both positive and negative security results, and the design of our library makes it easy to translate formal counterexamples into concrete attacks on websites. The effectiveness of the approach is validated by the discovery of several vulnerabilities in leading websites that use the OAuth 2.0 protocol. Expert human reviewers would have been able to find these attacks on a case-by-case basis. Our contribution is to make this discovery systematic, and partially automated. The models presented here do not cover some other common attacks, such as XSS, SQL Injection, and DNS rebinding. In future work, we plan to extend WebSpi in order to capture also these attacks, and verify more web security mechanisms and protocols. The first three configurations correspond to normal website attacks and their effect on website security goals. The rest of the table shows OAuth attacks discovered by ProVerif. For each configuration, we name the security policy violation found by ProVerif, the number of steps in the ProVerif derivation, and the size of our attacker process. The first section summarizes attacks on authorization servers, the second on OAuth clients, and the third on OAuth client libraries. This is a representative selection of attacks found between June 2011 and February 2012. Most of these websites have since been fixed.

Figure 1 :

 1 Figure 1: (L) Log in with Facebook on Wordpress; (R) Facebook requires authorization.

  POST /rate/listing?listingId=628337570 HTTP/1.1 Host: lasvegas.citysearch.com Content-Type: application/x-www-form-urlencoded Cookie: usrid=ab76fb... title=GREAT&rating=6&publishToFacebook=true&text=...

Figure 2 :

 2 Figure 2: (L) CitySearch review form; (R) Corresponding Post request.

Figure 3 :

 3 Figure 3: OAuth 2.0: User-Agent Flow.

Figure 4 :

 4 Figure 4: OAuth 2.0: Authorization Code Flow.

Inria

3. 4 A

 4 Threat Model for OAuth 2.0

  SocialLoginDone(RO,b,sid',C,u,AS,RS) : Login(RO,b,sid,AS,u), SocialLogin(RO,b,sid',C,AS,RS), Authorize(RO,b,sid,C,idPermission), Says(C,SocialLoginAccept(C,sid',u,AS,RS)).

Inria 4 . 1 . 2 Cryptography

 412 ,...,Mn) constructor or destructor f applied to M1,...,Mn =M matching operatorProVerif models symbolic cryptography: cryptographic algorithms are treated as perfect blackboxes whose properties are abstractly encoded using constructors (introduced by the fun keyword) and destructors (introduced by the reduc keyword). As an example, consider authenticated encryption: fun aenc(bitstring,symkey): bitstring. reduc forall b:bitstring,k:symkey; adec(aenc(b,k),k) = b.Given a bit-string b and a symmetric key k, the term aenc(b,k) stands for the bitstring obtained by encrypting b under k. The destructor adec, given an authenticated encryption and the original symmetric key, evaluates to the original bit-string b.

  fun hash(bitstring): bitstring. fun pk(privkey): pubkey. fun wrap(symkey,pubkey): bitstring. reduc forall k:symkey,dk:privkey; unwrap(wrap(k,pk(dk)),dk) = k. fun sign(bitstring,privkey): bitstring. reduc forall b:bitstring,sk:privkey; verify(sign(b,sk),pk(sk)) = b.

  forall p:Principal,e:Fact; fact(e) →fact(Says(p,e)); forall p:Principal,e:Fact; fact(Compromised(p)) →fact(Says(p,e)).

Figure 5 :

 5 Figure 5: WebSpi architectural diagram.

  Inria if p = aboutBlank() then (let p1 = mkPage(u) in insert pageOrigin(p1,o,h,u); out (newPage(b),(p1,u,dataIn))) else (if aj = ajax() then (get pageOrigin(=p,oldorig,oldh,olduri) in if (foo = xdr() || oldorig = o) then out (ajaxResponse(b),(p,u,dataIn))))) |(let httpRedirect(redir) = resp in out (internalRequest(b),(redir,httpGet(),ref,p,notajax())))) )

(

  get pageOrigin(p,o,h,ref) in get cookies(=b,=originhost(o),=slash(),cs) in get cookies(=b,=originhost(o),=h,ch) in get storage(=b,=o,s) in out (getCookieStorage(b),(p,cookiePair(protocolCookie(domcookie(cs),o), protocolCookie(domcookie(ch),o)),s)))

  let LoginUserAgent(b:Browser) = let p = principal(b) in in(newPage(b),(p1:Page, u:Uri, d:bitstring)); let (=https(), h:Host, loginPath(app)) = (protocol(u),host(u),path(u)) in (( let loginForm(as) = formTag(d) in get credentials(=h,=p,uId,pwd) in if assume(Login(p,b,h,uId)) then out(pageClick(b),(p1,u,httpPost(loginFormReply(d,uId,pwd)))) )|( if loginSuccess() = d then event Expect(ValidSession(p,b,h)))

Figure 6 :

 6 Figure 6: Model extraction and verification framework

  let dataConst T( e 1 , . . . , e n )= s in session start() if protocol(url) = https() then let cookiePair(session cookie,path cookie) = cookie jar in if secure(session cookie) <> nullCookie() then [...] embed script(S,DOM,event) let [P, S]UserAgent(b:Browser) = S JS free script S:bitstring. [...] script S f(e1, .., en) f( e 1 , . . . , e n ) $ GET['a'], $ POST['a'] get a, post a $ SESSION['a'] get serverSessions(=host, =session cookie, sessionPair(=str a, session a)) in [...] session a $x = e let var x = e in e + f , e.f ... add( e , f ), concat( e , f ) ...

Figure 9 :

 9 Figure 9: Login form handler and its translation

6 .

 6 APIRequest(C,RS,token,getId()): C makes an API request getId() to RS with token. RO is logged in to C in a browser session sid' associated with u at AS, granting access to RS.

	7. APIResponse(RS,C,token,getId(),u): RS verifies token, accepts the API request and returns u
	to C.
	8. SocialLoginAccept(C,sid',u,AS,RS): C accepts RO's social sign-on session sid' as u at AS for RS.
	9. SocialLoginDone(RO,b,sid',C,u,AS,RS): Inria

Table 1 :

 1 Principals createServer(sp)create a new server for principal sp createUser(up,h,p) create a new user up for the app at path p on host h compromiseUser(id,h,p)force user with login id on app p at h to reveal its password compromiseServer(h) force principal of server hosted at h to reveal its secret key A command API for the active web attacker attacker can create new data and can encrypt or decrypt any message for which it has obtained the cryptographic key, but otherwise cannot break cryptography.

	Network	injectMessage(e1,e2,m) interceptMessage(e1,e2)	send message m to endpoint e2 as if it came from e1 intercept a message from e1 to e2
		startUntrustedApp(h,p)	start a malicious application p at h
		getServerRequest(h,p)	intercept a request between the http module and app p at h
	Websites	sendServerResponse(h,p,u,r,c,m)	send m to u on behalf of h, p, with cookie c and
			HTTP response type r, from the server with principal sp
		httpRequestResponse(c,u,m)	send m to u and wait for response
	JavaScript	getClientResponse(b,h,p) sendClientRequest(b,h,p,c,u1,u2,m)	intercept the response from browser b to app h, p send m to h, p as if b clicked on u1 on a page from u2

Table 2 :

 2 Protocol Models Verified with ProVerif

	Verification Time

  P get params(get e 1 ,get e n ) = query string in if(isset($ POST[e1],..,$ POST[en])) fun P post params(bitstring,..,bitstring):Params [data]. , ..., post e n )) = method in if(get table(T, $vi,.., &$wj , ..)i,j ) get T(var v i , ..., =var w j , ...) in if(sscanf(s, T, &$e1,..,&$en)==n)

	Source	Translation
		fun dataConst T(bitstring,...,bitstring):bitstring [data].
	echo sprintf(T, e1, . . . , en)	out(httpServerResponse, (url,httpOk( dataConst T( e 1 , . . . , e n )
		),cookie jar, corr));
	die(M)	out(httpServerResponse, (url,httpError(),cookie jar, corr));
		out(httpServerResponse, (url, httpRedirect(
	redirect(e)	parseUri( e )
		)),nullCookie(), corr);
	if(isset($ GET[e1],..,$ GET[en]))	fun P get params(bitstring,..,bitstring):Params [data].
		let httpPost(P post params(
		post e 1

let

Table 3 :

 3 Overview of the translation from PHP to ProVerif

Table 4 :

 4 Formal Attacks found using ProVerif

	New Token Redirection Attacks	Unauthorized Cross Social-Network	Login Request Forgery	Yes	Yes	Yes	Yes							Yes	Yes
		Resource	Theft		Yes	Yes	Yes			Yes		Yes
	New Social CSRF Attacks	Login Sharing Automatic	CSRF CSRF Login		Yes		Yes Yes	Yes Yes Yes	Yes Yes Yes	Yes Yes	Yes Yes	Yes	Yes Yes
	Preexisting Vulnerabilities	Form Token Login	CSRF Redirector CSRF	Yes		Yes	Yes	Yes Yes	Yes Yes		Yes		Yes
	Role(s)			AS, RS	AS, RS	Client	Client	Client	Client	Client	Client	Client	Client	Client lib	Client lib
	Website			Twitter	Facebook	Yahoo	WordPress	CitySearch	IndiaTimes	Bitly	IMDB	Posterous	Shopbot	JanRain	GigYa

Table 5 :

 5 Concrete OAuth Website Attacks derived from ProVerif Traces

RR n°8287

Personal communication with the authors of[START_REF] Lei | AUTHSCAN: Automatic extraction of web authentication protocols from implementations[END_REF], 28/2/2013.RR n°8287

InriaRESEARCH CENTRE PARIS -ROCQUENCOURTDomaine de Voluceau, -Rocquencourt B.P. 105 -78153 Le Chesnay Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Syntax of Target PHP Subset

The syntax of the PHP subset that we translate to ProVerif is given below. Roughly speaking, a program written in that subset looks like a binary tree of if statements, whose leaves are either echo, die or redirect statements (similar to how WebSpi's application processes can return httpOk, httpError or httpRedirect).

program ::= '<?' ('require' @string';')* statement

There are four kinds of if statements: normal conditions, parameter checking with isset, database lookups with the library function get table and template parsing with sscanf. There is no support for functions, objects, arrays (besides those containing input parameters) or any kind of loop; while very limited compared to normal PHP, this subset is still expressive enough to build meaningful applications, provided operations that require actual computation (such as cryptographic primitives) are treated as calls to functions defined either in PHP's standard library or in an included file.

To demonstrate its usefulness, we implemented an example login provider for OAuth's implicit mode in this subset. The source code of the authorization handler is given in Table 7.

Translating PHP into ProVerif

At a high level, we require each PHP script to handle a single query path, for instance, login.php is translated into the process LoginServerApp, with a path constructor loginPath (corresponding to queries to /login.php). Before any other operation, the host and path of the script must be matched against incoming requests. Thus, a server process starts with the following preamble, which also introduces free names (headers, method, protocol, query string, cookie jar) required for the translation: