Automatic Verification of Security Properties of OAuth 2.0 Protocol with Cryptoverif in Computational Model

During the past several years, OAuth 2.0 protocol has been widely implemented and deployed. In order to give a strong confidence in its security to the people, in this study, Blanchet calculus in computational model is used to analyze OAuth 2.0 protocol with mechanized tool CryptoVerif. The term, process and correspondence are used to model OAuth 2.0 protocol . The authentication is formalized by non-injective or injective correspondence. The results show that OAuth 2.0 protocol has not authentication between the resource owner and authorization server, authentication between client and authorization server. The first automatic analysis on OAuth 2.0 protocol in computational model of in active adversary is implemented in this study.

INTRODUCTION

With the development of Internet technology and cloud computation, Internet has a strong influence on the life of people. Thus many transactions need the cooperation among the different system and websites. So there is an urgent requirement for accessing the data and services on the different and close websites. OAuth 2.0 protocol (http://tools.ietf.org/html/draft-ietf-oauth-v2-11) is proposed to address the problem. OAuth 2.0 protocol bas been implemented and deployed by Facebook, Twitter, LinkedIn, Google, Yahoo, .Sina, QQ, Renren and others. OAuth 2.0 protocol which is authentication and authorization protocol allows the third party to access to the protected resource which are require authentication using the related secure technologies, for example, authentication based on username and password. Although, OAuth 2.0 protocol is viewed as an authorization protocol, OAuth 2.0 protocol is being used for social login and hence for authentication between the resource owner and authorization server, authentication between client and authorization server.

In order to verify the security properties of security protocols including OAuth 2.0 protocol and enhance the confidence of the people, two models have been developed for analyzing security protocols form the beginning of the 1980s (Meng, 2011; Meng and Shao, 2010), symbolic model and computational model. In symbolic model cryptographic primitives are abstracted as black boxes and lots of mechanized tools have been implemented, for example, SMV, NRL, Isabelle, Athena, Revere, SPIN, Brutus, ProVerif and AVISPA. However, the results of analysis in this model are not quite clear.

The other model is computational model that bases issues of complexity and probability. This model uses a strong notion of security, against all probabilistic polynomial-time attacks. Chari et al. (2011) use universally composable security to formalize by hand the authorization code mode of the OAuth 2.0 protocol. The result of analysis in computation model is quite realistic; however it is a hard problem to develop an mechanized tool. The introduction of mechanized tool CryptoVerif (Blanchet, 2008) is the first automatic tool with computational model developed by Blanchet. At the same time, it does not existing that analysis security of OAuth 2.0 protocol with automatic tool in computational model.

Owning to the previous analysis of OAuth 2.0 protocol is not quite clear, in this study, Blanchet calculus in the computational is used to model to analyze OAuth 2.0 protocol with mechanized tool CryptoVerif.

CONTRIBUTION AND OVERVIEW

During the past several years OAuth 2.0 protocol bas been implemented and deployed by Facebook, Twitter, LinkedIn, Google, Yahoo,. Sina. QQ. Renren and others.

In order to verify the security properties of security protocol and improve the confidence of the people, symbolic model and computation model have been developed form the beginning of the 1980s. Computational model bases on complexity and probability. At the same time computational model uses a strong notion of security, guaranteed against all probabilistic polynomial-time attacks and is more realistic. The related references show that the Security properties of OAuth 2.0 protocol have been analyzed with informal method, or with symbolic method, or with computational model by hand which depends on experts’ knowledge and ability and is prone to make mistakes. Until now there does not exist that security analysis of OAuth 2.0 protocol with mechanized tool in computational model.

So analysis of security properties of OAuth 2.0 protocol with automatic tool in computational model plays an important role in security protocol field and is a significant work. Hence, in this study, Blanchet calculus in the computational is used to analyze OAuth 2.0 protocol with mechanized tool CryptoVerif.

The main contributions of this study are summarized as follows detail:

RELATED WORK

Here, the status of OAuth 2.0 protocol and its proof in symbolic model and in computational model are discussed. The related references show that security properties of OAuth 2.0 protocol are analyzed with informal method, or with symbolic method, or with computational model by hand. There does not existing that analysis of OAuth 2.0 protocol with automatic tool in computational model.

Chari et al. (2011) use universally composable security framework to formalize by hand the authorization code mode in OAuth2.0 protocol. They propose an ideal functionality for delegation of web access to a third-party where the authentication scheme is based on password. Corella and Lewison (2011) give an informal security analysis of OAuth 2.0 protocol by hand. They mainly focus on denial of service attacks on OAuth 2.0 protocol. Shi et al. (2012) introduce the principle of OAuth 2.0 protocol and analyze the procedure of refresh token and propose a framework of OAuth2.0 server objected to specific application. But they do not analyze its security properties.

REVIEW OF BLANCHET CALCULUS

Here, Blanchet calculus (Blanchet, 2008) is reviewed. Blanchet calculus is a probabilistic polynomial calculus and has been carefully designed to make the automated proof security protocols.

Fig. 1:	Model of automatic verification of OAuth 2.0 protocol

In this calculus, messages are bitstrings and cryptographic primitives are functions operating on bitstrings. Blanchet calculus includes terms and processes. Next the notations used in Blanchet calculus are discussed.

In Blanchet calculus c denote a countable set of channel names. The variable access x[M₁,…,M_m] returns the content of the cell of indices M₁,…,M_m of the m-dimensional array variable x. The function application f(M₁,…,M_m) returns the result of applying function f to M₁,…,M_m. Using different channels for each input and output allows the adversary to control the network. The find construct allows us to access arrays.

Process includes two types of processes: Input processes Q ready to receive a message on a channel; output processes P which output a message on a channel after executing some internal computations. The input process include processes nil 0, parallel composition Q|Q’, replication times !^I≤nQ, channel restriction new channel c; or Q input c[M₁, L, M_l]. The input process 0 does nothing; Q|Q’ is the parallel composition of Q and Q’; !^i≤nQ represents n copies of Q in parallel, each with a different value of iε[1, n]; new channel c; Q creates a new private channel n and executes Q. The output process include processes , random number new x[i₁,…i_m]: T; P, assignment let x[i₁,…i_m]: T = M in P, conditional if defined (M₁,…M_l)∧M then P else P’, event event e(M₁,…M_m); P, array lookup find such that defined then P_j), new x[i_i,…i_m]: T; P chooses a new random number uniformly in I_n(T), stores it in x[i_i,…i_m] and executes P. let x[i_i,…i_m]: T = M in P stores the bitstring value of M in x[i_i,…i_m] and executes P. find suchthat defined then P_i) else P means that it tries to find a branch J in [1, m] such that there are values of for which M_ji,…M_jlj are defined and M_i is true. In case of success, it executes P. In case of failure for all branches; it executes P. The formula event e(M₁,…M_m) holds when the event e(M₁,…M_m) has been executed.

MECHANIZED PROOF TOOL CRYPTOVERIF

This section presents a brief overview of the mechanized prover CryptoVerif, formalize OAuth 2.0 protocol using it (http://www.cryptoverif.ens.fr). In most cases, the prover succeeds in proving the desired properties when they hold and obviously it always fails to prove them when they do not hold. In other words CryptoVerif is sound but not complete which means that it cannot prove are not necessarily invalid.

The mechanized prover CryptoVerif can directly prove security properties of cryptographic protocols in the computational model in which the cryptographic primitives are functions on bit-strings and the adversary is a polynomial-time Turing machine. It also can prove secrecy properties and events that can be executed only with negligible probability. CryptoVerif runs either automatically or interactively, in which case it receives guidance from the user for selecting transformations.

Authentication is modeled as correspondences, much as in symbolic models. Computationally, correspondences assert that, if some event is executed, then other events must also have been executed, at least once, with matching parameters, at least with overwhelming probability. CryptoVerif can deal with more general properties expressed as logical formulas; also both injective and non-injective properties can be analyzed. A non-injective correspondence is a property of the form “if some events have been executed, then some other events have been executed at least once”. Injective correspondences are properties of the form “if some event has been executed n times, then some other events have been executed at least n times”. Injective correspondences are more difficult to check than non-injective ones, because they require distinguishing between several executions of the same event.

CryptoVerif operates in two modes: a fully automatic and an interactive mode. The interactive mode which is best suited for protocols using asymmetric cryptographic primitives, requires a CryptoVerif user to input commands that indicate the main game transformations the tool should perform. CryptoVerif is sound with respect to the security properties it shows in a proof but properties it cannot prove are not necessarily invalid.

REVIEW OF OAUTH 2.0 PROTOCOL

OAuth 2.0 protocol is used to access a protected resource for clients in the name of a resource owner. OAuth 2.0 protocol includes four roles: protected resource, resource server and client and resource owner. Before a client want to access a protected resource, it must first receive authorization, for example, access token, from the resource owner, then get the access token with the access grant. Finally the client accesses the protected resource by sending the access token to the resource server. Clients in OAuth 2.0 protocol can be fall into four categories: web server, user-agent and native application and autonomous. Here the analysis mainly focus on the web server-based client. At the same time the access grant type is authorization code.

Figure 2 describes the procedure of the abstracted flow in OAuth protocol and is the authorization code mode of the OAuth 2.0 protocol where the authentication scheme is based on password and the client profile is web server.

Fig. 2:	Procedure of the abstracted flow in OAuth 2.0 protocol

First the end-user must be authenticated with username and password of end-user by authorization server. At the same time the client also must be authenticated with the information mainly including client type and redirect_uri by authorization server. Authorization server gets the authorization request and then generates client_id and client_secret which is used to authenticate the identity of client.

End-user registration request: End-user registers to authorization server with his username and password. So End-user generates message (1) including his username and password and deliver it to authorization server. Thus the procedure of registration is completed.

Client authorization request: If client wants to request the resource of the protect resource owner in resource server, he must generate the message (2) client authorization request which mainly consists of the three parameters: respondence_type, client_id and redirect_uri and send it to authorization server. The parameter response_type which is “required” must be access token “token” or authorization code “code” and “access token and authorization code code_and_token”. The parameter response_type is used to issue the type of authorization response by authorization server. The parameter scope which is “required” is used to describe the scope of the access request and is generated by authorization server. The parameter client_id which is “required”and is used to express the identifier of end-user and is issued by authorization server after end-user has registered to authorization server. The parameter redirect_uri which is “required”and redirect the user-agent to the URI after complete of end-user authorization.

The authorization server validates the (2) client authorization request to make sure that all required parameters are exist and valid. If the request is invalid, the authorization server redirects the user-agent back to the client using the redirection URI provided with the appropriate error code. If the request is valid, the authorization server authenticates identifier of resource owner with the parameters username and password and gets the access grant of end-user. When access grant has been received, the authorization server directs the end-user's user-agent, for example, browser, to the provided client redirection URI with the help of an HTTP redirection response, or other means available to it via the end-user's user-agent.

End-user authentication and authorization request: The authorization server authenticates end-user with message (3) including the parameters username and password of end-user. If the parameters username and password is valid then it issues that the end-user agrees on the access request.

Authorization server authorization response: After authorization server authenticate end-user with the parameters username and password of end-user. Then authorization server generates message (4) authorization response which mainly includes an access token, an authorization code, or both. At the same time it delivers them and the parameters cliend_id and redirect_uri to the client by the redirection URI.

Access token request: The client gets the authorization code from the authorization server, then he can obtain an access token before accessing the protect resource. The access token is generated by authorization server.

The client constructs the following parameters grant_type, code, client_id, client_secret, rdirect_uri and scope to generate the message (5) access token request and deliver to the authorization server. The value of the parameter grant_type must be authorization_code. The value of the parameter code is consisting with to the value of the received code from the authorization response. The value of the parameter client_id and redirect_uri is same to the value of the received client_id and redirect_uri in authorization request. At the same time the value of the parameter client_secret is same to the value of the received client_id in authorization server generated.

When the authorization server receives the access toke request he must finish the following verifications:

If the previous three verifications all succeed then the authorization server generates the access token response message (6).

Access token response: If the access token request from client is valid and verified by authorization server, then he creates the access token response message (6) mainly including the parameters access_token, token_type, expires_in, refresh_token, scope and so on. At the same time those parameters are put into the JSON structures and are sent to the client by HTTP protocol. The value of the parameter access_token which is “required” and is access token which is used to access the protect resource from the resource owner. The value of parameter token_type which is “required” and is used to describe the type of access_token. The value of the parameter expires_in which is “optional “and depicts the duration in seconds of the access token lifetime. The parameter scope which is “required” is used to describe the scope of the access request and is generated by authorization server. The value of the parameter refresh_token which is “optional” and is used to obtain a new access tokens based on the same end-user access grant. The authorization server should not issue a refresh token when the access grant type is an assertion or a set of client credentials. The client accesses protected resources through presenting an access token to the resource server. The resource server must verify the access token and ensure it has not expired and that its scope covers the requested resource.

FORMALIZING OAUTH 2.0 PROTOCOL IN BLANCHET CALCULUS

Here, we use non-injective correspondences and Injective correspondences to model authentication from authorization server to end-user and from authorization server to client. First non-injective correspondences are used: event event authorization (x) ==> user (x) is used to authenticate end-user by authorization server. Event event authorization (x) ==> client (x) is used to authenticate client by authentication server. Injective correspondences are then used: event event inj: authorization (x) ==> inj: user (x) is used to authenticate end-user by authorization server. Event event inj: authorization (x) ==> inj: client (x) is used to authenticate client by authentication server. Figure 3 describes the events and correspondence.

The complete formal model of OAuth 2.0 protocol in Blanchet calculus is given in figures. Figure 4-8 report the basic process include authorization_server process, client process, web_server process and end_user process in authentication forming the model of OAuth 2.0 protocol. The process EPP of 3 KP process in Fig. 4 is assumed to run in interaction with an adversary which also models the network.

Fig. 3:	Query events

In (atart ( )) means that the protocol is executed. The authorization server is formalized as authorization_server process. Client process is modeled as client process. Web server process is formalized as web_server process. End-user is modeled as end_user process. !ⁿ¹client process means n client process parallels run.

End-user is modeled as End-user process in Fig. 5. End-user process first chooses randomly with uniform probability a bitstring name in the type user name by the construct new name: user name. At the same time it then chooses randomly with uniform probability a bitstring pass in the type password by the construct new pass: password. After that end-user sends the name and pass through the channel c1 by the construct . Then End-user process receives message string_from_author in the type bistring from the channel c2 by the construct c2(string_from_author.bistring). If the message string_from_author is error, then it outputs null message, otherwise the event event user(name) is executed. Finally End-user process outputs message (A, name, pass) by the construct and it ends.

Client process is formalized as client process in Fig. 6. Client process first receives information from the channel c by the construct c( ) and then he chooses randomly with uniform probability a bitstring uri in the type redirect_uri by the construct new uri:redirect_uri.

Fig. 4:	OAuth 2.0 protocol process

Fig. 5:	End-user process

Fig. 6:	Client process

Fig. 7:	Web server process

Fig. 8:	Authorization server process

After that he outputs the parameter uri through the channel c4 by the construct . Client process receives information clientid_:client_id, client secret_: client secret through the channel c5 by the construct c5(clientid_:client_id, client secret_: client secret) and chooses randomly with uniform probability a bitstring response type in the type response_type by the construct new response type: response_type. After that Client process send authorization request response type, clientid_,uri through the channel c6 by the construct . If the authorization server has successfully verify the authorization request then he sends the an authorization code code_from_web to the Web server process. After that the web server process sends it to Client process. Thus the Client process receives the authorization code code_from_web through the channel c7 by the construct c7(code_from_web:code). At the same time the event event client (code_from_web) is executed. Client process chooses randomly with uniform probability a bitstring grant type in the type grant_type by the construct new granttype_grant type. Thus he constructs access token request message granttype, code_from_web, cliented_, clientsecret_, uri and sends it to the Authorization server process through the channel c8 by the construct 〈granttype, code_from_web, cliented_clientsecret_, uri〉. Client process receives the access token accesstoken: access_token, tokentype_from_a: token_type through the channel c9 by the construct c9(access token accesstoken: access_token, tokentype_from_a: token_type).

Web server process is modeled as web_server process in Fig. 7. Web server process receives the authorization request response: respose_type, cliented_from_c: client_id, uri_from_c: redirect_uri through the channel c10 by the construct c10(response: respose_type, cliented_from_c: client_id, uri_from_c: redirect_uri). After that web server process delivers the authorization request web, response, cliented_from_c, uri_from_c through the channel c11 by the construct 〈web, response, cliented_from_c, uri_from_c〉 to authorization server. At the same time web server process receives the authorization code code_from_a from the channel c12 by the construct c12(=web, code_from_a: code) then delivers it to the client process through the channel c13 by the construct .

Authorization server process is formalized as authorization_server process in Fig. 8. In the model the resource owner first registers to authorization server. Authorization server receives the username and password information of resource owner name_reg:username, password_reg: password through the channel c14 by the construct c14(name_reg:username, password_reg: password). And then it uses the construct find I<=N such that defind (name_reg_success [I])&&(name_reg_ success [i] = name_reg) to verify the identity of resource owner. If the verification fails then it sends error message, otherwise it stores username and password of resource owner using the constructs let name_reg_success: username = name_reg in and let password_reg_success: password = password_reg in. At the same time authorization server binds the username name_reg_ success and password password_reg_success using the construct contactA(name_reg_success, password_reg_ success) and stores it as name_password_success. At the same time authorization server also receives the application of client process uri_reg:redirect_uri through the channel c15 by the construct c15(uri_reg:redirect_uri). And then uses the construct find j<=N such that defined (uri_reg_success[j])&&(uri_reg_success [j] = uri_reg) to verify the identity of client. If the verification fails then it sends the error message, otherwise it generates the identity clientid and secret key clientsecret of client by the constructs new clientid:client_id and new clientsecret: client_secret. Then authorization server process binds the identity clientid and secret key clientsecret of client using the construct contact B(clientid,clientsecret). At the same time authorization server process binds the client identifier clientid and URI uri_reg_success using the construct contact C(clientid, uri_reg_success). And then authorization server delivers the client identification clientid and client secret key clientsecret through the channel c16 by the construct to the client process.

Authorization server receives the authorization request information responseone_one:response_type, clientid_one:client_id, uri_one: redirect_uri through the channel c17 by the construct c17 (=web,responsetype_ one:response_type,clientid_one:clientid_id, uri_one: redirect_uri) from the web server process. And then it verifies the authorization request information. If the verification is successful, then it sends authentication_ message through the channel c18 by the construct 〈 authentication_message〉 to the resource owner. Authorization server first authenticates the identity of resource owner and then allows it to generate authorization code. The authorization server receives the identification information name_author:username, password_author:password through the channel c19 by the construct c19(=A,name_author.username,password_ author:password). Then authorization server uses the construct find k<=N such that defined (name_password_ success[k])&&(name_password_success[k] = contactA (name_author,password_author)) to check the identification of resource owner. If the verification is successful, then authorization server uses the construct find p<=N such that defined (name_reg_success[p])&& (name_reg_success[p]=name_author) to check the username of resource owner. If the verification is ok, then the event event authorization (name_author) is executed. Authorization server binds client identifier clientid_one and redirect identifier uri_one using the function contact C (clientid_one, uri_one) and stores it in id_uri_one. Then authorization server use the construct find 1<=N such that defined (id_uri_success[1])&&(id_uri_success[1]= id_uri_one) to check the valid of id_uri_one and clientid_one. If the verification succeeds then it generates the authorization code author_code by the construct new author_code:code. After that authorization server uses contact D(clientid_one, author_code) to bind clientid_one and author_code and stores it as id_code_one:bistring. And then authorization server delivers web,author_code through the channel c20 by the construct 〈web, author_code 〉to web server process. The authorization server receives the authorization request information granttype_two: grant_type, code_for_author_two:code, clientid_two:client_id,clientsecret_two:client_secret, uri_two,redirect_uri through channel c21 by the construct c21(granttype_two: grant_type, code_for_author_two: code,clientid_two:client_id,clientsecret_two:client_secret, uri_two,redirect_uri). Authorization server first checks whether code_grant is equal to value of granttype_two or not. If the verification succeeds, it uses the construct find m<=N such that defined (author_code[m])&&(author_ code[m]=code_for_author_two) to check the valid of authorization code code_for_author_two. If the verification succeeds and then it uses the construct find x<=N suchthat defined (id_secret_success[x])&& (id_secret_success[x]=contactB(clientid_two,client secret_two)) to verify the valid of cliented_two and cliented_one. If the verification is successful and then it uses the construct find y<=N suchthat defined (id_uri_one[y])&&(id_uri_one[y]=contactC(clientid_two, uri_two)) to verify the match of clientid_two and clientid_one and the match of uri_two and uri_one. Finally authorization server uses the construct find z<=N suchthat defined (id_code_one[z])&&(id_code_ one[z]=contactD(clientid_two, code_for_author_two)) to verify the match of (clientid_two,code_for_author_two) and (author_code,id_code_one) .If all previous verifications succeeds, then the event event authorization (code_for_author_two) is executed and authorization generates the access token token by the construct new token: access_token and the token type tokentype by the construct new tokentype:token_type. Finally the authorization server deliver the token,token_type through the channel c22 by the construct 〈 token,token_type 〉 to client process.

AUTOMATIC VERIFICATION OF AUTHENTICATION IN OAUTH 2.0 PROTOCOL WITH CRYPTOVERIF

CryptoVerif can take two formats as input: channels Front-end and oracles Front-end. In both cases, the output of the system is essentially the same. The main difference between the two front-ends is that the oracles front-end uses oracles while the channels front-end uses channels. In the channels front-end, channels must be declared by a channel declaration. There is no such declaration in the oracles front-end. Some constructs use a different syntax in the oracles front-end, to be closer to the syntax of cryptographic games.

In this study the form of channels Front-end is used as the input of CryptoVerif. In order to prove the in OAuth2.0 protocol the Blanchet calculus model are needed to be translated into the syntax of CryptoVerif and generated the CryptoVerif inputs in the form of channels Front-end.

Here, non-injective correspondences and Injective correspondences in Table 1 are used to model the authentication from authorization server to end-user and from authorization server to client. First non-injective correspondences are used: event event authorization (x)==>user(x) is used to authenticate end-user by authorization server. Event event authorizationa(x)==> client(x) is used to authenticate client by authentication server. Injective correspondences are then used: event event inj:authorization(x)==>inj:user(x) is used to authenticate end-user by authorization server. Event event inj:authorization(x)==>inj:client(x) is used to authenticate client by authentication server.

Figure 9 and 10 present the code of verification of authentication in CryptoVerif. The analysis was performed by CryptoVerif and succeeded. Table 2 presents the transforms of games in mechanized proof of OAuth 2.0 protocol.

Table 1:	Correspondences in OAuth 2.0 protocol

Table 2:	Transforms of games in OAuth 2.0 protocol

Fig. 9:	Code of protocol in Cryptoverif

Fig. 10:	Code of protocol in Cryptoverif

Fig. 11:	Result of OAuth 2.0 protocol in Cryptoverif

The results are showed in Fig. 11 and OAuth 2.0 protocol is proved not to guarantee authentication without secure measurement, for example, SSL protocol, in computation model.

CONCLUSION

During the past several years OAuth 2.0 protocol bas been implemented and deployed in many enterprises. In order to verify the security properties of security protocol including OAuth 2.0 protocol and improve the confidence of the people, two approaches have been developed form the beginning of the 1980s: symbolic model and computational model. Computational model uses a strong notion of security, guaranteed against all probabilistic polynomial-time attacks and is more realistic.

Hence, in this study, in order to improve the confidence of people, Blanchet calculus in the computational model is used to analyze OAuth 2.0 protocol with mechanized tool CryptoVerif. The term, process and correspondence assertion in Blanchet calculus are used to model authentication in OAuth 2.0 protocol. The analysis itself is executed by automatic tool CryptoVerif developed by Blanchet. The result shows that OAuth 2.0 protocol has not authentication between the resource owner and authorization server, authentication between client and authorization server without any other security mechanism. The first automatic analysis on OAuth 2.0 protocol in computational model of in active adversary is implemented in this study.

In the future, it is an interesting work on the verification of the Java implementation of OAuth 2.0 protocol in computational model.

ACKNOWLEDGMENTS

This study was supported in part by Natural Science Foundation of The state Ethnic Affairs Commission of PRC under the grants No: 12ZNZ008, titled “Automatic verification of cryptographic security in security protocol Java code”, conducted in Wuhan, China from 1/1/2013 to 30/12/2013.