改進的OpenID Connect協議及其安全性分析

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

(中南民族大學 計算機科學學院，武漢 430074)

改進的OpenID Connect協議及其安全性分析

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

(中南民族大學 計算機科學學院，武漢 430074)

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

OpenID Connect協議是最新的單點登錄協議之一，已經廣泛應用于用戶身份認證領域，其安全性受到了人們的重點關注。為增強OpenID Connect協議的安全性，首先引入數字簽名及非對稱加密技術，對其進行改進，重點關注改進后協議的秘密性和認證性; 其次基于符號模型，應用應用PI演算對改進的OpenID Connect協議進行形式化建模; 然后為驗證改進后協議的認證性和秘密性，分別使用非單射性和query對認證性和秘密性進行建模; 最后把改進的OpenID Connect協議的應用PI演算模型轉換為安全協議分析工具ProVerif的輸入，應用ProVerif對其進行形式化分析。實驗結果表明，改進后的OpenID Connect協議具有認證性和秘密性。

非對稱加密；數字簽名；認證性；符號模型；形式化方法；ProVerif

0 引言

身份認證[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.1 RP認證請求

為訪問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 改進的OpenID Connect協議消息結構Fig. 1 Procedure of modified OpenID Connect protocol

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對令牌端點的認證性。

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

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

圖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對令牌端點的認證性得到驗證。

圖2 改進的OpenID Connect協議ProVerif輸入Fig. 2 Inputs of modified OpenID connect protocol

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

圖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對授權服務器的認證性得到驗證。

圖4 RP與Token Endpoint相互認證結果Fig. 4 Authentication between RP and Token Endpoint

圖5 授權服務器與RP相互認證結果Fig. 5 Authentication between authorization server and 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對授權服務器的認證性得到驗證。

圖6 授權服務器與EU相互認證結果Fig. 6 Authentication between authorization server and 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協議。

References)

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

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

[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] 馮超,張權,唐朝京. 計算可靠的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.)

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。

國家自然科學基金資助項目(61272497)；湖北省自然科學基金資助項目(2014CFB249)。

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

1001-9081(2017)05-1347-06

10.11772/j.issn.1001-9081.2017.05.1347

TP393.08

A