身份认证[1]是网络空间安全[2]的一个重要研究领域，目前提出了OpenID Connect[3]、OAuth2.0[4]、OpenID[5]、CardSpace等安全身份认证协议，其中OpenID Connect是2014年发布的OpenID最新的用户身份认证及分布式身份系统标准，是非常重要的单点登录[6]认证协议标准之一，它已经被Google和Microsoft等互联网企业广泛应用，故其安全性受到人们的重点关注。Li等[7]发现并公布了该协议的诸多漏洞，攻击者能利用这些漏洞登录到OpenID Connect协议Relay Part的网站上，从而使整个系统面临被攻击的危险。Zhang等[8]使用基于计算模型的CryptoVerif对OpenID Connect协议进行形式化建模分析，结果表明该协议的认证性不完整和用户口令秘密性[9]不强。为此本文引入数字签名[10]及非对称加密技术[11-12]，对OpenID Connect协议进行改进，并在符号模型下，应用基于符号模型的安全协议分析工具ProVerif[13]对改进的OpenID Connect协议进行形式化建模分析[14]，结果表明改进后的协议具有认证性和秘密性。
1 改进的OpenID Connect协议改进的OpenID Connect协议同样定义了三个角色，分别是终端用户 (End User，EU)、OpenID服务提供方 (OpenID Provider，OP) 及OpenID依赖方 (Relay Part，RP)，其中OpenID服务提供方又包含令牌端点 (Token Endpoint)、授权服务器 (Authentication Server) 及用户信息端点，令牌端点主要负责生成和发送Token，授权服务器主要负责对认证请求作出响应并授权，用户信息端点主要存储用户在OpenID提供方注册时留下的个人相关信息，在通常应用场景中，RP是客户端，EU是用户个人，OP是OpenID服务提供者。改进的OpenID Connect协议的消息结构如图 1所示。
|
图 1 改进的OpenID Connect协议消息结构 Figure 1 Procedure of modified OpenID Connect protocol |
为访问EU存储在OP上受保护的资源，RP向OP发送一个身份认证请求消息 (1) Authentication Resquest，该消息包含5个主要参数，分别是客户端id (client_id)、授权方式的响应类型 (response_type)、访问域值 (scope)、重定向地址 (redirect_uri) 及请求和反馈之间的状态值 (state)，当协议使用混合流的方式进行身份认证时，response_type的值是code_ id_token。RP对这些参数进行数字签名后通过消息 (1) 发送给授权服务器。
1.2 认证EU请求当授权服务器收到消息 (1) 后，首先验证该消息的数字签名，若验证成功，则根据OAuth2.0的参数确认规则来确认所有参数的完整性和用法是否符合法。若参数合法，授权服务器就产生认证EU的请求消息 (2) Authenticate End_user，该消息包含认证参数ask_authentication，授权服务器对该参数签名后通过消息 (2) 发送给EU。若验签失败，则授权服务器返回一个验签失败消息给RP。
1.3 OP获得授权当EU收到消息 (2) 后，首先验证消息 (2) 的数字签名：验签成功，则对其参数进行确认；若验签失败，则EU返回一个验签失败消息给授权服务器。如果EU同意授权给授权服务器，它会产生授权消息 (3) End_user grant，该消息主要包含之前EU在OP端注册时的用户名 (username) 和用户口令 (password)。首先，EU对用户口令用OP的公钥PU (keyop1) 通过函数aenc (x, PU) 加密得到密文encP; 然后将密文encP和username经过数字签名后通过消息 (3) 发送给授权服务器。在改进的OpenID Connect协议中，参数password由主进程通过隐私信道c1分别发送给EU和OP。
1.4 认证响应当授权服务器收到消息 (3) 后，首先验证消息 (3) 的数字签名，验证成功后再根据得到的密文encp1用自己的私钥PR (keyop1) 通过函数adec (x, PR) 解密密文encp1，检查解密得到的口令明文是否与注册时的password一致，若一致，则说明EU用户同意授权，那么授权服务器产生包含授权码code及身份令牌id_token的认证响应消息 (4) Authentication Response，授权服务器再通过数字签名对这两个参数进行签名后通过消息 (4) 发送给RP。若验签失败，则授权服务器返回验签失败消息给EU。
1.5 令牌请求当RP收到消息 (4) 后，首先验证这个消息的数字签名，检查授权码code是否正确且未使用过，若验证成功，则产生令牌请求消息 (5) Token Resquest，该消息主要包含参数grant_type、客户id (client_id)、重定向地址redirect_uri、RP与OP共享的密钥client_secret，其中grant_type的值为code，这表明RP需要用授权码code在令牌端点换取访问令牌access_token，client_id与消息 (1) 的clien_id一致。最后RP将这些参数进行签名再通过消息 (5) 发送给令牌端点。若验签失败，RP则返回一个验签失败消息给授权服务器。
1.6 令牌响应当令牌端点收到消息 (5) 后，首先验证该消息的数字签名，检查授权类型grant_type和授权码code的值，验签成功后产生令牌响应消息 (6) Token Response，该消息主要包含参数access_token、令牌类型token_type、身份令牌id_token及access_token的生命周期expiress_in，其中id_token与消息 (4) 中的id_token保持一致，token_type值为Bear。若验签失败，则令牌端点返回一个验签失败消息给RP。然后令牌端点对这些参数进行数字签名后通过消息 (6) 发送给RP。RP收到令牌消息 (6) 后，首先验证该消息的数字签名：若验证结果为真，协议通信到此结束；否则RP返回一个验签失败消息给令牌端点。
2 形式化建模改进的OpenID Connect协议应用PI演算是Abadi等[15]在2001年提出来的，它是用来形式化建模并发进程之间相互通信的形式化语言，它在PI演算的通信与并发结构的基础上，增加了函数和等式原语。消息不仅可以包含名，还可以是通过函数和名构成的值。应用PI演算使用函数来表示通用的密码学原语[16]，如加密、解密、数字签名等，不需要为每一个密码操作都构造新的密码学原语，具有很好的通用性，因此可以建模和分析非常复杂的安全协议。
ProVerif是Blanchet于2001年开发的基于重写逼近法的一阶定理证明器，可以用来分析与验证使用Horn子句或者应用PI演算描述的安全协议，可以建模各种密码学原语：包括共享密钥密码学、公钥密钥密码学、数字签名、哈希函数以及Diffie-Hellman[17]密钥交换等。同时它克服了模型检测方法固有的缺陷——状态空间爆炸问题，能够处理无穷状态系统。它能够分析与验证保密性、认证性、更一般的一致性、强保密性和进程的观察等价。ProVerif已经成功分析了大量的复杂的安全协议。
2.1 函数与等式理论本文使用应用PI演算来建模改进的OpenID Connect协议，下面描述了改进的OpenID Connect协议的函数及等式理论。
fun sign (x, PR)
fun aenc (x, PU)
fun adec (x, PR)
fun versign (x, PU)
fun PR (b)
fun PU (b)
(*Digital signature*)
equation versign (sign (x, PR (y)), PU (y))=x
(*public key encryption*)
equation adec (aenc (x, PU (y)), PR (y))=x
进程用私钥PR通过函数fun sign (x, PR) 来签名消息x，用公钥PU通过函数fun versign (x, PU) 来验证数字签名消息x。用公钥PU通过函数fun aenc (x, PU) 来加密消息x，用私钥PR通过函数fun adec (x, PR) 解密消息x。通过函数fun PR (b) 接收私有值b作为输入并产生私钥作为输出，同理通过函数fun PU (b) 接收共有值b作为输入并产生公钥作为输出。
2.2 进程完整的改进的OpenID Connect协议进程主要包含3个进程：OP进程、RP进程及EU进程, 它们共同构成了主进程，如下所示：
OpenID=!processOP|!processRP|!processEU
EU进程的形式化建模如下所示：
processEU= (**Process E_U**)
in (c1, mp); (**E_U recieves password from main process**)
in (c, m2); (**E_U recieves message2 from OP**)
let (ask_authenticatione, signaskm2)=m2 in
if versign (signaskm2, PU (keyop1))=(ask_authenticatione) then
let password=mp in
let encP=aenc ((mp), PU (keyop1)) in
let signgM=sign ((encP, username), PR (keyeu)) in
let authorization = (encP, username, signgM) in
out (c, authorization) (**E_U sends message3 to OP**)
首先, EU通过隐私信道c1接收从主进程发来的password，再通过公开信道c接收OP进程发来的签名消息m2;然后, 用OP的公钥PU (Keyop1) 通过函数fun versign (x, PU) 来验证m2的数字签名，如果验证结果为真则用OP的公钥PU (Keyop1) 对password进行加密得到密文encP; 最后, 对encP和用户名进行数字签名从而产生消息authorization并通过公开信道c发送该消息给OP。
OP进程的形式化建模如下所示：
processOP= (**Process OP**)
in (c, m1); (**OP recieve message1 from RP**)
let (client_id_op, response_type_op, scope_op, redirect_uri_op, state_op, SignedARM1)=m1 in
if versign (SignedARM1, PU (keyrp1))=(client_id_op, response_type_op, scope_op, redirect_uri_op, state_op) then
new ask_authentication;
let signask=sign ((ask_authentication), PR (keyop1)) in
let authenticationE_U=(ask_authentication, signask) in
out (c, authenticationE_U);
(**OP sends message2 to End_Use**)
in (c1, mp1); (**OP recives the password from main process**)
in (c, m3); (**OP recieve message3 from End_User**)
let (encP1, username_op, signgM3)=m3 in
if versign (signgM3, PU (keyeu))=(encP1, username_op) then
let password=mp1 in
if adec (encP1, PR (keyop1))= (mp1) then
new code_op; new id_token_op;
let signedM=sign ((code_op, id_token_op), PR (keyop1)) in
let authorizationResp=(code_op, id_token_op, signedM) in
out (c, authorizationResp); (**OP sneds message4 to RP**)
in (c, m5); (**OP recieve message5 from RP**)
let (grant_type_op, code_op, redirect_uri_op, client_secret_op, client_id_op, signM5)=m5 in
if versign (signM5, PU (keyrp2))=(grant_type_op, code_op, redirect_uri_op, client_secret_op, client_id_op) then
new access_token_op; new id_token_op; new token_type_op; new expires_in_op;
let signedMessage=sign ((access_token_op, id_token_op, token_type_op, expires_in_op), PR (keyop1)) in
let token_response=(access_token_op, id_token_op, token_type_op, expires_in_op, signedMessage) in
out (c, token_response)
(**OP sends m6 which was signed to RP**)
OP通过信道c接收RP发来的签名消息m1，然后通过RP的公钥PU (keyrp1) 用函数fun versign (x, PU) 验证数字签名，若签名得到验证，则生成消息authenticationE_U，其参数是经过数字签名的ask_authentication。
首先经过公开信道c把此消息发送给EU。然后OP分别通过隐私信道c1和公开信道c接收主进程发来的password和签名消息m3，接下来用EU的公钥PU (keyeu) 通过函数fun versign (x, PU) 验证数字签名消息signgM3，若验证结果为真则OP通过自身的私钥PR (keyop1) 用函数fun adec (x, PR) 解密密文encP1，若成功解密则产生授权码code_op及身份令牌id_token_op并对这两个参数进行签名后得到授权响应消息authorizationResp，再经由信道c发送该消息给RP。最后，OP接收RP发来的签名消息m5，先用RP的私钥PR (keyrp2) 通过函数fun versign (x, PU) 验证签名，若验签成功，则生成如下参数：访问令牌access_token_op、id_token_op、token类型token_type_op及access_token生命周期expiress_in_op，然后用OP的私钥PR (keyop1) 对以上参数进行数字签名后得到令牌响应消息token_response并通过公开信道c将该消息发送给RP。
RP进程的形式化建模如下所示:
processRP= (**Process RP**)
new client_id_rp; new response_type_rp; new scope_rp;
new redirect_uri_rp; new state_rp;
let SignedMAR=sign ((client_id_rp, response_type_rp, scope_rp, redirect_uri_rp, state_rp), PR (keyrp1)) in
let authenticationRe=(client_id_rp, response_type_rp, scope_rp, redirect_uri_rp, state_rp, SignedMAR) in
out (c, authenticationRe); (**RP sends message1 to OP**)
in (c, m4); (**RP recieve message4 from OP**)
let (code_rp, id_token_rp, signedM4)=m4 in
if versign (signedM4, PU (keyop1))=(code_rp, id_token_rp) then
new grant_type_rp; new code_rp; new redirect_uri_rp;
new client_secret_rp; new client_id_rp;
let signM4=sign ((grant_type_rp, code_rp, redirect_uri_rp, client_secret_rp, client_id_rp), PR (keyrp2)) in
let tokenrequest=(grant_type_rp, code_rp, redirect_uri_rp, client_secret_rp, client_id_rp, signM4) in
out (c, tokenrequest); (**RP sends m5 to OP**)
in (c, m6);
let (access_token_rp, id_token_rp, token_type_rp, expires_in_rp, signedMessage1)=m6 in
if versign (signedMessage1, PU (keyop1))=(access_token_rp, id_token_rp, token_type_rp, expires_in_rp) then
new finished;
out (c, finished) (**Finished**)
首先RP产生消息参数：客户端身份标识client_id_rp、响应类型response_type_rp、访问域值scope_rp、重定向地址redirect_uri_rp及认证状态state_rp，然后对这些参数签名后验证请求消息authenticationRe并通过公开信道c发送该消息给OP。之后，RP接收OP进程发来的签名消息m4，再用OP的公钥PU (keyop1) 通过函数fun versign (x, PU) 对m4进行签名确认，若确认结果为真，则产生参数：授权类型grant_type_rp，授权码code_rp、重定向地址redirect_uri、RP与OP共享密码client_secret_rp及客户端身份标识client_id_rp，接下来RP对以上参数用RP的私钥进行PR (keyrp2) 签名后得到令牌请求消息tokenrequest并通过公开信道c发送该消息给OP，最后RP接收OP发来的签名后消息m6并用OP的公钥PU (keyop1) 通过函数fun versign (x, PU) 确认其数字签名，若签名得到确认，则RP通过信道c输出Finished，至此协议通信结束。
3 使用ProVerif自动化验证秘密性及认证性在ProVerif中，本文使用query attacker (password) 来验证口令password的秘密性，使用非单射性来建模认证性，如表 1所示，本文使用query ev:e1==>ev:e2来建模认证性，query ev:e1==>ev:e2的含义为：当事件e1执行并且事件e2在其之后执行时候结果为真。在表 1中，语句ev:endauthusera_s (x)==>ev:beginaauthusera_s (x) 用来建模授权服务器对EU的认证性，ev:endautha_suser (x)==>ev:beginaautha_suser (x) 用来建模EU对授权服务器的认证性，ev:endauthRPE_p (x)==>ev:beginaauthRpE_p (x) 用来建模令牌端点对RP的认证性，ev:endautha_sRP (x)==>ev:beginaautha_sRP (x) 用来建模RP对授权服务器的认证性，ev:endauthRPa_s (x)==>ev:beginaauthRPa_s (x) 用来建模授权服务器对RP的认证性，ev:endauthE_pRP (x)==>ev:beginaauthE_pRP (x) 用来建模RP对令牌端点的认证性。
|
表 1 非单射性对认证性的建模 Table 1 Modeling of authentication by non-injective relations |
ProVerif的输入有Horn子句和应用PI验算两种方式，本文建模选择应用PI演算作为输入，应用PI演算输入必须转化为ProVerif的语法才能输入到Proverif运行，图 2所示为转化后的ProVerif输入及添加验证认证性的事件查询。
|
图 2 改进的OpenID Connect协议ProVerif输入 Figure 2 Inputs of modified OpenID connect protocol |
将图 2中ProVerif语句输入到ProVerif执行，输出结果如图 3~6所示。图 3是password秘密性形式化建模分析的结果，其结果是true，证明口令具有秘密性，即用口令是安全的。因为在改进的OpenID Connect协议中，EU首先用OP的公钥PU (keyop1) 对口令password进行加密得到密文encP，再将此密文同用户名使用自己的私钥PR (keyeu) 签名后通过授权消息发送给OP，OP收到授权消息后先验证消息的数字签名再对密文使用自己的私钥PR (keyop1) 进行解密。在这个过程中，攻击者无法获得口令。
|
图 3 password秘密性 Figure 3 Secrecy of password |
|
图 4 RP与Token Endpoint相互认证结果 Figure 4 Authentication between RP and Token Endpoint |
|
图 5 授权服务器与RP相互认证结果 Figure 5 Authentication between authorization server and RP |
|
图 6 授权服务器与EU相互认证结果 Figure 6 Authentication between authorization server and EU |
图 4中 (a) 和 (b) 是RP对Token Endpoint认证性和Token Endpoint对RP认证性的建模分析结果，两者结果均为true，说明令牌端点对RP的认证性及RP对令牌端点的认证性都得到验证，即RP与Token Endpoint之间具有相互认证性。因为在改进的OpenID Connect协议中，在RP发送到令牌端点的令牌请求消息token_request前，RP用自己的私钥PR (keyrp2) 对令牌请求消息中的参数进行数字签名，在令牌端点接收到该签名消息之后使用RP的公钥PU (keyrp2) 验证该数字签名，从而使令牌端点对RP的认证性得到验证。同样，在令牌端点发送到RP的令牌响应消息token_response前，令牌端点使用OP的私钥PR (keyop1) 对响应消息中的参数都进行数字签名之后发送到RP，RP收到该消息之后用OP的公钥PU (keyop1) 验证该数字签名，从而使RP对令牌端点的认证性得到验证。
图 5中 (a) 和 (b) 是授权服务器对RP认证性和RP对授权服务器认证性的建模分析结果，两者的结果均为true，说明授权服务器对RP及RP对授权服务器的认证性都得到验证，即授权服务器与RP之间具有相互认证性。因为在改进的OpenID Connect协议中，在RP发送到授权服务器的认证请求消息authenticationRe前，RP用自己的私钥PR (keyrp1) 对认证请求消息的参数签名，授权服务器收到该签名消息之后用RP的公钥PU (keyrp1) 验证该了签名，从而使授权服务器对RP的认证性得到验证。
在授权服务器发送到RP的认证响应消息前，授权服务器用OP的私钥PR (keyop1) 对该消息参数进行数字签名，RP收到该签名消息后用OP公钥PU (keyop1) 验证该了数字签名，从而使RP对授权服务器的认证性得到验证。
图 6中 (a) 和 (b) 是授权服务器对EU认证性和EU对授权服务器的建模分析结果，两者的结果均为true，表明授权服务器对EU及EU对授权服务器的认证性都得到验证，即授权服务器与EU之间具有相互认证性。因为在改进的OpenID Connect协议中，在EU发送给授权服务器的authorization消息前，EU首先对口令password用OP的公钥PU (keyop1) 进行加密后得到密文encP，EU用自己的私钥PR (keyeu) 再对encP及username进行数字签名之后再通过授权消息发送到授权服务器，授权服务器收到该消息后用OP的公钥PR (keyop1) 验证了签名，从而使授权服务器对EU的认证性得到验证。在授权服务器发送到EU的authentication消息前，授权服务器用OP的私钥PR (keyop1) 对参数ask_authentication进行数字签名之后发送给EU，EU收到该签名消息后用OP的公钥PU (keyop1) 验证了该签名，从而使EU对授权服务器的认证性得到验证。
在改进的OpenID Connect协议中，采用数字签名及加密技术能很好地解决原来协议中存在的安全性问题及不完整的认证性的问题，结果表明，改进方法可行且正确。
4 结语OpenID Connect协议规范指出用标准的安全协议如安全传输层协议 (Transport Layer Security, TLS) 等来解决其安全性。然而，在OpenID Connect协议中，已经有用于实现实体认证性的数字签名机制；此外，部署TLS协议的开销比较大也比较复杂，同时也使得通信效率降低。通过对标准的OpenID Connect协议使用基于符号模型的ProVerif进行形式化建模分析后发现，在整个协议中只存在RP对令牌端点的认证性且用户口令无秘密性。令牌端点对RP、EU对授权服务器及授权服务器对EU均无认证性。关于令牌端点对RP的认证性，攻击者通过函数tuple能获取到通信时的消息参数 (clien_id_op, code_id_op, scope, redirect_uri_op, state_op)、(username, userpassword)、(grant_type_op, code_op, redirect_uri_op, client_secret_op, client_id_op) 进而展开攻击，从而使令牌端点对RP无认证性。同理，关于EU对授权服务器及授权服务器对EU的认证性，攻击者都能获取到通信相关的消息参数进而发起攻击使得它们不具有相互认证性。对于用户口令password，根据ProVerif结果发现，攻击者能截取到password，故用户口令无秘密性。
本文的研究对象和文献[18]相同，但本文的工作与文献[18]的区别有以下4个方面：
1) 文献[18]的形式化建模语言采用的是基于计算模型的Blanchet演算，而本文采用的是基于符号模型的应用PI演算。
2) 文献[18]使用的软件工具是CryptoVerif，而本文所使用的工具是ProVerif。
3) 分析结论方面，文献[18]针对终端用户与授权服务器不具相互认证性及令牌端点对RP不具认证性提出了使用数字签名来解决认证性不完整的缺陷的方法，但只指出了对某个参数进行签名来达到完善认证性的目的。例如文献[18]为了完善令牌端点对RP的认证性，指出当RP发送令牌请求消息时只对授权码code进行签名，令牌端点收到包含该签名的消息之后对该签名进行验证，若验证通过则实现了令牌端点对RP的认证。但是在标准的OpenID Connect中，令牌请求消息还包含了重定向地址redirect_uri、RP与OP共享密码client_secret等必需参数，若它们被攻击者截获利用，那么整个系统将面临被攻击的危险。而本文采用对各个消息的每个必需参数进行签名从而完善协议的认证性。
4) 文献[18]没有关注用户口令password的秘密性，而本文关注了用户口令的秘密性且就password秘密性不强的缺陷使用非对称加密技术对其进行改进。
因此本文使用数字签名及非对称加密技术，加强了用户口令的秘密性以及完善了协议中通信三方之间的相互认证性。在符号模型下应用应用PI演算对改进的OpenID Connect协议进行形式化建模并转化为ProVerif的输入并在ProVerif中执行。建模分析结果表明用户口令的秘密性和协议通信三方的相互认证性得到完善。
对于用户口令，终端用户通过OP的公钥加密用户口令后得到密文，然后再将此密文与用户名一起签名后通过授权消息发送到授权服务器，在授权服务器端进行签名确认及私钥解密的操作，整个过程攻击者无法获取到口令，保证了用户口令的秘密性。在终端用户与授权服务器之间的相互认证方面，因为授权服务器需要向终端用户发送认证请求消息并且终端用户需要响应此消息并返回响应消息给授权服务器，在这两个消息中，本文均对各自的参数进行了数字签名，并且在对方收到签名消息后都验证了签名，这就使终端用户与授权服务器之间相互认证得到验证。在授权服务器与RP方的相互认证方面，因为RP首先需要发送用自己私钥签名的访问认证请求消息给授权服务器，授权服务器收到这个签名的认证消息后，首先用RP的公钥验证签名，再对这个请求作出响应，然后再把认证后的结果用自己私钥数字签名后发送给RP，RP收到该消息后用授权服务器公钥验证该签名，这样使授权服务器和RP之间的认证性得到验证。在RP与令牌端点之间的相互认证性方面，因为RP需要发送令牌请求消息到令牌端点，当令牌端点收到这个请求消息后需要对该请求消息作出响应，所以本文对令牌请求消息和请求响应消息中的所有参数都进行了数字签名，当对方收到消息后都对签名进行验证，这样就验证了令牌端点和RP之间的相互认证性。
下阶段工作主要是将改进的协议应用到实际的网络环境中去，在实际应用中发现攻击与漏洞并逐步完善OpenID Connect协议。
| [1] | 李雄. 多种环境下身份认证协议的研究与设计[D]. 北京: 北京邮电大学, 2012: 11-55. ( LI X. Research and design on identity authentication protocol for multi-environments[D].Beijing:Beijing University of Posts and Telecommunications, 2012:11-55. ) |
| [2] | 张焕国, 韩文报, 来学嘉, 等. 网络空间安全综述[J]. 中国科学:信息科学, 2016, 46(2): 125-164. ( ZHANG H G, HAN W B, LAI X J, et al. Survey on cyberspace security[J]. SCIENTIA SINICA Informationis, 2016, 46(2): 125-164. ) |
| [3] | OpenID Connect Core 1.0 incorporating errata set 1[EB/OL].[2016-04-16]. http://OpenID.net/specs/OpenID-connect-core-1_0.html#toc. |
| [4] | DICK H. The OAuth 2.0 authorization framework[EB/OL].[2016-02-15].http://tools.ietf.org/html/rfc6749. |
| [5] | DAVID R, BRAD F. OpenID Authentication 2.0-Final, 2007[EB/OL].[2016-02-26].http://OpenID.net/specs/OpenID-authentication-2_0.html. |
| [6] | 高焕芝. 单点登录技术的研究[D]. 北京: 北京邮电大学, 2006: 7-39. ( GAO H Z. Research of single sign-on technology[D].Beijing:Beijing University of Posts and Telecommunications, 2006:7-39. ) |
| [7] | LI W P, MITCHELLC J. Analysing the security of Google's implementation of OpenID connect[C]//Proceedings of 13th International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment. Berlin:Springer, 2016:357-376. |
| [8] | ZHANG J L, LU J T, WAN Z Y, et al. Security analysis of OpenID connect protocol with cryptoverif in the computational model[C]//Proceedings of the 11th International Conference on P2P, Parallel, Grid, Cloud and Internet Computing. Berlin:Springer, 2016:925-934. |
| [9] | BLANCHET B. Automatic proof of strong secrecy for security protocols[C]//Proceedings of the 2004 IEEE Symposium on Security and Privacy. Piscataway, NJ:IEEE, 2004:86-100. |
| [10] | BHAVESH N B, MAITY S, HANSDAH R C. An authentication protocol for vehicular Ad Hoc networks with heterogeneous anonymity requirements[J]. International Journal of Space-Based and Situated Computing, 2014, 4(1): 1-14. doi: 10.1504/IJSSC.2014.060684 |
| [11] | 来学嘉, 卢明欣, 秦磊, 等. 基于DNA技术的非对称加密与签名方法[J]. 中国科学:信息科学, 2010, 40(2): 240-248. ( LAI X J, LU M X, QIN L, et al. Asymmetric encryption and signature methods with DNA technology[J]. SCIENTIA SINICA Informationis, 2010, 40(2): 240-248. ) |
| [12] | 卓先德, 赵菲, 曾德明. 非对称加密技术研究[J]. 四川理工学院学报 (自然科学版), 2010, 23(5): 562-564. ( ZHUO X D, ZHAO F, ZENG D M. Research of asymmetric encryption technology[J]. Journal of Sichuan University of Science & Engineering (Natural Science Edition), 2010, 23(5): 562-564. ) |
| [13] | BLANCHET B. An efficient cryptographic protocol verifier based on Prolog rules[C]//Proceedings of the 14th IEEE Computer Security Foundations. Washington, DC:IEEE Computer Society, 2011:82-96. |
| [14] | GUANGYE S, MOHAMED M. FASER (Formal and Automatic Security Enforcement by Rewriting) by BPA algebra with test[J]. International Journal of Grid and Utility Computing, 2013, 4(2/3): 204-211. doi: 10.1504/IJGUC.2013.056257 |
| [15] | ABADI M, FOURNET C. Mobile values, new names, and secure communication[C]//Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York:ACM, 2001:104-115. |
| [16] | BARENGHI A, GERARDO P, TERANEO F. Secure and efficient design of software block cipher implementations on microcontrollers[J]. International Journal of Grid and Utility Computing, 2013, 4(2/3): 110-118. doi: 10.1504/IJGUC.2013.056246 |
| [17] | 冯超, 张权, 唐朝京. 计算可靠的Diffie-Hellman密钥交换协议自动证明[J]. 通信学报, 2011, 32(10): 118-126. ( FENG C, ZHANG Q, TANG C J. Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols[J]. Journal on Communications, 2011, 32(10): 118-126. ) |
| [18] | 孟博, 张金丽, 鲁金钿. 基于计算模型的OpenID Connect协议认证性的自动化分析[J]. 中南民族大学学报 (自然科学版), 2016, 35(3): 123-129. ( MENG B, ZHANG J L, LU J T. Automatic analysis of authentication of OpenID Connect protocol based on the computational model[J]. Journal of South-Central University for Nationalities (Natural Science Edition), 2016, 35(3): 123-129. ) |