孟博，唐獲野，陳雙

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

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

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

1 PPMUAS認證協(xié)議的消息結構

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

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

1.1 用戶注冊請求

用戶User注冊時向認證服務器發(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ā)送給認證服務器.

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

1.2 認證服務器注冊請求

認證服務器接收到消息1 Registration request后，通過哈希函數(shù)Hash對Idi，Rpwi和i進行散列得到Vi并存儲到認證服務器中；同時產(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 認證服務器登錄請求

1.5 數(shù)據(jù)庫響應

1.6 登錄響應

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

2 應用Applied PI演算對PPMUAS認證協(xié)議形式化建模

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

函數(shù)和等式理論主要包含：公鑰算法包含加密算法aenc(x,Pu)和解密算法adec(y，Pu).aenc(x,Pu)對應用公鑰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、認證服務器進程processAs和數(shù)據(jù)庫進程processDB.它們共同構成了主進程，具體表述如下：

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

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

登錄階段，用戶再次執(zhí)行與注冊階段相同的工作，將登錄消息e′發(fā)送給認證服務器進程.若登錄成功則會通過信道c接受到認證服務器返回的登錄響應.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演算對認證服務器進程建模為processAs.

注冊階段，通過公開信道c收到消息m1，通過對Rpwi、用戶Idi和用戶代號i進行哈希運算得到散列值Vi并存儲在認證服務器本地，同時用戶個人隱私文件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ù)庫服務器進程建模為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認證協(xié)

議的秘密性和認證性

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

表1 認證模型Tab.1 Authentication model

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

4 分析結果

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

圖3 Pwi秘密性Fig.3 Pwi secrecy

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

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

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

圖5 認證服務器與用戶相互認證結果Fig.5 Mutual authentication results between authentication server and user

5 結論

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

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

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