改進(jìn)的OpenID Connect協(xié)議及其安全性分析

魯金鈿，堯利利,何旭東，孟 博

(中南民族大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院，武漢 430074)

改進(jìn)的OpenID Connect協(xié)議及其安全性分析

魯金鈿，堯利利,何旭東，孟 博*

(中南民族大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院，武漢 430074)

(*通信作者電子郵箱mengscuec@gmail.com)

OpenID Connect協(xié)議是最新的單點(diǎn)登錄協(xié)議之一，已經(jīng)廣泛應(yīng)用于用戶身份認(rèn)證領(lǐng)域，其安全性受到了人們的重點(diǎn)關(guān)注。為增強(qiáng)OpenID Connect協(xié)議的安全性，首先引入數(shù)字簽名及非對(duì)稱加密技術(shù)，對(duì)其進(jìn)行改進(jìn)，重點(diǎn)關(guān)注改進(jìn)后協(xié)議的秘密性和認(rèn)證性; 其次基于符號(hào)模型，應(yīng)用應(yīng)用PI演算對(duì)改進(jìn)的OpenID Connect協(xié)議進(jìn)行形式化建模; 然后為驗(yàn)證改進(jìn)后協(xié)議的認(rèn)證性和秘密性，分別使用非單射性和query對(duì)認(rèn)證性和秘密性進(jìn)行建模; 最后把改進(jìn)的OpenID Connect協(xié)議的應(yīng)用PI演算模型轉(zhuǎn)換為安全協(xié)議分析工具ProVerif的輸入，應(yīng)用ProVerif對(duì)其進(jìn)行形式化分析。實(shí)驗(yàn)結(jié)果表明，改進(jìn)后的OpenID Connect協(xié)議具有認(rèn)證性和秘密性。

非對(duì)稱加密；數(shù)字簽名；認(rèn)證性；符號(hào)模型；形式化方法；ProVerif

0 引言

身份認(rèn)證[1]是網(wǎng)絡(luò)空間安全[2]的一個(gè)重要研究領(lǐng)域，目前提出了OpenID Connect[3]、OAuth2.0[4]、OpenID[5]、CardSpace等安全身份認(rèn)證協(xié)議，其中OpenID Connect是2014年發(fā)布的OpenID最新的用戶身份認(rèn)證及分布式身份系統(tǒng)標(biāo)準(zhǔn)，是非常重要的單點(diǎn)登錄[6]認(rèn)證協(xié)議標(biāo)準(zhǔn)之一，它已經(jīng)被Google和Microsoft等互聯(lián)網(wǎng)企業(yè)廣泛應(yīng)用，故其安全性受到人們的重點(diǎn)關(guān)注。Li等[7]發(fā)現(xiàn)并公布了該協(xié)議的諸多漏洞，攻擊者能利用這些漏洞登錄到OpenID Connect協(xié)議Relay Part的網(wǎng)站上，從而使整個(gè)系統(tǒng)面臨被攻擊的危險(xiǎn)。Zhang等[8]使用基于計(jì)算模型的CryptoVerif對(duì)OpenID Connect協(xié)議進(jìn)行形式化建模分析，結(jié)果表明該協(xié)議的認(rèn)證性不完整和用戶口令秘密性[9]不強(qiáng)。為此本文引入數(shù)字簽名[10]及非對(duì)稱加密技術(shù)[11-12]，對(duì)OpenID Connect協(xié)議進(jìn)行改進(jìn)，并在符號(hào)模型下，應(yīng)用基于符號(hào)模型的安全協(xié)議分析工具ProVerif[13]對(duì)改進(jìn)的OpenID Connect協(xié)議進(jìn)行形式化建模分析[14]，結(jié)果表明改進(jìn)后的協(xié)議具有認(rèn)證性和秘密性。

1 改進(jìn)的OpenID Connect協(xié)議

改進(jìn)的OpenID Connect協(xié)議同樣定義了三個(gè)角色，分別是終端用戶(End User，EU)、OpenID 服務(wù)提供方(OpenID Provider，OP)及OpenID依賴方(Relay Part，RP)，其中OpenID 服務(wù)提供方又包含令牌端點(diǎn)(Token Endpoint)、授權(quán)服務(wù)器(Authentication Server)及用戶信息端點(diǎn)，令牌端點(diǎn)主要負(fù)責(zé)生成和發(fā)送Token，授權(quán)服務(wù)器主要負(fù)責(zé)對(duì)認(rèn)證請(qǐng)求作出響應(yīng)并授權(quán)，用戶信息端點(diǎn)主要存儲(chǔ)用戶在OpenID提供方注冊(cè)時(shí)留下的個(gè)人相關(guān)信息，在通常應(yīng)用場(chǎng)景中，RP是客戶端，EU是用戶個(gè)人，OP是OpenID服務(wù)提供者。改進(jìn)的OpenID Connect協(xié)議的消息結(jié)構(gòu)如圖1所示。

1.1 RP認(rèn)證請(qǐng)求

為訪問EU存儲(chǔ)在OP上受保護(hù)的資源，RP向OP發(fā)送一個(gè)身份認(rèn)證請(qǐng)求消息(1)Authentication Resquest，該消息包含5個(gè)主要參數(shù)，分別是客戶端id(client_id)、授權(quán)方式的響應(yīng)類型(response_type)、訪問域值(scope)、重定向地址(redirect_uri)及請(qǐng)求和反饋之間的狀態(tài)值(state)，當(dāng)協(xié)議使用混合流的方式進(jìn)行身份認(rèn)證時(shí)，response_type的值是code_ id_token。RP對(duì)這些參數(shù)進(jìn)行數(shù)字簽名后通過消息(1)發(fā)送給授權(quán)服務(wù)器。

圖1 改進(jìn)的OpenID Connect協(xié)議消息結(jié)構(gòu)Fig. 1 Procedure of modified OpenID Connect protocol

1.2 認(rèn)證EU請(qǐng)求

當(dāng)授權(quán)服務(wù)器收到消息(1)后，首先驗(yàn)證該消息的數(shù)字簽名，若驗(yàn)證成功，則根據(jù)OAuth2.0的參數(shù)確認(rèn)規(guī)則來確認(rèn)所有參數(shù)的完整性和用法是否符合法。若參數(shù)合法，授權(quán)服務(wù)器就產(chǎn)生認(rèn)證EU的請(qǐng)求消息(2)Authenticate End_user，該消息包含認(rèn)證參數(shù)ask_authentication，授權(quán)服務(wù)器對(duì)該參數(shù)簽名后通過消息(2)發(fā)送給EU。若驗(yàn)簽失敗，則授權(quán)服務(wù)器返回一個(gè)驗(yàn)簽失敗消息給RP。

1.3 OP獲得授權(quán)

當(dāng)EU收到消息(2)后，首先驗(yàn)證消息(2)的數(shù)字簽名：驗(yàn)簽成功，則對(duì)其參數(shù)進(jìn)行確認(rèn)；若驗(yàn)簽失敗，則EU返回一個(gè)驗(yàn)簽失敗消息給授權(quán)服務(wù)器。如果EU同意授權(quán)給授權(quán)服務(wù)器，它會(huì)產(chǎn)生授權(quán)消息(3)End_user grant，該消息主要包含之前EU在OP端注冊(cè)時(shí)的用戶名(username)和用戶口令(password)。首先，EU對(duì)用戶口令用OP的公鑰PU(keyop1)通過函數(shù)aenc(x,PU)加密得到密文encP; 然后將密文encP和username經(jīng)過數(shù)字簽名后通過消息(3)發(fā)送給授權(quán)服務(wù)器。在改進(jìn)的OpenID Connect協(xié)議中，參數(shù)password由主進(jìn)程通過隱私信道c1分別發(fā)送給EU和OP。

1.4 認(rèn)證響應(yīng)

當(dāng)授權(quán)服務(wù)器收到消息(3)后，首先驗(yàn)證消息(3)的數(shù)字簽名，驗(yàn)證成功后再根據(jù)得到的密文encp1用自己的私鑰PR(keyop1)通過函數(shù)adec(x,PR)解密密文encp1，檢查解密得到的口令明文是否與注冊(cè)時(shí)的password一致，若一致，則說明EU用戶同意授權(quán)，那么授權(quán)服務(wù)器產(chǎn)生包含授權(quán)碼code及身份令牌id_token的認(rèn)證響應(yīng)消息(4)Authentication Response，授權(quán)服務(wù)器再通過數(shù)字簽名對(duì)這兩個(gè)參數(shù)進(jìn)行簽名后通過消息(4)發(fā)送給RP。若驗(yàn)簽失敗，則授權(quán)服務(wù)器返回驗(yàn)簽失敗消息給EU。

1.5 令牌請(qǐng)求

當(dāng)RP收到消息(4)后，首先驗(yàn)證這個(gè)消息的數(shù)字簽名，檢查授權(quán)碼code是否正確且未使用過，若驗(yàn)證成功，則產(chǎn)生令牌請(qǐng)求消息(5)Token Resquest，該消息主要包含參數(shù)grant_type、客戶id(client_id)、重定向地址redirect_uri、RP與OP共享的密鑰client_secret，其中g(shù)rant_type的值為code，這表明RP需要用授權(quán)碼code在令牌端點(diǎn)換取訪問令牌access_token，client_id與消息(1)的clien_id一致。最后RP將這些參數(shù)進(jìn)行簽名再通過消息(5)發(fā)送給令牌端點(diǎn)。若驗(yàn)簽失敗，RP則返回一個(gè)驗(yàn)簽失敗消息給授權(quán)服務(wù)器。

1.6 令牌響應(yīng)

當(dāng)令牌端點(diǎn)收到消息(5)后，首先驗(yàn)證該消息的數(shù)字簽名，檢查授權(quán)類型grant_type和授權(quán)碼code的值，驗(yàn)簽成功后產(chǎn)生令牌響應(yīng)消息(6)Token Response，該消息主要包含參數(shù)access_token、令牌類型token_type、身份令牌id_token及access_token的生命周期expiress_in，其中id_token與消息(4)中的id_token保持一致，token_type值為Bear。若驗(yàn)簽失敗，則令牌端點(diǎn)返回一個(gè)驗(yàn)簽失敗消息給RP。然后令牌端點(diǎn)對(duì)這些參數(shù)進(jìn)行數(shù)字簽名后通過消息(6)發(fā)送給RP。RP收到令牌消息(6)后，首先驗(yàn)證該消息的數(shù)字簽名：若驗(yàn)證結(jié)果為真，協(xié)議通信到此結(jié)束；否則RP返回一個(gè)驗(yàn)簽失敗消息給令牌端點(diǎn)。

2 形式化建模改進(jìn)的OpenID Connect協(xié)議

應(yīng)用PI演算是Abadi等[15]在2001年提出來的，它是用來形式化建模并發(fā)進(jìn)程之間相互通信的形式化語言，它在PI演算的通信與并發(fā)結(jié)構(gòu)的基礎(chǔ)上，增加了函數(shù)和等式原語。消息不僅可以包含名，還可以是通過函數(shù)和名構(gòu)成的值。應(yīng)用PI演算使用函數(shù)來表示通用的密碼學(xué)原語[16]，如加密、解密、數(shù)字簽名等，不需要為每一個(gè)密碼操作都構(gòu)造新的密碼學(xué)原語，具有很好的通用性，因此可以建模和分析非常復(fù)雜的安全協(xié)議。

ProVerif是Blanchet于2001年開發(fā)的基于重寫逼近法的一階定理證明器，可以用來分析與驗(yàn)證使用Horn子句或者應(yīng)用PI演算描述的安全協(xié)議，可以建模各種密碼學(xué)原語：包括共享密鑰密碼學(xué)、公鑰密鑰密碼學(xué)、數(shù)字簽名、哈希函數(shù)以及Diffie-Hellman[17]密鑰交換等。同時(shí)它克服了模型檢測(cè)方法固有的缺陷——狀態(tài)空間爆炸問題，能夠處理無窮狀態(tài)系統(tǒng)。它能夠分析與驗(yàn)證保密性、認(rèn)證性、更一般的一致性、強(qiáng)保密性和進(jìn)程的觀察等價(jià)。ProVerif已經(jīng)成功分析了大量的復(fù)雜的安全協(xié)議。

2.1 函數(shù)與等式理論

本文使用應(yīng)用PI演算來建模改進(jìn)的OpenID Connect協(xié)議，下面描述了改進(jìn)的OpenID Connect協(xié)議的函數(shù)及等式理論。

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

進(jìn)程用私鑰PR通過函數(shù)fun sign(x,PR)來簽名消息x，用公鑰PU通過函數(shù)fun versign(x,PU)來驗(yàn)證數(shù)字簽名消息x。用公鑰PU通過函數(shù)fun aenc(x,PU)來加密消息x，用私鑰PR通過函數(shù)fun adec(x,PR)解密消息x。通過函數(shù)fun PR(b)接收私有值b作為輸入并產(chǎn)生私鑰作為輸出，同理通過函數(shù)fun PU(b)接收共有值b作為輸入并產(chǎn)生公鑰作為輸出。

2.2 進(jìn)程

完整的改進(jìn)的OpenID Connect協(xié)議進(jìn)程主要包含3個(gè)進(jìn)程：OP進(jìn)程、RP進(jìn)程及EU進(jìn)程,它們共同構(gòu)成了主進(jìn)程，如下所示：

OpenID=!processOP|!processRP|!processEU

EU進(jìn)程的形式化建模如下所示：

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接收從主進(jìn)程發(fā)來的password，再通過公開信道c接收OP進(jìn)程發(fā)來的簽名消息m2; 然后, 用OP的公鑰PU(Keyop1)通過函數(shù)fun versign(x,PU)來驗(yàn)證m2的數(shù)字簽名，如果驗(yàn)證結(jié)果為真則用OP的公鑰PU(Keyop1)對(duì)password進(jìn)行加密得到密文encP; 最后, 對(duì)encP和用戶名進(jìn)行數(shù)字簽名從而產(chǎn)生消息authorization并通過公開信道c發(fā)送該消息給OP。

OP進(jìn)程的形式化建模如下所示：

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發(fā)來的簽名消息m1，然后通過RP的公鑰PU(keyrp1)用函數(shù)fun versign(x,PU)驗(yàn)證數(shù)字簽名，若簽名得到驗(yàn)證，則生成消息authenticationE_U，其參數(shù)是經(jīng)過數(shù)字簽名的ask_authentication。首先經(jīng)過公開信道c把此消息發(fā)送給EU。然后OP分別通過隱私信道c1和公開信道c接收主進(jìn)程發(fā)來的password和簽名消息m3，接下來用EU的公鑰PU(keyeu)通過函數(shù)fun versign(x,PU)驗(yàn)證數(shù)字簽名消息signgM3，若驗(yàn)證結(jié)果為真則OP通過自身的私鑰PR(keyop1)用函數(shù)fun adec(x,PR)解密密文encP1，若成功解密則產(chǎn)生授權(quán)碼code_op及身份令牌id_token_op并對(duì)這兩個(gè)參數(shù)進(jìn)行簽名后得到授權(quán)響應(yīng)消息authorizationResp，再經(jīng)由信道c發(fā)送該消息給RP。最后，OP接收RP發(fā)來的簽名消息m5，先用RP的私鑰PR(keyrp2)通過函數(shù)fun versign(x,PU)驗(yàn)證簽名，若驗(yàn)簽成功，則生成如下參數(shù)：訪問令牌access_token_op、id_token_op、token類型token_type_op及access_token生命周期expiress_in_op，然后用OP的私鑰PR(keyop1)對(duì)以上參數(shù)進(jìn)行數(shù)字簽名后得到令牌響應(yīng)消息token_response并通過公開信道c將該消息發(fā)送給RP。

RP進(jìn)程的形式化建模如下所示:

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產(chǎn)生消息參數(shù)：客戶端身份標(biāo)識(shí)client_id_rp、響應(yīng)類型response_type_rp、訪問域值scope_rp、重定向地址redirect_uri_rp及認(rèn)證狀態(tài)state_rp，然后對(duì)這些參數(shù)簽名后驗(yàn)證請(qǐng)求消息authenticationRe并通過公開信道c發(fā)送該消息給OP。之后，RP接收OP進(jìn)程發(fā)來的簽名消息m4，再用OP的公鑰PU(keyop1)通過函數(shù)fun versign(x,PU)對(duì)m4進(jìn)行簽名確認(rèn)，若確認(rèn)結(jié)果為真，則產(chǎn)生參數(shù)：授權(quán)類型grant_type_rp，授權(quán)碼code_rp、重定向地址redirect_uri、RP與OP共享密碼client_secret_rp及客戶端身份標(biāo)識(shí)client_id_rp，接下來RP對(duì)以上參數(shù)用RP的私鑰進(jìn)行PR(keyrp2)簽名后得到令牌請(qǐng)求消息tokenrequest并通過公開信道c發(fā)送該消息給OP，最后RP接收OP發(fā)來的簽名后消息m6并用OP的公鑰PU(keyop1)通過函數(shù)fun versign(x,PU)確認(rèn)其數(shù)字簽名，若簽名得到確認(rèn)，則RP通過信道c輸出Finished，至此協(xié)議通信結(jié)束。

3 使用ProVerif自動(dòng)化驗(yàn)證秘密性及認(rèn)證性

在ProVerif中，本文使用query attacker(password)來驗(yàn)證口令password的秘密性，使用非單射性來建模認(rèn)證性，如表1所示，本文使用query ev:e1==>ev:e2來建模認(rèn)證性，query ev:e1==>ev:e2的含義為：當(dāng)事件e1執(zhí)行并且事件e2在其之后執(zhí)行時(shí)候結(jié)果為真。在表1中，語句ev:endauthusera_s(x)==>ev:beginaauthusera_s(x)用來建模授權(quán)服務(wù)器對(duì)EU的認(rèn)證性，ev:endautha_suser(x)==>ev:beginaautha_suser(x) 用來建模EU對(duì)授權(quán)服務(wù)器的認(rèn)證性，ev:endauthRPE_p(x)==>ev:beginaauthRpE_p(x) 用來建模令牌端點(diǎn)對(duì)RP的認(rèn)證性，ev:endautha_sRP(x)==>ev:beginaautha_sRP(x) 用來建模RP對(duì)授權(quán)服務(wù)器的認(rèn)證性，ev:endauthRPa_s(x)==>ev:beginaauthRPa_s(x) 用來建模授權(quán)服務(wù)器對(duì)RP的認(rèn)證性，ev:endauthE_pRP(x)==>ev:beginaauthE_pRP(x) 用來建模RP對(duì)令牌端點(diǎn)的認(rèn)證性。

ProVerif的輸入有Horn子句和應(yīng)用PI驗(yàn)算兩種方式，本文建模選擇應(yīng)用PI演算作為輸入，應(yīng)用PI演算輸入必須轉(zhuǎn)化為ProVerif的語法才能輸入到Proverif運(yùn)行，圖2所示為轉(zhuǎn)化后的ProVerif輸入及添加驗(yàn)證認(rèn)證性的事件查詢。

將圖2中ProVerif語句輸入到ProVerif執(zhí)行，輸出結(jié)果如圖3～6所示。圖3是password秘密性形式化建模分析的結(jié)果，其結(jié)果是true，證明口令具有秘密性，即用口令是安全的。因?yàn)樵诟倪M(jìn)的OpenID Connect協(xié)議中，EU首先用OP的公鑰PU(keyop1)對(duì)口令password進(jìn)行加密得到密文encP，再將此密文同用戶名使用自己的私鑰PR(keyeu)簽名后通過授權(quán)消息發(fā)送給OP，OP收到授權(quán)消息后先驗(yàn)證消息的數(shù)字簽名再對(duì)密文使用自己的私鑰PR(keyop1)進(jìn)行解密。在這個(gè)過程中，攻擊者無法獲得口令。

圖4中(a)和(b)是RP對(duì)Token Endpoint認(rèn)證性和Token Endpoint對(duì)RP認(rèn)證性的建模分析結(jié)果，兩者結(jié)果均為true，說明令牌端點(diǎn)對(duì)RP的認(rèn)證性及RP對(duì)令牌端點(diǎn)的認(rèn)證性都得到驗(yàn)證，即RP與Token Endpoint之間具有相互認(rèn)證性。因?yàn)樵诟倪M(jìn)的OpenID Connect協(xié)議中，在RP發(fā)送到令牌端點(diǎn)的令牌請(qǐng)求消息token_request前，RP用自己的私鑰PR(keyrp2)對(duì)令牌請(qǐng)求消息中的參數(shù)進(jìn)行數(shù)字簽名，在令牌端點(diǎn)接收到該簽名消息之后使用RP的公鑰PU(keyrp2)驗(yàn)證該數(shù)字簽名，從而使令牌端點(diǎn)對(duì)RP的認(rèn)證性得到驗(yàn)證。同樣，在令牌端點(diǎn)發(fā)送到RP的令牌響應(yīng)消息token_response前，令牌端點(diǎn)使用OP的私鑰PR(keyop1)對(duì)響應(yīng)消息中的參數(shù)都進(jìn)行數(shù)字簽名之后發(fā)送到RP，RP收到該消息之后用OP的公鑰PU(keyop1)驗(yàn)證該數(shù)字簽名，從而使RP對(duì)令牌端點(diǎn)的認(rèn)證性得到驗(yàn)證。

圖2 改進(jìn)的OpenID Connect協(xié)議ProVerif輸入Fig. 2 Inputs of modified OpenID connect protocol

圖3 password秘密性Fig. 3 Secrecy of password

圖5中(a)和(b)是授權(quán)服務(wù)器對(duì)RP認(rèn)證性和RP對(duì)授權(quán)服務(wù)器認(rèn)證性的建模分析結(jié)果，兩者的結(jié)果均為true，說明授權(quán)服務(wù)器對(duì)RP及RP對(duì)授權(quán)服務(wù)器的認(rèn)證性都得到驗(yàn)證，即授權(quán)服務(wù)器與RP之間具有相互認(rèn)證性。因?yàn)樵诟倪M(jìn)的OpenID Connect協(xié)議中，在RP發(fā)送到授權(quán)服務(wù)器的認(rèn)證請(qǐng)求消息authenticationRe前，RP用自己的私鑰PR(keyrp1)對(duì)認(rèn)證請(qǐng)求消息的參數(shù)簽名，授權(quán)服務(wù)器收到該簽名消息之后用RP的公鑰PU(keyrp1)驗(yàn)證該了簽名，從而使授權(quán)服務(wù)器對(duì)RP的認(rèn)證性得到驗(yàn)證。在授權(quán)服務(wù)器發(fā)送到RP的認(rèn)證響應(yīng)消息前，授權(quán)服務(wù)器用OP的私鑰PR(keyop1)對(duì)該消息參數(shù)進(jìn)行數(shù)字簽名，RP收到該簽名消息后用OP公鑰PU(keyop1)驗(yàn)證該了數(shù)字簽名，從而使RP對(duì)授權(quán)服務(wù)器的認(rèn)證性得到驗(yàn)證。

圖4 RP與Token Endpoint相互認(rèn)證結(jié)果Fig. 4 Authentication between RP and Token Endpoint

圖5 授權(quán)服務(wù)器與RP相互認(rèn)證結(jié)果Fig. 5 Authentication between authorization server and RP

圖6中(a)和(b)是授權(quán)服務(wù)器對(duì)EU認(rèn)證性和EU對(duì)授權(quán)服務(wù)器的建模分析結(jié)果，兩者的結(jié)果均為true，表明授權(quán)服務(wù)器對(duì)EU及EU對(duì)授權(quán)服務(wù)器的認(rèn)證性都得到驗(yàn)證，即授權(quán)服務(wù)器與EU之間具有相互認(rèn)證性。因?yàn)樵诟倪M(jìn)的OpenID Connect協(xié)議中，在EU發(fā)送給授權(quán)服務(wù)器的authorization消息前，EU首先對(duì)口令password用OP的公鑰PU(keyop1)進(jìn)行加密后得到密文encP，EU用自己的私鑰PR(keyeu)再對(duì)encP及username進(jìn)行數(shù)字簽名之后再通過授權(quán)消息發(fā)送到授權(quán)服務(wù)器，授權(quán)服務(wù)器收到該消息后用OP的公鑰PR(keyop1)驗(yàn)證了簽名，從而使授權(quán)服務(wù)器對(duì)EU的認(rèn)證性得到驗(yàn)證。在授權(quán)服務(wù)器發(fā)送到EU的authentication消息前，授權(quán)服務(wù)器用OP的私鑰PR(keyop1)對(duì)參數(shù)ask_authentication進(jìn)行數(shù)字簽名之后發(fā)送給EU，EU收到該簽名消息后用OP的公鑰PU(keyop1)驗(yàn)證了該簽名，從而使EU對(duì)授權(quán)服務(wù)器的認(rèn)證性得到驗(yàn)證。

圖6 授權(quán)服務(wù)器與EU相互認(rèn)證結(jié)果Fig. 6 Authentication between authorization server and EU

在改進(jìn)的OpenID Connect協(xié)議中，采用數(shù)字簽名及加密技術(shù)能很好地解決原來協(xié)議中存在的安全性問題及不完整的認(rèn)證性的問題，結(jié)果表明，改進(jìn)方法可行且正確。

4 結(jié)語

OpenID Connect協(xié)議規(guī)范指出用標(biāo)準(zhǔn)的安全協(xié)議如安全傳輸層協(xié)議(Transport Layer Security, TLS)等來解決其安全性。然而，在OpenID Connect協(xié)議中，已經(jīng)有用于實(shí)現(xiàn)實(shí)體認(rèn)證性的數(shù)字簽名機(jī)制；此外，部署TLS協(xié)議的開銷比較大也比較復(fù)雜，同時(shí)也使得通信效率降低。通過對(duì)標(biāo)準(zhǔn)的OpenID Connect協(xié)議使用基于符號(hào)模型的ProVerif進(jìn)行形式化建模分析后發(fā)現(xiàn)，在整個(gè)協(xié)議中只存在RP對(duì)令牌端點(diǎn)的認(rèn)證性且用戶口令無秘密性。令牌端點(diǎn)對(duì)RP、EU對(duì)授權(quán)服務(wù)器及授權(quán)服務(wù)器對(duì)EU均無認(rèn)證性。關(guān)于令牌端點(diǎn)對(duì)RP的認(rèn)證性，攻擊者通過函數(shù)tuple能獲取到通信時(shí)的消息參數(shù)(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)進(jìn)而展開攻擊，從而使令牌端點(diǎn)對(duì)RP無認(rèn)證性。同理，關(guān)于EU對(duì)授權(quán)服務(wù)器及授權(quán)服務(wù)器對(duì)EU的認(rèn)證性，攻擊者都能獲取到通信相關(guān)的消息參數(shù)進(jìn)而發(fā)起攻擊使得它們不具有相互認(rèn)證性。對(duì)于用戶口令password，根據(jù)ProVerif結(jié)果發(fā)現(xiàn)，攻擊者能截取到password，故用戶口令無秘密性。

本文的研究對(duì)象和文獻(xiàn)[18]相同，但本文的工作與文獻(xiàn)[18] 的區(qū)別有以下4個(gè)方面：

1)文獻(xiàn)[18]的形式化建模語言采用的是基于計(jì)算模型的Blanchet演算，而本文采用的是基于符號(hào)模型的應(yīng)用PI演算。

2)文獻(xiàn)[18]使用的軟件工具是CryptoVerif，而本文所使用的工具是ProVerif。

3)分析結(jié)論方面，文獻(xiàn)[18]針對(duì)終端用戶與授權(quán)服務(wù)器不具相互認(rèn)證性及令牌端點(diǎn)對(duì)RP不具認(rèn)證性提出了使用數(shù)字簽名來解決認(rèn)證性不完整的缺陷的方法，但只指出了對(duì)某個(gè)參數(shù)進(jìn)行簽名來達(dá)到完善認(rèn)證性的目的。例如文獻(xiàn)[18]為了完善令牌端點(diǎn)對(duì)RP的認(rèn)證性，指出當(dāng)RP發(fā)送令牌請(qǐng)求消息時(shí)只對(duì)授權(quán)碼code進(jìn)行簽名，令牌端點(diǎn)收到包含該簽名的消息之后對(duì)該簽名進(jìn)行驗(yàn)證，若驗(yàn)證通過則實(shí)現(xiàn)了令牌端點(diǎn)對(duì)RP的認(rèn)證。但是在標(biāo)準(zhǔn)的OpenID Connect中，令牌請(qǐng)求消息還包含了重定向地址redirect_uri、RP與OP共享密碼client_secret等必需參數(shù)，若它們被攻擊者截獲利用，那么整個(gè)系統(tǒng)將面臨被攻擊的危險(xiǎn)。而本文采用對(duì)各個(gè)消息的每個(gè)必需參數(shù)進(jìn)行簽名從而完善協(xié)議的認(rèn)證性。

4)文獻(xiàn)[18]沒有關(guān)注用戶口令password的秘密性，而本文關(guān)注了用戶口令的秘密性且就password秘密性不強(qiáng)的缺陷使用非對(duì)稱加密技術(shù)對(duì)其進(jìn)行改進(jìn)。

因此本文使用數(shù)字簽名及非對(duì)稱加密技術(shù)，加強(qiáng)了用戶口令的秘密性以及完善了協(xié)議中通信三方之間的相互認(rèn)證性。在符號(hào)模型下應(yīng)用應(yīng)用PI演算對(duì)改進(jìn)的OpenID Connect協(xié)議進(jìn)行形式化建模并轉(zhuǎn)化為ProVerif的輸入并在ProVerif中執(zhí)行。建模分析結(jié)果表明用戶口令的秘密性和協(xié)議通信三方的相互認(rèn)證性得到完善。

對(duì)于用戶口令，終端用戶通過OP的公鑰加密用戶口令后得到密文，然后再將此密文與用戶名一起簽名后通過授權(quán)消息發(fā)送到授權(quán)服務(wù)器，在授權(quán)服務(wù)器端進(jìn)行簽名確認(rèn)及私鑰解密的操作，整個(gè)過程攻擊者無法獲取到口令，保證了用戶口令的秘密性。在終端用戶與授權(quán)服務(wù)器之間的相互認(rèn)證方面，因?yàn)槭跈?quán)服務(wù)器需要向終端用戶發(fā)送認(rèn)證請(qǐng)求消息并且終端用戶需要響應(yīng)此消息并返回響應(yīng)消息給授權(quán)服務(wù)器，在這兩個(gè)消息中，本文均對(duì)各自的參數(shù)進(jìn)行了數(shù)字簽名，并且在對(duì)方收到簽名消息后都驗(yàn)證了簽名，這就使終端用戶與授權(quán)服務(wù)器之間相互認(rèn)證得到驗(yàn)證。在授權(quán)服務(wù)器與RP方的相互認(rèn)證方面，因?yàn)镽P首先需要發(fā)送用自己私鑰簽名的訪問認(rèn)證請(qǐng)求消息給授權(quán)服務(wù)器，授權(quán)服務(wù)器收到這個(gè)簽名的認(rèn)證消息后，首先用RP的公鑰驗(yàn)證簽名，再對(duì)這個(gè)請(qǐng)求作出響應(yīng)，然后再把認(rèn)證后的結(jié)果用自己私鑰數(shù)字簽名后發(fā)送給RP，RP收到該消息后用授權(quán)服務(wù)器公鑰驗(yàn)證該簽名，這樣使授權(quán)服務(wù)器和RP之間的認(rèn)證性得到驗(yàn)證。在RP與令牌端點(diǎn)之間的相互認(rèn)證性方面，因?yàn)镽P需要發(fā)送令牌請(qǐng)求消息到令牌端點(diǎn)，當(dāng)令牌端點(diǎn)收到這個(gè)請(qǐng)求消息后需要對(duì)該請(qǐng)求消息作出響應(yīng)，所以本文對(duì)令牌請(qǐng)求消息和請(qǐng)求響應(yīng)消息中的所有參數(shù)都進(jìn)行了數(shù)字簽名，當(dāng)對(duì)方收到消息后都對(duì)簽名進(jìn)行驗(yàn)證，這樣就驗(yàn)證了令牌端點(diǎn)和RP之間的相互認(rèn)證性。

下階段工作主要是將改進(jìn)的協(xié)議應(yīng)用到實(shí)際的網(wǎng)絡(luò)環(huán)境中去，在實(shí)際應(yīng)用中發(fā)現(xiàn)攻擊與漏洞并逐步完善OpenID Connect協(xié)議。

References)

[1] 李雄.多種環(huán)境下身份認(rèn)證協(xié)議的研究與設(shè)計(jì)[D]. 北京：北京郵電大學(xué),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] 張煥國(guó),韓文報(bào),來學(xué)嘉,等. 網(wǎng)絡(luò)空間安全綜述[J]. 中國(guó)科學(xué):信息科學(xué),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] 高煥芝.單點(diǎn)登錄技術(shù)的研究[D]. 北京：北京郵電大學(xué),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.

[11] 來學(xué)嘉,盧明欣,秦磊,等. 基于DNA技術(shù)的非對(duì)稱加密與簽名方法[J]. 中國(guó)科學(xué):信息科學(xué),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] 卓先德,趙菲,曾德明. 非對(duì)稱加密技術(shù)研究[J]. 四川理工學(xué)院學(xué)報(bào)(自然科學(xué)版),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.

[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.

[17] 馮超,張權(quán),唐朝京. 計(jì)算可靠的Diffie-Hellman密鑰交換協(xié)議自動(dòng)證明[J]. 通信學(xué)報(bào),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] 孟博，張金麗，魯金鈿.基于計(jì)算模型的OpenID Connect協(xié)議認(rèn)證性的自動(dòng)化分析[J].中南民族大學(xué)學(xué)報(bào)(自然科學(xué)版), 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.)

This work is partially supported by the National Natural Science Foundation of China (61272497), the Natural Science Foundation of Hubei Province (2014CFB249).

LU Jintian, born in 1991, M. S. candidate. His research interests include formal analysis and reverse engineering of network protocol.

YAO Lili, born in 1993, M. S. candidate. Her research interests include data storage security.

HE Xudong, born in 1991, M. S. candidate. His research interests include security architecture and protocol.

MENG Bo, born in 1974, Ph. D., professor. His research interests include cyberspace security.

Improvement of OpenID Connect protocol and its security analysis

LU Jintian, YAO Lili, HE Xudong, MENG Bo*

(CollegeofComputerScience,South-CentralUniversityforNationalities,WuhanHubei430074,China)

OpenID Connect protocol is widely used in identity authentication field and is one of the newest single sign-on protocols. In this paper, the digital signature and asymmetric encryption were used to improve OpenID connect protocol. The secrecy and authentication of the improved protocol were focused. And then the improved OpenID connect protocol was formalized with the applied PI calculus in the symbolic model, next the secrecy was modeled by query and the authentication was modeled by non-injective relations to test the secrecy and authentication of improved OpenID Connect protocol. Finally the formal model of the OpenID Connect protocol was transformed into the input of the automatic tool ProVerif based on symbol model. The results indicate that the improved OpenID Connect protocol is authenticable and secret.

aasymmetric encryption; digital signature; authentication; symbol model; formal method; ProVerif

2016-10-08;

2016-12-28。

國(guó)家自然科學(xué)基金資助項(xiàng)目(61272497)；湖北省自然科學(xué)基金資助項(xiàng)目(2014CFB249)。

魯金鈿(1991—)，男，湖南湘西人，碩士研究生，主要研究方向：網(wǎng)絡(luò)協(xié)議形式化及逆向分析; 堯利利(1993—)，女，江西撫州人，碩士研究生，主要研究方向：數(shù)據(jù)存儲(chǔ)安全； 何旭東(1991—)，男，湖北武漢人，碩士研究生，主要研究方向：安全體系結(jié)構(gòu)與協(xié)議； 孟博(1974—),男,河北石家莊人,教授,博士,主要研究方向：網(wǎng)絡(luò)空間安全。

1001-9081(2017)05-1347-06

10.11772/j.issn.1001-9081.2017.05.1347

TP393.08

A