Abstract: 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:
| • | The status of analysis in OAuth 2.0 protocol including in symbolic model and in computational model is presented. The related references show that OAuth 2.0 protocol has been analyzed with informal method, or with symbolic method, or with computational model by hand. Until now there does not existing that analysis security of OAuth 2.0 protocol with automatic tool in computational model |
| • | Applying Blanchet calculus in computational model with active adversary for automatic analysis of OAuth 2.0 protocol. So the term, process and correspondence assertion in Blanchet calculus are used to model authentication in OAuth 2.0 protocol. The authentication is expressed by non-injective or injective correspondence. The analysis itself is executed by automatic tool CryptoVerif developed by Blanchet. Figure 1 shows the model of automatic verification of OAuth 2.0 protocol |
| • | The result shows 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 |
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[M1,…,Mm] returns the content of the cell of indices M1,…,Mm of the m-dimensional array variable x. The function application f(M1,…,Mm) returns the result of applying function f to M1,…,Mm. 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[M1, L, Ml].
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
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:
| • | Firstly, verification of identifier of the client is executed. The authorization server mainly verifies the value of the parameters client_id and client_secret. If the result failed, then the authorization server sends the response error message to the client |
| • | Secondly, verification of code is run. The authorization server checks whether the value of the parameter grant_type does match the value of the parameter authorization_code. At the same time he also checks the value of code is valid and the parameters of code and client_id are consistent |
| • | Finally verification of redirect_uri is executed. The authorization server need to verify that whether the value of the parameter redirect_uri is valid or not. At the same time he also checks that whether the value of the parameter redirect_uri does match the value of the parameter redirect_uri in authorization request or not. If the two verifications failed, then authorization server sends the response error message to the client |
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. !n1client 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
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
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
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
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
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.