基于计算模型的OpenID Connect协议认证性的自动化分析

孟　博，张金丽，鲁金钿

(中南民族大学 计算机科学学院，武汉430074)



基于计算模型的OpenID Connect协议认证性的自动化分析

孟博，张金丽，鲁金钿

(中南民族大学 计算机科学学院，武汉430074)

分析了OpenID Connect协议的消息结构，基于计算模型应用Blanchet演算对OpenID Connect协议进行了形式化建模，应用自动化验证工具CryptoVerif验证了其认证性.结果表明：在OpenID Connect协议中，客户端能够认证终端用户，但是终端用户与授权服务器之间不能相互认证、令牌终端不能认证客户端.为此，给出了OpenID Connect协议中不具有认证性问题的解决方法.

OpenID Connect协议；计算模型；自动化验证；认证性

OpenID Connect[1]是2014年发布的OpenID最新的用户身份认证及分布式身份系统标准，是非常重要的单点登录认证协议标准之一，建立于OAuth2.0[2]协议的基础之上，引入了一个抽象为身份令牌ID Token的身份层，用来将用户的认证信息由OpenID供应商传送到客户端[3].基于OpenID Connect协议，客户端可以直接为用户提供登录服务，而客户端无需在自己的服务器中存储及管理用户密码，从而再也不必担心用户的账户安全.OpenID Connect协议一经推出便获得了雅虎、谷歌、微软及多家其他公司的支持[4]，人们也开始对其安全性进行分析，目前主要集中在实际应用方面，文献[5-8]通过各种不同的分析方式，提出了OpenID Connect协议在实际应用中可能存在307重定向攻击、OpenID供应商混淆客户端攻击、网页仿冒、网络钓鱼攻击等各种不安全因素.

本文对OpenID Connect协议安全性的分析集中在协议本身，基于计算模型[9]对OpenID Connect协议的认证性进行自动化分析.首先分析OpenID Connect协议的消息结构，然后利用Blanchet演算[10]来对OpenID Connect协议进行建模，最后通过自动化验证工具CryptoVerif[11]分析其认证性，并根据认证结果提出了解决问题的建议.

1　OpenID Connect协议的消息结构

OpenID Connect协议身份认证有3种类型：授权码流、隐式流、混合流，本文中对OpenID Connect协议的分析选取的身份认证方式是授权码流认证方式，基于该方式的所有令牌都从令牌终端返回，授权服务器向客户端发送授权码，随后客户端可以利用这个授权码直接从令牌终端获得身份令牌和访问令牌，这样就可以成功地避免将令牌暴露给用户代理或者其他能够访问用户代理的恶意应用程序.采用授权码流认证方式的OpenID Connect协议消息流程如图1所示.

图1　OpenID Connect协议消息结构Fig.1 The structure of message of OpenID Connect Protocol

1.1客户端向授权服务器发送认证请求

如果客户端需要访问受保护的终端用户的资源，就需要向OpenID供应商的授权服务器发送认证请求，认证请求中必须包含域值scope、响应类型参数response_type、客户端标识符client_id、客户端重定向URI redirect_uri和状态参数state.在发送认证请求时，这些参数作为OpenID供应商的重定向URI的数据请求参数，Web浏览器通过HTTP机制重定向到OpenID供应商的授权服务器.OpenID供应商收到客户端的认证请求之后，授权服务器通过核查请求中是否包含必备参数，并且这些参数的用法是否符合协议规范来验证该请求是否有效.如果请求有效，则授权服务器根据请求中使用的参数值来做出响应;否则，授权服务器必须返回一个错误响应.

1.2授权服务器认证终端用户并获得授权

当授权服务器需要认证终端用户并获得授权时，就向终端用户发送请求认证消息Authentication_Message，请求认证资源拥有者的身份.终端用户收到认证请求消息Authentication_Message后，若同意授权，则向授权服务器发送自己的用户名和密码.授权服务器收到该用户名和密码后，与其存储的用户名和密码进行验证，如果验证成功，则表明授权服务器已成功认证终端用户并获得终端用户的授权.

1.3授权服务器响应认证请求

当授权服务器获得终端用户的授权之后，生成授权码code，并将其与认证请求中的客户端标识符和重定向URI进行绑定，然后将产生的授权码code和认证请求中的参数state作为请求参数添加到客户端的重定向URI中，Web浏览器通过HTTP机制重定向到客户端，从而将产生的授权码code发送到客户端.如果终端用户认证失败或者终端用户不同意授权，授权服务器需要通过认证请求中的重定向URI向客户端返回错误提示信息.

1.4客户端发送令牌请求

当客户端获得授权服务器发送的授权码之后，需要向OpenID供应商发送令牌请求，将授权许可类型grant_type(在授权码流中，它的值为“authorization_code”)、授权服务器发送的授权码code、client_id和client_secret、客户端重定向URI redirect_uri一起作为令牌请求参数，添加到OpenID供应商的URI中，发送给OpenID供应商，从而获得已经授权的终端用户的身份令牌和访问令牌.只有获得了访问令牌，客户端才能够访问终端用户的资源.

1.5令牌终端响应令牌请求

OpenID供应商的令牌终端接收到客户端的令牌请求之后，需要验证客户端的身份凭证，确保客户端标识符和密码正确且存在绑定关系；验证授权码是否有效，并且，授权码是否发送给了得到授权的客户端，即授权码与客户端标识符和客户端重定向URI是否存在绑定关系；验证令牌请求中的客户端地址与认证请求中的客户端地址是否相同；验证授权码是用来响应OpenID Connect认证请求而发布的，从而决定令牌终端响应令牌请求时是否需要发送身份令牌.当确认客户端发送的令牌请求有效且该客户端得到了终端用户的授权，OpenID供应商的令牌终端对客户端返回令牌请求响应，即向客户端发送身份令牌id_token、访问令牌access_token、令牌类型参数token_type(值为“Bearer”)、访问令牌的有效期限espires_in及域值scope.身份令牌即ID Token，用来将用户的认证信息从授权服务器发送到客户端.访问令牌即Access Token，客户端可以通过向OpenID供应商的用户信息终端发送访问令牌来访问得到授权的终端用户的资源.

2　应用Blanchet演算对OpenID Connect协议建模

应用Blanchet演算，对OpenID Connect协议进行建模，Blanchet演算可以得到自动化验证工具CryptoVerif的支持.通道是数据传递的重要媒介，所有的数据都是通过通道在不同实体之间进行传输，建模时首先要对通道进行定义.在OpenID Connect协议中，身份令牌ID Token必须通过JWS进行签名，需要引用数字签名技术，这里选用CryptoVerif中预先定义的一个具有较强抵抗选择消息攻击能力的概率公钥签名算法SUF_CMA_signature.

2.1认证性

利用Blanchet演算进行安全协议建模时，首先要对事件进行声明，并给出最终需要证明的目标，这个目标主要是针对不同实体之间的认证性，这里采用非单射一致性来建模认证性，认证性证明目标如表1所示.

表1　认证性目标

2.2主进程process

在OpenID Connect协议建模的主进程process中，首先要利用new语句生成一个keyseed类型随机数signseed，作为数字签名密钥种子，然后将signseed作为函数参数，调用概率公钥签名算法SUF_CMA_signature中的公钥、私钥生成函数pkgen()、skgen()，生成ID Token进行数字签名时所需要的公钥signpkey和私钥signskey，并将signpkey通过通道c发送.最后，采用((!N OP_Process)|(!N1 Client_Process)|(!N2 End_User_Process))这个多个进程并发执行语句模拟OpenID Connect协议执行，其中，OP_Process、Client_Process、End_User_Process进程分别用于模拟OpenID供应商、客户端、终端用户.主进程process建模如下：

process

start(); new signseed:keyseed;

let signpkey:pkey=pkgen(signseed) in

let signskey:skey=skgen(signseed) in

((!N OP_Process)|(!N1 Client_Process)|(!N2 End_User_Process)).

2.3终端用户进程End_User_Process

当终端用户由通道c10接收到来自OpenID供应商的消息string_from_OP后，需要判断消息的具体内容，当消息是请求认证授权ask_for_authentication时，表明OpenID供应商请求认证用户并获得授权.终端用户同意授权，通过通道c11向OpenID供应商发送自己的用户名user_name和密码user_password.终端用户进程End_User_Process建模关键部分如下：

c10 (=OpenIDP_one,string_from_OP:bitstring);

if string_from_OP=ask_for_authentication then

2.4客户端进程Client_Process

当客户端需要访问终端用户的资源时，利用new语句生成返回类型参数responsetype、会话状态参数state_one、openid域值参数scope_one，并将这些参数与客户端标识符id_client和重定向地址uri_client一起，作为认证请求参数通过通道c7发送给OpenID供应商.客户端由通道c14接收到OpenID供应商发送的授权码code_from_OP之后，为了能够访问终端用户的资源，还需要向OpenID供应商发送令牌请求，利用new语句生成许可类型参数granttype_one，并将其与code_from_OP、uri_client、id_client、secret_client一起作为令牌请求参数通过通道c15发送给OpenID供应商.当OpenID供应商成功验证令牌请求参数之后，会向客户端返回身份令牌ID Token和访问令牌Access Token.客户端由通道c17接收签名信息message、签名结果sign_one_s、访问令牌accesstoken_one、访问令牌类型tokentype_one、令牌有效期限expiresin_one等参数，然后通过check()函数验证签名是否有效，并通过let赋值语句获得身份令牌idtoken_one.当客户端获得访问令牌之后，就可以与用户信息终端进行交互，从而访问受保护终端用户的资源.客户端进程Client_Process建模关键部分如下：

new responsetype:response_type;

new state_one:state;new scope_one:scope;

c14(=OpenIDP_two,code_from_OP:code_authorization,state_three:state);

new granttype_one:grant_type;

c18(message:signinput,sign_one_s:signature,accesstoken_one:access_token,tokentype_one:token_type,expiresin_one:expires_in,scope_three:scope);

if check(message,signpkey,sign_one_s) then

let combine5(idtoken_one:id_token)=message.

2.5OpenID供应商进程OP_Process

OpenID供应商由通道c8接收到包含域值scope_two、返回类型responsetype_two、客户端标识符clientid_two、客户端重定向地址uri_two及会话状态参数state_two这些请求参数的认证请求之后，首先利用find语句、combine2()函数来判断clientid_two与uri_two是否存在绑定关系，若存在绑定关系，则确定该认证请求是否由客户端本身发送.在使用授权码流时，responsetype_two值应该为“code”，判断responsetype_two的值是否为“code”，如果满足，授权服务器将认证终端用户，通过通道c9将认证请求消息ask_for_authentication发送给终端用户.授权服务器由通道c12接收终端用户的认证响应，即用户名user和密码pass，通过find语句查询是否存在该user，并且利用combine3()函数判定user与pass是否存在绑定关系.如果这两个条件均满足，则说明终端用户同意授权，授权服务器利用new语句生成授权码auth_code，并通过combine4()函数将auth_code与clientid_two、uri_two进行绑定后存储到clientid_code中.最后，授权服务器将授权码auth_code与状态参数state_two一起通过通道c13发送给客户端，从而完成对客户端认证请求响应.建模部分关键代码如下：

c8(scope_two:scope,responsetype_two:response_type,clientid_two:client_id,uri_two:redirect_uri,state_two:state);

find k<=N suchthat defined

(clientid_client_uri_succ[k])&&(clientid_client_uri_succ[k]=combine2(clientid_two,uri_two)) then

if responsetype_two=code then

c12(=User_one,user:username,pass:password);

若仔细考察杰克·伦敦的其他作品，会发现其中蕴含着大同小异的意识形态立场。以《海狼》(1904)为代表，得出结论：弱者终于战胜了强者，文明终于战胜了野蛮(王宁、张艳红2010：124)。以《白牙》（1906）为代表，白牙的整个成长过程充满痛苦和挫折，最后在人类爱的感召下变成了一只忠实的“狗”,表现出作者强调博爱与毅力对人类发展的重要性(李智2012：208)。

find l<=N suchthat defined (login_username_succ[l])&&(login_username_succ[l]=user) then

find m<=N suchthat defined

(username_password_succ[m])&&(username_password_succ[m]=combine3(user,pass)) then

new auth_code:code_authorization;

let clientid_code:bitstring=combine4(clientid_two,uri_two,auth_code) in

当OpenID供应商的令牌终端由c16接收包含许可类型grant_type_two、授权码code_from_client、客户端重定向地址client_uri_three、客户端标识符clientid_three、客户端登录密码client_secret_three这些参数的令牌请求，首先要判断grant_type_two参数的值是否为“authorization_code”.如果是，判断接收到的client_uri_three与认证请求中的uri_two是否相同，若相同，则表明认证请求与令牌请求来自于同一个用户.然后利用3个find语句验证clientid_three与client_secret_three是否匹配、code_from_client是否存在且与clientid_three、client_uri_three存在绑定关系.若这些验证都成功，令牌终端需要向客户端返回对令牌请求的响应.首先利用new语句生成身份令牌idtoken、访问令牌accesstoken、访问令牌类型tokentype、令牌有效期限expiresin这些必要参数.然后利用new需要生成随机数seed_one，通过combine5()函数将idtoken存储在签名信息signmessage中，并利用签名算法SUF_CMA_signature中的签名函数sign()对其签名，结果存储在sign_one中，然后通过通道c17将signmessage、sign_one、accesstoken、tokentype、expiresin和认证请求中的scope_two一起发送给客户端.此部分建模关键代码如下：

if grant_type_two=authorization_code then

if client_uri_three=uri_two then

find p<=N suchthat defined

(clientid_clientsecret_succ[p])&&(clientid_clientsecret_succ[p]=combine1(clientid_three,client_secret_three)) then

find q<=N suchthat defined (auth_code[q])&&(auth_code[q]=code_from_client) then

find r<=N suchthat defined

(clientid_code[r])&&(clientid_code[r]=combine4(clientid_three,client_uri_three,code_from_client)) then

new idtoken:id_token;

new seed_one:seed;

new accesstoken:access_token;

new tokentype:token_type;

new expiresin:expires_in;

let signmessage:signinput=combine5(idtoken) in

let sign_one:signature=sign(signmessage,signskey,seed_one) in

3　利用CryptoVerif验证OpenID Connect协议的认证性

自动化验证工具CryptoVerif对安全协议的证明依赖于一系列的Game转换[12].将基于Blanchet演算的OpenID Connect协议代码转换成CryptoVerif语法，并添加事件event的声明及事件查询语句，添加方式如下：

event Authentication(bitstring).

event UserAuth(bitstring).

event User(username).

event Authorization(username).

event client(code_authorization).

event TokenEnd(code_authorization).

event IDTokenEnd(seed).

event IDTokenClient(id_token).

query x:bitstring; event UserAuth(x)⟹

Authentication(x).

query x:username; event Authorization(x)⟹

User(x).

query x:code_authorization; event TokenEnd(x)⟹

client(x).

query x:seed,y:id_token; event IDTokenClient(y)⟹

IDTokenEnd(x).

let Client_Process=

……

new granttype_one:grant_type;

out(c15,(granttype_one,code_from_OP,uri_client,id_client,secret_client));

……

let combine5(idtoken_one:id_token)=message in

let End_User_Process=

……

in(c10,(=OpenIDP_one,string_from_OP:bitstring));

if string_from_OP=ask_for_authentication then

out(c11,(User_one,user_name,user_password)).

let OP_Process=

……

if responsetype_two=code then

out(c9,(OpenIDP_one,ask_for_authentication));

……

find m<=N suchthat defined

(username_password_succ[m])&&(username_password_succ[m]=combine3(user,pass)) then

new auth_code:code_authorization;

……

find r<=N suchthat defined

(clientid_code[r])&&(clientid_code[r]=combine4(clientid_three,client_uri_three,code_from_client)) then

new idtoken:id_token;

……

let sign_one:signature=sign(signmessage,signskey,seed_one) in

out(c17,(signmessage,sign_one,accesstoken,tokentype,expiresin,scope_two)).

process

……

将CryptoVerif语法代码输入自动化验证工具CryptoVerif中，得到OpenID Connect协议模型分析结果如图2、图3、图4、图5所示.

图2　event UserAuth(x)⟹Authentication(x)证明的结果Fig.2　Result of proof event UserAuth(x)⟹Authentication(x)

由图2可知，对一致性关系event UserAuth(x)⟹Authentication(x)的证明结果为RESULT Could not prove event UserAuth(x)⟹Authentication(x)，表明终端用户无法认证授权服务器.经过分析可知，授权服务器向终端用户发送认证请求消息ask_for_authentication时，并没有采用一定的安全策略.为了解决终端用户无法认证授权服务器的问题，授权服务器发送认证请求消息ask_for_authentication时，可以利用其签名私钥对ask_for_authentication进行数字签名.终端用户接收到认证请求消息之后，利用授权服务器的签名公钥验证签名，从而实现对授权服务器的认证.

图3　event Authorization(x)⟹User(x)证明的结果Fig.3　Result of proof event Authorization(x)⟹User(x)

由图3可知，对一致性关系event Authorization(x)⟹User(x)的证明结果为RESULT Could not prove event Authorization(x)⟹User(x)，表明授权服务器无法认证终端用户.经过分析可知，终端用户同意授权，向授权服务器发送用户名和密码时，并没有采用一定的安全策略.为了解决授权服务器无法认证终端用户的问题，终端用户向授权服务器发送用户名user_name和密码user_password时，可以利用其签名私钥对user_name和user_password进行数字签名.授权服务器接收到授权响应之后，利用终端用户的签名公钥验证签名，从而实现对终端用户的认证.

图4　event TokenEnd(x)⟹client(x)证明的结果Fig.4　Result of proof event TokenEnd(x)⟹client(x)

由图4可知，对一致性关系event TokenEnd(x)⟹client(x)的证明结果为RESULT Could not prove event TokenEnd(x)⟹client(x)，表明令牌终端无法认证客户端.经过分析可知，客户端向令牌终端发送令牌请求的过程中，请求参数并没有采用一定的安全策略.为了解决令牌终端无法认证客户端的问题，客户端发送令牌请求时，可以利用其签名私钥对授权码code_from_OP进行数字签名.令牌终端接收到令牌请求之后，利用客户端的签名公钥验证签名，从而实现对客户端的认证.

由图5可知，对一致性关系event IDTokenClient(y)⟹IDTokenEnd(x)的证明结果为All queries proved，表明客户端能够认证令牌终端.分析可知，令牌终端向客户端发送令牌响应时，身份令牌采用令牌终端的私钥进行了JWS签名，接收到身份令牌的客户端必须用令牌终端的公钥解密签名信息，获得身份令牌，所以客户端能够认证令牌终端的身份.

针对不具有认证性的缺陷，提出了相应的解决方法，并采用形式化建模的方式证明了解决方法的可行性和正确性.

图5　event IDTokenClient(y)⟹IDTokenEnd(x)证明的结果Fig.5　Result of proof event IDTokenClient(y)⟹IDTokenEnd(x)

4　结语

为了研究OpenID Connect协议的实体之间是否具有认证性，本文通过对OpenID Connect协议消息流中的数据项进行分析，得到其整体的消息结构，然后利用Blanchet演算对OpenID Connect协议消息流程进行建模，并将建模语句导入自动化验证工具CryptoVerif中进行自动化分析.分析结果表明：OpenID Connect协议中终端用户与授权服务器之间无法相互认证、令牌终端无法认证客户端，但客户端能够认证令牌终端，因为令牌终端向客户端发送令牌响应的过程中采用了数字签名机制，而其他实体之间进行消息传递的时候并没有采取一定的安全策略，并不能保证实体之间的相互认证.在OpenID Connect协议标准中规定，所有与OpenID供应商的通信操作必须建立在TLS机制之上，希望借此来保证安全性.然而，我们考虑的是，启用TLS机制的开销比较大、布署起来比较麻烦，并且在协议中已经存在用于保证实体认证性的数字签名机制.因此，如果要通过数字签名机制来解决协议中不存在认证性的问题，在技术上是可以实现的，本文也给出了相应的解决方案.

[1]Sakimura N, Bradley J, Jones M, et al. OpenID Connect Core 1.0[S/OL]. [2014-11-08]. http://openid.net/specs/openid-connect-core-1_0.html.

[2]Hardt D. The OAuth 2.0 authorization framework[S/OL]. IETF.RFC 6749. [2012-10-15]. http://tools.ietf.org/html/rfc6749.

[3]Siriwardena P. Advanced API security: securing APIs with OAuth 2.0, OpenID Connect, JWS, and JWE[M]. New York: Apress Media, 2014:181-200.

[4]Mladenov V, Mainka C, Krautwald J, et al. On the security of modern Single Sign-On Protocols-OpenID Connect 1.0[J/OL]. [2015-08-18]. http://www.oalib.com/paper/4051037#.Vx8yGtJAUzA.

[5]Fett D, Küsters R, Schmitz G. A comprehensive formal security analysis of OAuth 2.0[J/OL]. [2016-01-07]. http://arxiv.org/abs/1601.01229.

[6]Li W P, Mitchell C J. Addressing threats to real-world identity management systems[C]//Reimer H,Pohlmann N,Schneider W. ISSE 2015: Highlights of the Information Security Solutions Europe 2015 Conference. Berlin: Springer Vieweg, 2015: 251-259.

[7]Mainka C,Mladenov V,Schwenk J. On the security of modern Single Sign-On Protocols-Second-Order Vulnerabilities in OpenID Connect[J/OL].[2016-01-07]. http://arxiv.org/abs/1508.04324.

[8]Li W P, Mitchell C J. Analysing the security of Google′s implementation of OpenID Connect[J/OL]. [2015-08-07]. http://arxiv.org/abs/1508.01707.

[9]薛锐, 雷新锋. 安全协议:信息安全保障的灵魂-安全协议分析研究现状与发展趋势[J]. 中国科学院院刊, 2011, 26(3):287-296.

[10]孟博, 王德军. 安全远程网络投票协议[M]. 北京：科学出版社，2013: 238-281.

[11]Blanchet B. A computationally sound mechanized prover for security protocols[J]. IEEE Transactions on Dependable & Secure Computing, 2007,5(4):193-207.

[12]邵飞．基于概率进程演算的安全协议自动化分析技术研究[D]. 武汉：中南民族大学，2011.

Automatic Analysis of Authentication of OpenID Connect Protocol Based on the Computational Model

MengBo,ZhangJinli,LuJintian

(College of Computer Science, South-Central University for Nationalities, Wuhan 430074, China)

In this paper, we get the message term of OpenID Connect by analyzing its authentication message flow, model it with Blanchet calculus in computational model, and use the automatic verification tool CryptoVerif to analyze its authentication. The result shows that, in OpenID Connect protocol, Client can authenticate Token Endpoint, while there is no authentication between the End-User and Authorization Server, and Token Endpoint can′t authenticate Client. Finally, the solutions for the problem of no authentication in OpenID Connect protocol are presented.

OpenID Connect protocol; computational model; automatic verification; authentication

2016-04-06

孟博(1974-)，男，教授，博士后，研究方向：网络空间安全，E-mail: mengscuec@gmail.com

湖北省自然科学基金资助项目(2014CFB249)

TP309

A

1672-4321(2016)03-0123-07