基于符號模型自動分析隱私保留的用戶認(rèn)證協(xié)議安全性

孟博，唐獲野，陳雙

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

隨著大數(shù)據(jù)[1,2]及其應(yīng)用的快速發(fā)展，應(yīng)用大數(shù)據(jù)挖掘和分析[3,4]可以發(fā)現(xiàn)許多敏感信息，如：用戶隱私信息、健康數(shù)據(jù)和醫(yī)療保健信息等，因此大數(shù)據(jù)安全和隱私[5-7]受到了人們的重點關(guān)注，研究重點是保留用戶隱私的身份認(rèn)證協(xié)議.

目前人們提出了許多面向大數(shù)據(jù)的用戶身份認(rèn)證協(xié)議[8-12].2012年，基于用戶筆跡模式特征和用戶口令，Omri等[8]提出安全地訪問云；2013年，應(yīng)用基于ID /密碼、移動識別號碼和用戶生物信息，Jeong等[9]提出了移動云計算的多因素身份認(rèn)證協(xié)議，實現(xiàn)了智能設(shè)備和服務(wù)器集群的相互認(rèn)證并且提高了認(rèn)證的性能；面向移動設(shè)備平臺，Dey等[10]應(yīng)用MDA(Message Digest Authentication)提出了一種身份認(rèn)證協(xié)議，實現(xiàn)了移動設(shè)備和云服務(wù)器的相互認(rèn)證；面向云計算環(huán)境，基于零知識認(rèn)證、數(shù)字簽名和模糊保險庫，Schwab and Yang[11]提出了一種面向移動用戶的FDZ認(rèn)證協(xié)議，用于驗證云計算環(huán)境中的移動設(shè)備.然而，這些工作沒有重點關(guān)注用戶隱私信息. 2016年，面向云環(huán)境，利用大數(shù)據(jù)特征，Vorugunti等[12]提出了一種隱私保護的多因素移動用戶身份認(rèn)證協(xié)議PPMUAS.據(jù)悉，它是第一個聲稱實現(xiàn)了用戶身份認(rèn)證和用戶隱私保護的認(rèn)證協(xié)議.Vorugunti聲稱該協(xié)議具有認(rèn)證性和隱私性.但是，沒有進行嚴(yán)格的分析和證明.應(yīng)用形式化方法，自動分析和驗證協(xié)議認(rèn)證性[13,14]已被廣泛使用.故此，基于符號模型，本文首先應(yīng)用Applied PI 演算對PPMUAS身份認(rèn)證協(xié)議進行形式化建模得到其形式化模型，然后分別使用非單射一致性和 Query 對認(rèn)證性和秘密性進行建模；最后把PPMUAS身份認(rèn)證協(xié)議的Applied PI 演算模型轉(zhuǎn)換為安全協(xié)議分析工具 ProVerif[15]的輸入，應(yīng)用 ProVerif 對其進行形式化分析，結(jié)果表明PPMUAS身份認(rèn)證協(xié)議具有秘密性，但不具有認(rèn)證性，最后給出了實現(xiàn)認(rèn)證性的方法.

1 PPMUAS認(rèn)證協(xié)議的消息結(jié)構(gòu)

PPMUAS協(xié)議包含3個實體：用戶User，認(rèn)證服務(wù)器As，數(shù)據(jù)庫DB.其協(xié)議消息結(jié)構(gòu)如圖1所示，主要包含6條通信消息.

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

1.1 用戶注冊請求

用戶User注冊時向認(rèn)證服務(wù)器發(fā)送一條注冊請求消息1 Registration request，該消息包含用戶身份碼Idi、 用戶代號i、用戶配置文件Cupi和Rpwi.Rpwi由哈希函數(shù)Hash對用戶口令Pwi、隨機數(shù)bi進行散列生成；Cupi由模糊哈希函數(shù)FuzzyHash和同態(tài)加密函數(shù)FH_Enc生成.模糊哈希函數(shù)FuzzyHash對Pwi，U_OlInfo和U_BrInfo進行散列，同態(tài)加密函數(shù)FH_Enc對U_KeySD，U_AMM和U_GM進行加密，最后把消息1發(fā)送給認(rèn)證服務(wù)器.

其中U_OlInfo是用戶在線信息、U_BrInfo是用戶瀏覽器信息、U_KeySD是用戶擊鍵動力學(xué)信息、U_AMM是加速度計測量信息、U_GM是陀螺儀測量信息.

1.2 認(rèn)證服務(wù)器注冊請求

認(rèn)證服務(wù)器接收到消息1 Registration request后，通過哈希函數(shù)Hash對Idi，Rpwi和i進行散列得到Vi并存儲到認(rèn)證服務(wù)器中；同時產(chǎn)生消息2 Authentication server request.該消息包含α，Rpupi和i.其中，α由隨機數(shù)ri和用戶特定秘鑰kn通過公鑰k1加密得到，Rpupi通過以下方法得到：首先通過置換函數(shù)Permute(P)重新排列用戶加密文件Cupi得到Pupi，再將Pupi與ri進行異或運算(XOR)，最后生成消息2發(fā)送給數(shù)據(jù)庫.數(shù)據(jù)庫用k1解密得到ri和kn.Pupi由Rpupi和ri通過XOR計算得到，最后將ri，kn和Pupi保存到數(shù)據(jù)庫，用戶的注冊完成.

1.3 用戶登錄請求

1.4 認(rèn)證服務(wù)器登錄請求

1.5 數(shù)據(jù)庫響應(yīng)

1.6 登錄響應(yīng)

認(rèn)證服務(wù)器在收到消息6 Login response，首先檢查消息參數(shù)，若是yes則允許用戶接入服務(wù)，否則拒絕用戶接入服務(wù).

2 應(yīng)用Applied PI演算對PPMUAS認(rèn)證協(xié)議形式化建模

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

函數(shù)和等式理論主要包含：公鑰算法包含加密算法aenc(x,Pu)和解密算法adec(y，Pu).aenc(x,Pu)對應(yīng)用公鑰Pu對消息x進行加密生成密文.adec(y,Pu)使用公鑰Pu對消息y解密得到明文.異或算法XOR(x,y)對消息x，y進行異或計算.漢明重量算法HW(x,y)對消息x，y進行漢明重量測量.置換函數(shù)P對消息x進行置換.其形式化建模如下：

2.2 進程

完整的PPMUAS協(xié)議進程主要包含：用戶進程processUser、認(rèn)證服務(wù)器進程processAs和數(shù)據(jù)庫進程processDB.它們共同構(gòu)成了主進程，具體表述如下：

使用Applied PI演算對用戶進程建模為processUser.

注冊階段，用戶進程使用new語句生成用戶的個人隱私信息.然后使用模糊哈希FuzzyHash和同態(tài)加密FH_Enc分別對參數(shù)進行計算，通過let in語句將生成的用戶個人隱私文件賦值給Cupi，同時將用戶輸入口令Pwi與隨機數(shù)bi進行哈希散列，散列值用let in語句賦值給Rpwi，最后通過公開信道c把注冊消息e發(fā)送給認(rèn)證服務(wù)器進程；

登錄階段，用戶再次執(zhí)行與注冊階段相同的工作，將登錄消息e′發(fā)送給認(rèn)證服務(wù)器進程.若登錄成功則會通過信道c接受到認(rèn)證服務(wù)器返回的登錄響應(yīng).processUser具體表述如下：

let processUser=

new U_OlInfo

new U_BrInfo

new U_KeySD

new U_AMM

new U_GM

let Rpwi=Hash(Pwi,bi) in

let e=(IDi, Rpwi, Cupi,i) in

out(c,e)

new U_OlInfo′

new U_BrInfo′

new U_KeySD′

new U_AMM′

new U_GM′

let Rpwi=Hash(Pwi,bi) in

out(c, e′)

in(c,ticket)

使用Applied PI演算對認(rèn)證服務(wù)器進程建模為processAs.

注冊階段，通過公開信道c收到消息m1，通過對Rpwi、用戶Idi和用戶代號i進行哈希運算得到散列值Vi并存儲在認(rèn)證服務(wù)器本地，同時用戶個人隱私文件Cupi通過P運算得到Pupi，Pupi與隨機數(shù)ri進行異或運算得到Rpupi，最后ri，kn與Pu(k1)做對稱加密得到α，通過公開信道c將α，Rpupi和i一起發(fā)送給數(shù)據(jù)庫；

let processAs=

in(c, m1)

new ri

new kn

let (IDi, Rpwi, Cupi,i)=m1in

let Vi=Hashone(IDi,Rpwi,i) in

let Pupi=P(Cupi) in

let Rpupi=XOR(Pupi,ri) in

let a=aenc((ri,kn),Pu(k1))in

let DB=(a,Rpupi,i) in

out(c, DB)

in(c, m3)

new yeah

new knn

out(c, DB′)

in(c, yes)

out(c, ticket)

使用Applied PI演算對數(shù)據(jù)庫服務(wù)器進程建模為processDB.

注冊階段，通過公開信道c收到消息m2，通過對稱解密adec(a,Pu(k1))得到ri和kn，然后異或運算得到Pupi，至此用戶完成在數(shù)據(jù)庫的注冊.

let processDB=

in(c,m2)

let(a,Rpupi,i)=m2in

let(ri,kn)=adec(a,Pu(k1)) in

let Pupi=XOR(Rpupi,ri) in

in(c,m4)

let (ri,knn)=adec(a′,Pu(kn)) in

new yes

out(c, yes)

3 利用ProVerif驗證PPMUAS認(rèn)證協(xié)

議的秘密性和認(rèn)證性

ProVerif應(yīng)用非單射一致性來建模認(rèn)證性，因此應(yīng)用ev: event one→ev:event two來建模認(rèn)證性.如果事件ev: event one被執(zhí)行，那么事件ev:event two必定被執(zhí)行.PPUMAS身份認(rèn)證協(xié)議認(rèn)證性建模如表1所示.同時，應(yīng)用ProVerif中query attacker:Pwi驗證用戶口令Pwi的秘密性.

表1 認(rèn)證模型Tab.1 Authentication model

ProVerif 的輸入有 Horn 子句和Applied PI 演算兩種方式，本文建模選擇Applied PI 演算作為輸入，Appied PI 演算輸入必須轉(zhuǎn)化為 ProVerif 的語法才能輸入到 ProVerif 工具運行，圖2為轉(zhuǎn)化后的 ProVerif 輸入及添加驗證認(rèn)證性的事件查詢.

4 分析結(jié)果

應(yīng)用ProVerif 運行PPMUAS協(xié)議的ProVerif格式的輸入，結(jié)果如圖3～圖5所示.query attacker：Pwi運行結(jié)果如圖3所示，其結(jié)果是true，證明用戶口令Pwi具有秘密性.因為用戶對口令Pwi進行哈希散列，得到的是口令摘要值，將摘要值發(fā)送給認(rèn)證服務(wù)器,攻擊者無法獲得口令.

圖3 Pwi秘密性Fig.3 Pwi secrecy

認(rèn)證服務(wù)器對數(shù)據(jù)庫的認(rèn)證結(jié)果是“cannot be proved”，表明認(rèn)證服務(wù)器不能實現(xiàn)對數(shù)據(jù)庫的認(rèn)證，因為數(shù)據(jù)庫返回給認(rèn)證服務(wù)器的消息Database response只有一個參數(shù)yes/no，并且消息沒采取安全機制，故攻擊者通過監(jiān)控公開信道可以直接發(fā)起冒充攻擊，因此，認(rèn)證服務(wù)器不能認(rèn)證數(shù)據(jù)庫服務(wù)器.

圖4 認(rèn)證服務(wù)器與數(shù)據(jù)庫相互認(rèn)證結(jié)果Fig.4 Mutual authentication results between authentication server and database

圖5(a)和(b)分別是認(rèn)證服務(wù)器對用戶認(rèn)證性和用戶對認(rèn)證服務(wù)器認(rèn)證性的建模分析結(jié)果，兩者的結(jié)果均為“cannot be proved”，說明認(rèn)證服務(wù)器和用戶之間不能相互認(rèn)證.因為用戶對發(fā)送給認(rèn)證服務(wù)器的消息3 Login request未作任何安全處理，攻擊者可以監(jiān)控公開信道，得到消息3的內(nèi)容，進而發(fā)起冒充攻擊，因此，不能實現(xiàn)認(rèn)證服務(wù)器認(rèn)證用戶；并且認(rèn)證服務(wù)器發(fā)送給用戶的消息6 Login response中只包含一個參數(shù)ticket/reject，并且消息未作任何安全處理，攻擊者通過監(jiān)控公開信道得到消息，進而發(fā)起冒充攻擊，因此不能實現(xiàn)用戶認(rèn)證認(rèn)證服務(wù)器.

圖5 認(rèn)證服務(wù)器與用戶相互認(rèn)證結(jié)果Fig.5 Mutual authentication results between authentication server and user

5 結(jié)論

隨著大數(shù)據(jù)挖掘和分析技術(shù)的發(fā)展，大數(shù)據(jù)安全和隱私受到了人們的重點關(guān)注，特別是保留用戶隱私的身份認(rèn)證協(xié)議已經(jīng)成為一個非?；钴S的研究領(lǐng)域.利用大數(shù)據(jù)特征，認(rèn)證協(xié)議PPMUAS聲稱實現(xiàn)了移動用戶的隱私保護和身份認(rèn)證.但是本文通過對其使用基于符號模型的ProVerif進行形式化建模分析后發(fā)現(xiàn)，認(rèn)證服務(wù)器對數(shù)據(jù)庫具有認(rèn)證性，而數(shù)據(jù)庫對認(rèn)證服務(wù)器無認(rèn)證性，用戶和認(rèn)證服務(wù)器間均無認(rèn)證，對于用戶口令Pwi有秘密性.

關(guān)于認(rèn)證服務(wù)器與用戶的相互認(rèn)證性和認(rèn)證服務(wù)器對數(shù)據(jù)庫的認(rèn)證性，可以在不引入新的秘鑰系統(tǒng)[16,17]下，分別對消息3 Login request，6 Login response和5 Database response中的參數(shù)進行數(shù)字簽名[18,19]，從而實現(xiàn)認(rèn)證性.

將來對PPMUAS協(xié)議進行改進，在完善認(rèn)證性的基礎(chǔ)上，通過隱私度量[20,21]對其隱私性進行量化分析.同時，通過引入差分隱私[22,23]改善其隱私性.