孟　博，張金麗，魯金鈿

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

?

基于計算模型的OpenID Connect協(xié)議認(rèn)證性的自動化分析

孟博，張金麗，魯金鈿

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

分析了OpenID Connect協(xié)議的消息結(jié)構(gòu)，基于計算模型應(yīng)用Blanchet演算對OpenID Connect協(xié)議進(jìn)行了形式化建模，應(yīng)用自動化驗(yàn)證工具CryptoVerif驗(yàn)證了其認(rèn)證性.結(jié)果表明：在OpenID Connect協(xié)議中，客戶端能夠認(rèn)證終端用戶，但是終端用戶與授權(quán)服務(wù)器之間不能相互認(rèn)證、令牌終端不能認(rèn)證客戶端.為此，給出了OpenID Connect協(xié)議中不具有認(rèn)證性問題的解決方法.

OpenID Connect協(xié)議；計算模型；自動化驗(yàn)證；認(rèn)證性

OpenID Connect[1]是2014年發(fā)布的OpenID最新的用戶身份認(rèn)證及分布式身份系統(tǒng)標(biāo)準(zhǔn)，是非常重要的單點(diǎn)登錄認(rèn)證協(xié)議標(biāo)準(zhǔn)之一，建立于OAuth2.0[2]協(xié)議的基礎(chǔ)之上，引入了一個抽象為身份令牌ID Token的身份層，用來將用戶的認(rèn)證信息由OpenID供應(yīng)商傳送到客戶端[3].基于OpenID Connect協(xié)議，客戶端可以直接為用戶提供登錄服務(wù)，而客戶端無需在自己的服務(wù)器中存儲及管理用戶密碼，從而再也不必?fù)?dān)心用戶的賬戶安全.OpenID Connect協(xié)議一經(jīng)推出便獲得了雅虎、谷歌、微軟及多家其他公司的支持[4]，人們也開始對其安全性進(jìn)行分析，目前主要集中在實(shí)際應(yīng)用方面，文獻(xiàn)[5-8]通過各種不同的分析方式，提出了OpenID Connect協(xié)議在實(shí)際應(yīng)用中可能存在307重定向攻擊、OpenID供應(yīng)商混淆客戶端攻擊、網(wǎng)頁仿冒、網(wǎng)絡(luò)釣魚攻擊等各種不安全因素.

本文對OpenID Connect協(xié)議安全性的分析集中在協(xié)議本身，基于計算模型[9]對OpenID Connect協(xié)議的認(rèn)證性進(jìn)行自動化分析.首先分析OpenID Connect協(xié)議的消息結(jié)構(gòu)，然后利用Blanchet演算[10]來對OpenID Connect協(xié)議進(jìn)行建模，最后通過自動化驗(yàn)證工具CryptoVerif[11]分析其認(rèn)證性，并根據(jù)認(rèn)證結(jié)果提出了解決問題的建議.

1　OpenID Connect協(xié)議的消息結(jié)構(gòu)

OpenID Connect協(xié)議身份認(rèn)證有3種類型：授權(quán)碼流、隱式流、混合流，本文中對OpenID Connect協(xié)議的分析選取的身份認(rèn)證方式是授權(quán)碼流認(rèn)證方式，基于該方式的所有令牌都從令牌終端返回，授權(quán)服務(wù)器向客戶端發(fā)送授權(quán)碼，隨后客戶端可以利用這個授權(quán)碼直接從令牌終端獲得身份令牌和訪問令牌，這樣就可以成功地避免將令牌暴露給用戶代理或者其他能夠訪問用戶代理的惡意應(yīng)用程序.采用授權(quán)碼流認(rèn)證方式的OpenID Connect協(xié)議消息流程如圖1所示.

圖1　OpenID Connect協(xié)議消息結(jié)構(gòu)Fig.1 The structure of message of OpenID Connect Protocol

1.1客戶端向授權(quán)服務(wù)器發(fā)送認(rèn)證請求

如果客戶端需要訪問受保護(hù)的終端用戶的資源，就需要向OpenID供應(yīng)商的授權(quán)服務(wù)器發(fā)送認(rèn)證請求，認(rèn)證請求中必須包含域值scope、響應(yīng)類型參數(shù)response_type、客戶端標(biāo)識符client_id、客戶端重定向URI redirect_uri和狀態(tài)參數(shù)state.在發(fā)送認(rèn)證請求時，這些參數(shù)作為OpenID供應(yīng)商的重定向URI的數(shù)據(jù)請求參數(shù)，Web瀏覽器通過HTTP機(jī)制重定向到OpenID供應(yīng)商的授權(quán)服務(wù)器.OpenID供應(yīng)商收到客戶端的認(rèn)證請求之后，授權(quán)服務(wù)器通過核查請求中是否包含必備參數(shù)，并且這些參數(shù)的用法是否符合協(xié)議規(guī)范來驗(yàn)證該請求是否有效.如果請求有效，則授權(quán)服務(wù)器根據(jù)請求中使用的參數(shù)值來做出響應(yīng);否則，授權(quán)服務(wù)器必須返回一個錯誤響應(yīng).

1.2授權(quán)服務(wù)器認(rèn)證終端用戶并獲得授權(quán)

當(dāng)授權(quán)服務(wù)器需要認(rèn)證終端用戶并獲得授權(quán)時，就向終端用戶發(fā)送請求認(rèn)證消息Authentication_Message，請求認(rèn)證資源擁有者的身份.終端用戶收到認(rèn)證請求消息Authentication_Message后，若同意授權(quán)，則向授權(quán)服務(wù)器發(fā)送自己的用戶名和密碼.授權(quán)服務(wù)器收到該用戶名和密碼后，與其存儲的用戶名和密碼進(jìn)行驗(yàn)證，如果驗(yàn)證成功，則表明授權(quán)服務(wù)器已成功認(rèn)證終端用戶并獲得終端用戶的授權(quán).

1.3授權(quán)服務(wù)器響應(yīng)認(rèn)證請求

當(dāng)授權(quán)服務(wù)器獲得終端用戶的授權(quán)之后，生成授權(quán)碼code，并將其與認(rèn)證請求中的客戶端標(biāo)識符和重定向URI進(jìn)行綁定，然后將產(chǎn)生的授權(quán)碼code和認(rèn)證請求中的參數(shù)state作為請求參數(shù)添加到客戶端的重定向URI中，Web瀏覽器通過HTTP機(jī)制重定向到客戶端，從而將產(chǎn)生的授權(quán)碼code發(fā)送到客戶端.如果終端用戶認(rèn)證失敗或者終端用戶不同意授權(quán)，授權(quán)服務(wù)器需要通過認(rèn)證請求中的重定向URI向客戶端返回錯誤提示信息.

1.4客戶端發(fā)送令牌請求

當(dāng)客戶端獲得授權(quán)服務(wù)器發(fā)送的授權(quán)碼之后，需要向OpenID供應(yīng)商發(fā)送令牌請求，將授權(quán)許可類型grant_type(在授權(quán)碼流中，它的值為“authorization_code”)、授權(quán)服務(wù)器發(fā)送的授權(quán)碼code、client_id和client_secret、客戶端重定向URI redirect_uri一起作為令牌請求參數(shù)，添加到OpenID供應(yīng)商的URI中，發(fā)送給OpenID供應(yīng)商，從而獲得已經(jīng)授權(quán)的終端用戶的身份令牌和訪問令牌.只有獲得了訪問令牌，客戶端才能夠訪問終端用戶的資源.

1.5令牌終端響應(yīng)令牌請求

OpenID供應(yīng)商的令牌終端接收到客戶端的令牌請求之后，需要驗(yàn)證客戶端的身份憑證，確?？蛻舳藰?biāo)識符和密碼正確且存在綁定關(guān)系；驗(yàn)證授權(quán)碼是否有效，并且，授權(quán)碼是否發(fā)送給了得到授權(quán)的客戶端，即授權(quán)碼與客戶端標(biāo)識符和客戶端重定向URI是否存在綁定關(guān)系；驗(yàn)證令牌請求中的客戶端地址與認(rèn)證請求中的客戶端地址是否相同；驗(yàn)證授權(quán)碼是用來響應(yīng)OpenID Connect認(rèn)證請求而發(fā)布的，從而決定令牌終端響應(yīng)令牌請求時是否需要發(fā)送身份令牌.當(dāng)確認(rèn)客戶端發(fā)送的令牌請求有效且該客戶端得到了終端用戶的授權(quán)，OpenID供應(yīng)商的令牌終端對客戶端返回令牌請求響應(yīng)，即向客戶端發(fā)送身份令牌id_token、訪問令牌access_token、令牌類型參數(shù)token_type(值為“Bearer”)、訪問令牌的有效期限espires_in及域值scope.身份令牌即ID Token，用來將用戶的認(rèn)證信息從授權(quán)服務(wù)器發(fā)送到客戶端.訪問令牌即Access Token，客戶端可以通過向OpenID供應(yīng)商的用戶信息終端發(fā)送訪問令牌來訪問得到授權(quán)的終端用戶的資源.

2　應(yīng)用Blanchet演算對OpenID Connect協(xié)議建模

應(yīng)用Blanchet演算，對OpenID Connect協(xié)議進(jìn)行建模，Blanchet演算可以得到自動化驗(yàn)證工具CryptoVerif的支持.通道是數(shù)據(jù)傳遞的重要媒介，所有的數(shù)據(jù)都是通過通道在不同實(shí)體之間進(jìn)行傳輸，建模時首先要對通道進(jìn)行定義.在OpenID Connect協(xié)議中，身份令牌ID Token必須通過JWS進(jìn)行簽名，需要引用數(shù)字簽名技術(shù)，這里選用CryptoVerif中預(yù)先定義的一個具有較強(qiáng)抵抗選擇消息攻擊能力的概率公鑰簽名算法SUF_CMA_signature.

2.1認(rèn)證性

利用Blanchet演算進(jìn)行安全協(xié)議建模時，首先要對事件進(jìn)行聲明，并給出最終需要證明的目標(biāo)，這個目標(biāo)主要是針對不同實(shí)體之間的認(rèn)證性，這里采用非單射一致性來建模認(rèn)證性，認(rèn)證性證明目標(biāo)如表1所示.

表1　認(rèn)證性目標(biāo)

2.2主進(jìn)程process

在OpenID Connect協(xié)議建模的主進(jìn)程process中，首先要利用new語句生成一個keyseed類型隨機(jī)數(shù)signseed，作為數(shù)字簽名密鑰種子，然后將signseed作為函數(shù)參數(shù)，調(diào)用概率公鑰簽名算法SUF_CMA_signature中的公鑰、私鑰生成函數(shù)pkgen()、skgen()，生成ID Token進(jìn)行數(shù)字簽名時所需要的公鑰signpkey和私鑰signskey，并將signpkey通過通道c發(fā)送.最后，采用((!N OP_Process)|(!N1 Client_Process)|(!N2 End_User_Process))這個多個進(jìn)程并發(fā)執(zhí)行語句模擬OpenID Connect協(xié)議執(zhí)行，其中，OP_Process、Client_Process、End_User_Process進(jìn)程分別用于模擬OpenID供應(yīng)商、客戶端、終端用戶.主進(jìn)程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終端用戶進(jìn)程End_User_Process

當(dāng)終端用戶由通道c10接收到來自O(shè)penID供應(yīng)商的消息string_from_OP后，需要判斷消息的具體內(nèi)容，當(dāng)消息是請求認(rèn)證授權(quán)ask_for_authentication時，表明OpenID供應(yīng)商請求認(rèn)證用戶并獲得授權(quán).終端用戶同意授權(quán)，通過通道c11向OpenID供應(yīng)商發(fā)送自己的用戶名user_name和密碼user_password.終端用戶進(jìn)程End_User_Process建模關(guān)鍵部分如下：

c10 (=OpenIDP_one,string_from_OP:bitstring);

if string_from_OP=ask_for_authentication then

2.4客戶端進(jìn)程Client_Process

當(dāng)客戶端需要訪問終端用戶的資源時，利用new語句生成返回類型參數(shù)responsetype、會話狀態(tài)參數(shù)state_one、openid域值參數(shù)scope_one，并將這些參數(shù)與客戶端標(biāo)識符id_client和重定向地址uri_client一起，作為認(rèn)證請求參數(shù)通過通道c7發(fā)送給OpenID供應(yīng)商.客戶端由通道c14接收到OpenID供應(yīng)商發(fā)送的授權(quán)碼code_from_OP之后，為了能夠訪問終端用戶的資源，還需要向OpenID供應(yīng)商發(fā)送令牌請求，利用new語句生成許可類型參數(shù)granttype_one，并將其與code_from_OP、uri_client、id_client、secret_client一起作為令牌請求參數(shù)通過通道c15發(fā)送給OpenID供應(yīng)商.當(dāng)OpenID供應(yīng)商成功驗(yàn)證令牌請求參數(shù)之后，會向客戶端返回身份令牌ID Token和訪問令牌Access Token.客戶端由通道c17接收簽名信息message、簽名結(jié)果sign_one_s、訪問令牌accesstoken_one、訪問令牌類型tokentype_one、令牌有效期限expiresin_one等參數(shù)，然后通過check()函數(shù)驗(yàn)證簽名是否有效，并通過let賦值語句獲得身份令牌idtoken_one.當(dāng)客戶端獲得訪問令牌之后，就可以與用戶信息終端進(jìn)行交互，從而訪問受保護(hù)終端用戶的資源.客戶端進(jìn)程Client_Process建模關(guān)鍵部分如下：

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供應(yīng)商進(jìn)程OP_Process

OpenID供應(yīng)商由通道c8接收到包含域值scope_two、返回類型responsetype_two、客戶端標(biāo)識符clientid_two、客戶端重定向地址uri_two及會話狀態(tài)參數(shù)state_two這些請求參數(shù)的認(rèn)證請求之后，首先利用find語句、combine2()函數(shù)來判斷clientid_two與uri_two是否存在綁定關(guān)系，若存在綁定關(guān)系，則確定該認(rèn)證請求是否由客戶端本身發(fā)送.在使用授權(quán)碼流時，responsetype_two值應(yīng)該為“code”，判斷responsetype_two的值是否為“code”，如果滿足，授權(quán)服務(wù)器將認(rèn)證終端用戶，通過通道c9將認(rèn)證請求消息ask_for_authentication發(fā)送給終端用戶.授權(quán)服務(wù)器由通道c12接收終端用戶的認(rèn)證響應(yīng)，即用戶名user和密碼pass，通過find語句查詢是否存在該user，并且利用combine3()函數(shù)判定user與pass是否存在綁定關(guān)系.如果這兩個條件均滿足，則說明終端用戶同意授權(quán)，授權(quán)服務(wù)器利用new語句生成授權(quán)碼auth_code，并通過combine4()函數(shù)將auth_code與clientid_two、uri_two進(jìn)行綁定后存儲到clientid_code中.最后，授權(quán)服務(wù)器將授權(quán)碼auth_code與狀態(tài)參數(shù)state_two一起通過通道c13發(fā)送給客戶端，從而完成對客戶端認(rèn)證請求響應(yīng).建模部分關(guān)鍵代碼如下：

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);

若仔細(xì)考察杰克·倫敦的其他作品，會發(fā)現(xiàn)其中蘊(yùn)含著大同小異的意識形態(tài)立場。以《海狼》(1904)為代表，得出結(jié)論：弱者終于戰(zhàn)勝了強(qiáng)者，文明終于戰(zhàn)勝了野蠻(王寧、張艷紅2010：124)。以《白牙》（1906）為代表，白牙的整個成長過程充滿痛苦和挫折，最后在人類愛的感召下變成了一只忠實(shí)的“狗”,表現(xiàn)出作者強(qiáng)調(diào)博愛與毅力對人類發(fā)展的重要性(李智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

當(dāng)OpenID供應(yīng)商的令牌終端由c16接收包含許可類型grant_type_two、授權(quán)碼code_from_client、客戶端重定向地址client_uri_three、客戶端標(biāo)識符clientid_three、客戶端登錄密碼client_secret_three這些參數(shù)的令牌請求，首先要判斷grant_type_two參數(shù)的值是否為“authorization_code”.如果是，判斷接收到的client_uri_three與認(rèn)證請求中的uri_two是否相同，若相同，則表明認(rèn)證請求與令牌請求來自于同一個用戶.然后利用3個find語句驗(yàn)證clientid_three與client_secret_three是否匹配、code_from_client是否存在且與clientid_three、client_uri_three存在綁定關(guān)系.若這些驗(yàn)證都成功，令牌終端需要向客戶端返回對令牌請求的響應(yīng).首先利用new語句生成身份令牌idtoken、訪問令牌accesstoken、訪問令牌類型tokentype、令牌有效期限expiresin這些必要參數(shù).然后利用new需要生成隨機(jī)數(shù)seed_one，通過combine5()函數(shù)將idtoken存儲在簽名信息signmessage中，并利用簽名算法SUF_CMA_signature中的簽名函數(shù)sign()對其簽名，結(jié)果存儲在sign_one中，然后通過通道c17將signmessage、sign_one、accesstoken、tokentype、expiresin和認(rèn)證請求中的scope_two一起發(fā)送給客戶端.此部分建模關(guān)鍵代碼如下：

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驗(yàn)證OpenID Connect協(xié)議的認(rèn)證性

自動化驗(yàn)證工具CryptoVerif對安全協(xié)議的證明依賴于一系列的Game轉(zhuǎn)換[12].將基于Blanchet演算的OpenID Connect協(xié)議代碼轉(zhuǎn)換成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語法代碼輸入自動化驗(yàn)證工具CryptoVerif中，得到OpenID Connect協(xié)議模型分析結(jié)果如圖2、圖3、圖4、圖5所示.

圖2　event UserAuth(x)?Authentication(x)證明的結(jié)果Fig.2　Result of proof event UserAuth(x)?Authentication(x)

由圖2可知，對一致性關(guān)系event UserAuth(x)?Authentication(x)的證明結(jié)果為RESULT Could not prove event UserAuth(x)?Authentication(x)，表明終端用戶無法認(rèn)證授權(quán)服務(wù)器.經(jīng)過分析可知，授權(quán)服務(wù)器向終端用戶發(fā)送認(rèn)證請求消息ask_for_authentication時，并沒有采用一定的安全策略.為了解決終端用戶無法認(rèn)證授權(quán)服務(wù)器的問題，授權(quán)服務(wù)器發(fā)送認(rèn)證請求消息ask_for_authentication時，可以利用其簽名私鑰對ask_for_authentication進(jìn)行數(shù)字簽名.終端用戶接收到認(rèn)證請求消息之后，利用授權(quán)服務(wù)器的簽名公鑰驗(yàn)證簽名，從而實(shí)現(xiàn)對授權(quán)服務(wù)器的認(rèn)證.

圖3　event Authorization(x)?User(x)證明的結(jié)果Fig.3　Result of proof event Authorization(x)?User(x)

由圖3可知，對一致性關(guān)系event Authorization(x)?User(x)的證明結(jié)果為RESULT Could not prove event Authorization(x)?User(x)，表明授權(quán)服務(wù)器無法認(rèn)證終端用戶.經(jīng)過分析可知，終端用戶同意授權(quán)，向授權(quán)服務(wù)器發(fā)送用戶名和密碼時，并沒有采用一定的安全策略.為了解決授權(quán)服務(wù)器無法認(rèn)證終端用戶的問題，終端用戶向授權(quán)服務(wù)器發(fā)送用戶名user_name和密碼user_password時，可以利用其簽名私鑰對user_name和user_password進(jìn)行數(shù)字簽名.授權(quán)服務(wù)器接收到授權(quán)響應(yīng)之后，利用終端用戶的簽名公鑰驗(yàn)證簽名，從而實(shí)現(xiàn)對終端用戶的認(rèn)證.

圖4　event TokenEnd(x)?client(x)證明的結(jié)果Fig.4　Result of proof event TokenEnd(x)?client(x)

由圖4可知，對一致性關(guān)系event TokenEnd(x)?client(x)的證明結(jié)果為RESULT Could not prove event TokenEnd(x)?client(x)，表明令牌終端無法認(rèn)證客戶端.經(jīng)過分析可知，客戶端向令牌終端發(fā)送令牌請求的過程中，請求參數(shù)并沒有采用一定的安全策略.為了解決令牌終端無法認(rèn)證客戶端的問題，客戶端發(fā)送令牌請求時，可以利用其簽名私鑰對授權(quán)碼code_from_OP進(jìn)行數(shù)字簽名.令牌終端接收到令牌請求之后，利用客戶端的簽名公鑰驗(yàn)證簽名，從而實(shí)現(xiàn)對客戶端的認(rèn)證.

由圖5可知，對一致性關(guān)系event IDTokenClient(y)?IDTokenEnd(x)的證明結(jié)果為All queries proved，表明客戶端能夠認(rèn)證令牌終端.分析可知，令牌終端向客戶端發(fā)送令牌響應(yīng)時，身份令牌采用令牌終端的私鑰進(jìn)行了JWS簽名，接收到身份令牌的客戶端必須用令牌終端的公鑰解密簽名信息，獲得身份令牌，所以客戶端能夠認(rèn)證令牌終端的身份.

針對不具有認(rèn)證性的缺陷，提出了相應(yīng)的解決方法，并采用形式化建模的方式證明了解決方法的可行性和正確性.

圖5　event IDTokenClient(y)?IDTokenEnd(x)證明的結(jié)果Fig.5　Result of proof event IDTokenClient(y)?IDTokenEnd(x)

4　結(jié)語

為了研究OpenID Connect協(xié)議的實(shí)體之間是否具有認(rèn)證性，本文通過對OpenID Connect協(xié)議消息流中的數(shù)據(jù)項進(jìn)行分析，得到其整體的消息結(jié)構(gòu)，然后利用Blanchet演算對OpenID Connect協(xié)議消息流程進(jìn)行建模，并將建模語句導(dǎo)入自動化驗(yàn)證工具CryptoVerif中進(jìn)行自動化分析.分析結(jié)果表明：OpenID Connect協(xié)議中終端用戶與授權(quán)服務(wù)器之間無法相互認(rèn)證、令牌終端無法認(rèn)證客戶端，但客戶端能夠認(rèn)證令牌終端，因?yàn)榱钆平K端向客戶端發(fā)送令牌響應(yīng)的過程中采用了數(shù)字簽名機(jī)制，而其他實(shí)體之間進(jìn)行消息傳遞的時候并沒有采取一定的安全策略，并不能保證實(shí)體之間的相互認(rèn)證.在OpenID Connect協(xié)議標(biāo)準(zhǔn)中規(guī)定，所有與OpenID供應(yīng)商的通信操作必須建立在TLS機(jī)制之上，希望借此來保證安全性.然而，我們考慮的是，啟用TLS機(jī)制的開銷比較大、布署起來比較麻煩，并且在協(xié)議中已經(jīng)存在用于保證實(shí)體認(rèn)證性的數(shù)字簽名機(jī)制.因此，如果要通過數(shù)字簽名機(jī)制來解決協(xié)議中不存在認(rèn)證性的問題，在技術(shù)上是可以實(shí)現(xiàn)的，本文也給出了相應(yīng)的解決方案.

[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]薛銳, 雷新鋒. 安全協(xié)議:信息安全保障的靈魂-安全協(xié)議分析研究現(xiàn)狀與發(fā)展趨勢[J]. 中國科學(xué)院院刊, 2011, 26(3):287-296.

[10]孟博, 王德軍. 安全遠(yuǎn)程網(wǎng)絡(luò)投票協(xié)議[M]. 北京：科學(xué)出版社，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]邵飛．基于概率進(jìn)程演算的安全協(xié)議自動化分析技術(shù)研究[D]. 武漢：中南民族大學(xué)，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-)，男，教授，博士后，研究方向：網(wǎng)絡(luò)空間安全，E-mail: mengscuec@gmail.com

湖北省自然科學(xué)基金資助項目(2014CFB249)

TP309

A

1672-4321(2016)03-0123-07