杜夢瑤,王 崢,李 娜,強 彥
1.太原理工大學 信息與計算機學院,山西 晉中 030600
2.國網(wǎng)山西省電力公司,太原 030024
無線體域網(wǎng)(Wireless Body Area Network,WBAN)是指以人體為核心,由一系列嵌入式或者可穿戴傳感器節(jié)點和個人智能設(shè)備(如智能手機、PDA等)組成的無線通信網(wǎng)絡(luò)。個人服務(wù)器收集傳感器獲取的生理信息后,通過無線局域網(wǎng)傳遞至醫(yī)療服務(wù)端,由醫(yī)療服務(wù)端對患者的病情進行診治[1]。由于無線網(wǎng)絡(luò)的開放性,無線體域網(wǎng)在給人類帶來醫(yī)療幫助的同時,存在的安全問題也日益突出。身份認證一方面可以防止非法用戶登錄服務(wù)端享受資源和服務(wù),同時另一方面也可以防止攻擊者假冒合法醫(yī)療服務(wù)端獲取病人的敏感數(shù)據(jù)[2-3]。因此,無線體域網(wǎng)認證協(xié)議的安全性問題成為近幾年來無線體域網(wǎng)領(lǐng)域研究的熱點[4]。
現(xiàn)有的WBAN身份認證方案主要分為兩類,基于人體生物信息的認證方案和基于傳統(tǒng)密碼學的認證方案[5]。朱淑文等人于2018年設(shè)計了用心電特征作為認證私鑰的雙向認證協(xié)議,實現(xiàn)了用戶與醫(yī)療服務(wù)端的相互認證[6],但心電特征較難進行提取。Dodangeh P等人于2018年設(shè)計了整個無線體域網(wǎng)網(wǎng)絡(luò)架構(gòu)的安全方案,使用生物識別技術(shù)作為認證和密鑰交換的一部分,通過BAN邏輯驗證方案能夠抵御各種攻擊[7],但生物識別技術(shù)存在偶然性大、誤差性大的問題。因此,總體來說,基于人體生物特征信息的身份認證方案存在生物信息難提取、較大偶然性和較大誤差性的缺陷,所以這種身份認證方法有待進一步商榷[8]。陳少輝于2015年在無證書公鑰密碼體制的基礎(chǔ)上提出一種新的基于無對的無證書簽名認證協(xié)議,但該方案存在用戶與服務(wù)器認證復(fù)雜、速度慢的缺陷[9]。Yeh H L等人于2011年在分析Das等人提出的無線體域網(wǎng)認證方案存在內(nèi)部攻擊和偽造攻擊的基礎(chǔ)上,提出一種基于ECC機制的認證協(xié)議[10],但后被指出該協(xié)議不能有效完成雙向認證[11]。文獻[8]中,彭彥彬等人基于挑戰(zhàn)應(yīng)答S/Key,SAS和SAS-2認證協(xié)議低成本的優(yōu)點,通過引入設(shè)備標志、減少哈希運算與消息傳輸次數(shù)等方法,提出一種端到端的醫(yī)療無線體域網(wǎng)認證方案,該方案經(jīng)測試各項資源占用和能耗指標總體上小于挑戰(zhàn)應(yīng)答協(xié)議,但該協(xié)議不能抵御拒絕服務(wù)器攻擊。
本文對前人提出的無線體域網(wǎng)認證協(xié)議的優(yōu)缺點進行總結(jié)分析,針對人體生物信息的認證方法和傳統(tǒng)密碼學的認證方法不能滿足無線體域網(wǎng)環(huán)境的問題,基于動態(tài)口令(又稱一次性口令,Dynamic Password,DP)的輕量、隨機性、動態(tài)性和一次性[12]及非對稱加密算法的高安全性,提出一種適用于無線體域網(wǎng)的動態(tài)口令雙向認證協(xié)議,并對協(xié)議采用SVO邏輯推理方法[13]和SPIN模型檢測實驗方法進行形式化驗證分析。
本文提出的無線體域網(wǎng)的動態(tài)口令認證協(xié)議WBAN_DPAP(Wireless Body Area Network_Dynamic Password Authentication Protocol)分為兩個階段:協(xié)議注冊階段和協(xié)議認證階段。注冊階段只在客戶第一次登錄醫(yī)療服務(wù)端時執(zhí)行,認證階段在每次登錄醫(yī)療服務(wù)端時執(zhí)行。協(xié)議由兩個實體組成:個人服務(wù)器實體和醫(yī)療服務(wù)端實體。為了方便協(xié)議描述及形式化分析,表1給出協(xié)議過程中使用的具體符號定義。
表1 WBAN_DPAP協(xié)議符號定義表
WBAN_DPAP協(xié)議注冊過程的步驟如下:
(1)PS實體向MS實體發(fā)送注冊請求消息,執(zhí)行msg1。
msg1:PS(注冊請求)→MS
(2)MS實體收到消息后,執(zhí)行msg2。
msg2:MS(KMR)→PS
(3)PS實體收到消息后保存KMR,并計算EKMR(PID//KPR//PW),執(zhí)行msg3。
msg3:PS(EKMR(PID//KPR//PW))→MS
(4)MS實體收到消息,用其私鑰進行解密得到PID、KPR、PW并保存,同時產(chǎn)生隨機數(shù)MR并保存為MR′。計算EKPR(MID//MR),執(zhí)行msg4。
msg4:MS(EKPR(MID//MR))→PS
(5)PS實體對msg4進行解密并保存MID、MR。
WBAN_DPAP認證協(xié)議的注冊過程如圖1所示。
圖1 WBAN_DPAP協(xié)議注冊過程
WBAN_DPAP協(xié)議認證過程的步驟如下:
(1)PS實體輸入PID、PW,提取當前時間戳T1,產(chǎn)生隨機數(shù)PR并保存為PR′。計算(EKMR(PID//H(MR//PW)//PR//T1)//T1),執(zhí)行Msg1。
Msg1:PS(EKMR(PID//H(MR//PW)//
(2)MS實體在T?1時刻收到消息。若T?1-T1≤ΔT,則接收認證請求,否則拒接登錄認證。
(3)MS計算 DKMS(EKMR(PID//H(MR//PW)//PR//T1)),得到 PID、A=H(MR//PW)、PR、T1,首先檢查解密得到的時間戳與未加密時間戳是否一致,若不一致,則認為認證失敗。其次檢查醫(yī)療服務(wù)端是否保存PID所對應(yīng)的PW,若不存在,則認證失敗,否則計算B=H(MR′//PW)。最后進行驗證,若A=B,則PS為合法實體,若不相等,MS拒接其認證請求,認證結(jié)束。
(4)若PS為合法實體,MS提取當前時間戳T2,產(chǎn)生隨機數(shù)MR并保存為MR′以供PS下次驗證,計算 EKPR(MID//H(PW//PR)//MR//T2)//T2,執(zhí)行Msg2。
Msg2:MS(EKPR(MID//H(PW//PR)//
(5)PS實體在T?2時刻收到消息。若T?2-T2≤ΔT,則接收認證請求,否則拒絕登錄認證。
(6)PS計算 DKPS(EKPR(MID//H(PW//PR)//MR//T2)),得到 MID、C=H(PW//PR)、MR、T2,首先檢查解密得到的時間戳與未加密時間戳是否一致,若不一致,則認證失敗。其次計算D=H(PW//PR′),最后進行驗證,若C=D,則MS為合法實體,否則認證結(jié)束。
WLAN_DPAP認證協(xié)議的認證過程如圖2所示。
圖2 WBAN_DPAP協(xié)議認證過程
1994年,Syverson P和van Oorschot P C提出SVO邏輯,其標志著BAN及BAN類邏輯的成熟[14]。SVO邏輯可以有效地發(fā)現(xiàn)協(xié)議設(shè)計中的漏洞和安全漏洞,并在認證協(xié)議的形式化分析中發(fā)揮重要作用。
SVO邏輯包含2個初始規(guī)則和20條公理,本文協(xié)議認證過程使用的包括必要性規(guī)則Nec、源關(guān)聯(lián)公理Ax4、接受公理Ax7、Ax8、看見公理Ax10、說過公理Ax14、新鮮性公理Ax17、Nonce驗證公理Ax19,具體如下:
必要性規(guī)則Nec:|-φ?|-P believes φ
Nec規(guī)則表明,如果φ是一個定理,則P believes φ也是一個定理。
源關(guān)聯(lián)公理Ax4:
PKσ(Q,K)∧R received X∧SV(X,K,Y)?Q said Y
Ax4表明,如果R收到X,且簽名驗證通過,則可推理出Q說過Y。
接收公理Ax7:
P received(X1,X2,…,Xn)? P received Xi
Ax7表明,主體接收到一個消息,也同時接收了該消息的連接項。
接收公理Ax8:
Ax8表明,如果主體擁有解密密鑰,可以獲得被加密前的消息。
看見公理Ax10:P received X?P sees X
Ax10表明,一個主體能看見所有它接收到的。
說過公理Ax14:
Ax14表明,一個主體只能說他所擁有的。
新鮮性公理Ax17:fresh(Xi)?fresh(X1,X2,…,Xn)Ax17表明,若 Xi是新鮮的,則其級聯(lián)(X1,X2,…,Xn)是新鮮的。
Nonce驗證公理Ax19:
Ax19表明,如果X是新鮮的,且主體說過X,就意味著主體最近說過,也即在當前時期內(nèi)說過。
使用SVO邏輯對協(xié)議的形式化分析分為三個步驟,即給出協(xié)議初始化假設(shè)、列出協(xié)議目標和進行推理證明[15]。
(1)協(xié)議初始化假設(shè)
P1:PS believes fresh(PR)
P2:MS believes fresh(MR)
P3:PS believes PKσ(PS,KPS)
P4:MS believes PKσ(MS,KMS)
P5:PS believes PKψ(MS,KMR)
P6:MS believes PKψ(PS,KPR)
P7:PS received{MID,H(PW,PR),MR,T2}KPR,T2
P8:MS received{PID,H(MR,PW),PR,T1}KMR,T1
P9:PS believes SV({MID,H(PW,PR),MR,T2}KPR,KPS,{MID,H(PW,PR),MR,T2})
P10:MS believes SV({PID,H(MR,PW),PR,T1}KMR,KMS,{PID,H(MR,PW),PR,T1})
給出主體對接收到的消息的理解
P11:PS believes PS received{MID,H(PW,PR),MR,T2}KPR,T2
P12:MS believes MS received{PID,H(MR,PW),PR,T1}KMR,T1
(2)協(xié)議目標
T1:PS believes MS says H(PW,PR)
PS believes PS sees H(PW,PR)
T2:MS believes PS says H(MR,PW)
MS believes MS sees H(MR,PW)
(3)推理證明
根據(jù)P11,Ax7可得:
PS believes PS received{MID,H(PW,PR),
根據(jù)P12,Ax7可得:
MS believes MS received{PID,H(MR,PW),
根據(jù)式(1),P3,Ax8,Nec可得:
PS believes PS received{MID,H(PW,PR),MR,T2}(3)
根據(jù)式(2),P4,Ax8,Nec可得:
MS believes MS received{PID,H(MR,PW),PR,T1} (4)
根據(jù)式(3),Ax7可得:
PS received PS received H(PW,PR) (5)
根據(jù)式(4),Ax7可得:
MS believes MS received H(MR,PW) (6)
根據(jù)式(5),Ax10,Nec可得:
PS believes PS sees H(PW,PR) (7)
根據(jù)式(6),Ax10,Nec可得:
MS believes MS sees H(MR,PW) (8)
根據(jù)P1,Ax17可得:
PS believes fresh H(PW,PR) (9)
根據(jù)P2,Ax17可得:
MS believes fresh H(MR,PW) (10)
根據(jù)式(5),P3,P6,P9,Ax4,Ax14,Nec可得:
PS believes MS said H(PW,PR) (11)
根據(jù)式(6),P4,P5,P10,Ax4,Ax14,Nec可得:
MS believes PS said H(MR,PW) (12)
根據(jù)式(9),(11),Ax19可得:
PS believes MS says H(PW,PR) (13)
根據(jù)式(10),(12),Ax19可得:
MS believes PS says H(MR,PW) (14)
綜上所述,目標T1可由式(7)、(13)得到;目標T2可由式(8)、(14)得到。
本協(xié)議是基于動態(tài)口令和非對稱密碼學的無線體域網(wǎng)認證協(xié)議。不斷變化的因素將作為動態(tài)因子加入到認證過程中形成動態(tài)口令,計算量小,與靜態(tài)口令相比具有隨機性、動態(tài)性、一次性。非對稱加密不需要在通信前同步密鑰,與對稱加密相比安全性更好。因此,WBAN_DPAP協(xié)議是輕量的并且具有高安全性。具體分析如下:
(1)實現(xiàn)雙向認證。在協(xié)議認證過程中,當MS計算 B=H(MR′//PW)與 PS發(fā)送的 A=H(MR//PW)相等時,PS是合法的;當PS計算D=H(PW//PR′)與MS發(fā)送的C=H(PW//PR)相等時,MS是合法的。若有其中一方結(jié)果不相等,則實體為非法用戶,由此可實現(xiàn)協(xié)議實體的雙向認證。
(2)阻止重放攻擊。協(xié)議認證過程包含的隨機數(shù)PR、MR,時間戳T1、T2均為一次有效的動態(tài)因子,保證了消息的不可重用。即使被攔截,攻擊者獲取消息并進行重放也將花費一定時間,時延超過ΔT,實體拒絕接受認證請求。因此可以抵抗重放攻擊。
(3)阻止偽裝攻擊。攻擊者偽裝合法實體進行攻擊,包括偽裝PS實體和偽裝MS實體兩種情況。如果攻擊者試圖偽裝PS實體登錄醫(yī)療服務(wù)端獲取服務(wù),則必須計算對應(yīng)的A=H(MR//PW)。由于攻擊者未在服務(wù)器端注冊,無法獲得第一次認證所需的MR,因此不能偽裝成PS實體。若攻擊者嘗試偽裝MS實體獲取用戶敏感資源或數(shù)據(jù),必須計算對應(yīng)的C=H(PW//PR),由于攻擊者不可能得到MS的私鑰,無法解密PS實體發(fā)送的消息也就無法獲得隨機數(shù)PR,故無法偽裝為MS實體。因此協(xié)議能夠有效阻止偽裝攻擊。
(4)阻止拒絕服務(wù)器攻擊。假設(shè)協(xié)議過程中沒有加入時間戳,PS實體和MS實體收到消息未加判斷即進行私鑰解密操作,容易導致耗盡資源而拒絕服務(wù)。WBAN_DPAP協(xié)議中加入時間戳,實體收到消息后首先進行判斷,若時延超過ΔT,則拒絕認證,因此協(xié)議能有效抵御拒絕服務(wù)器攻擊。
(5)阻止口令離線攻擊。在整個協(xié)議交互過程中,PS和MS實體之間的認證消息是由隨機數(shù)、時間戳等因子經(jīng)過復(fù)雜的數(shù)學運算和加密運算得到的,消息間不存在運算關(guān)系,且消息中運用的散列函數(shù)是單向的安全散列函數(shù)。若試圖使用窮舉法,巨大的計算量將會使攻擊者束手無策。
Promela語言解析器SPIN(Simple Promela Interpreter)是由美國貝爾實驗室Gerard J.Holzmann開發(fā)的用于驗證通信協(xié)議的模型檢測工具。工具采用深度優(yōu)先搜索遍歷狀態(tài)空間,以Promela作為建模語言,使用線性時態(tài)邏輯(Linear Temporal Logic,LTL)公式描述系統(tǒng)需求。SPIN模型檢測工具可以提供系統(tǒng)語言用于直觀準確地描述系統(tǒng)模型而不考慮具體實現(xiàn)細節(jié),功能強大而簡明地描述系統(tǒng)應(yīng)滿足的屬性,提供了一套驗證系統(tǒng)建模邏輯一致性及系統(tǒng)是否滿足所要驗證性質(zhì)的方法。SPIN的協(xié)議驗證模型如圖3所示。
圖3 SPIN協(xié)議驗證模型
如圖3所示,SPIN的協(xié)議驗證模型包括三個階段:設(shè)計階段、建模階段以及驗證階段。在協(xié)議設(shè)計階段,根據(jù)無線體域網(wǎng)環(huán)境的特點設(shè)計一種適用于無線體域網(wǎng)的認證協(xié)議;協(xié)議建模階段包括兩方面,一方面使用Promela語言編寫描述系統(tǒng)行為的模型,另一方面采用LTL公式表達系統(tǒng)要求的安全性屬性;在協(xié)議驗證階段,使用SPIN對協(xié)議進行分析,經(jīng)語法分析沒有錯誤后對系統(tǒng)交互進行模擬,直到確認協(xié)議設(shè)計擁有預(yù)期的行為。如果SPIN在驗證過程中發(fā)現(xiàn)模型不滿足LTL公式描述的目標屬性,則表明所驗證的協(xié)議存在缺陷或攻擊,這時跟蹤trail文件可以得出反例,可由人工進行診斷,返回設(shè)計階段找出錯誤原因[16]。
本次協(xié)議的SPIN檢測分析實驗環(huán)境為:Windows10操作系統(tǒng)、SPIN版本為6.4.9、iSpin版本為1.1.4,TclTk版本為8.5。
用Promela對WBAN_DPAP協(xié)議的實體進行建模以模擬協(xié)議運行過程。PS、MS和入侵者Intruder三者身份分別用AgentP、AgentM、AgentI表示;通信對象partner包括 PS、MS 和Intruder;Msg1和Msg2為協(xié)議認證過程中兩個不同的消息,分別表示W(wǎng)BAN_DPAP協(xié)議中實體PS和MS發(fā)送的消息;statusP、statusM表示協(xié)議認證執(zhí)行結(jié)束后MS和PS的狀態(tài),為布爾類型值。MS、PS的建模如圖4所示[17]。
圖4 PS與MS的通信建模示意圖
如圖4所示,主體PS選擇通信對象partner并向通道中發(fā)送消息Msg1,該消息由主體MS接收并選擇通信對象partner后回應(yīng)消息Msg2。雙方在協(xié)議順利完成,即沒有攻擊者參與的情況下將各自狀態(tài)statusP、statusM設(shè)置為OK。
對WBAN_DPAP協(xié)議進行Promela描述后,為了驗證建模的正確性及協(xié)議運行的過程,使用SPIN模型檢測工具模擬協(xié)議各主體的通信行為,如圖5協(xié)議行為模擬圖所示,在沒有入侵者存在的情況下,可以成功地模擬協(xié)議執(zhí)行順序,達到協(xié)議所期望的目的。
圖5 無入侵者時議通信行為模擬圖
從圖5中可以看出,該協(xié)議共創(chuàng)建兩個進程,從左至右分別為PS、MS兩個進程,分別表示個人服務(wù)器和醫(yī)療服務(wù)端進程。系統(tǒng)為每個進程賦予一個唯一的進程號Pid,PS實體進程號為0,MS實體進程號為1。PS首先向MS發(fā)送消息Msg1,MS收到消息后返回消息Msg2,由此可知協(xié)議執(zhí)行順序與協(xié)議設(shè)計一致。
在WBAN_DPAP協(xié)議中,PS與MS實體間完成相互認證,需要滿足協(xié)議安全性的LTL公式表示如下:
其中,&&表示與運算,[]P表示P在所有狀態(tài)點都成立,<>P表示P最終會在某些狀態(tài)點成立。
采用Dolev-Yao模型對非法攻擊者Intruder進行建模。攻擊者在協(xié)議通信過程中竊取消息并進行存儲,然后選擇一個消息接收者進行消息的重放。攻擊者的Promela建模示意圖如圖6所示。
圖6 Intruder的通信建模示意圖
從圖中可以看出,攻擊者通過截獲PS與MS之間通信的消息達到攻擊目的。加入攻擊者模型后,對協(xié)議需滿足的LTL屬性進行驗證,驗證結(jié)果如圖7所示。圖中“Full statespace search for”表示默認為完全的狀態(tài)空間搜索?!癝tate-vector 64 byte,depth reached 26”表示完全描述一個全局系統(tǒng)的狀態(tài)需要64 Byte的內(nèi)存,最長深度優(yōu)先搜索路徑包含26個從樹根開始的轉(zhuǎn)移?!癳rrors:0”表示在這次搜索過程中沒有發(fā)生錯誤,即協(xié)議滿足LTL公式描述的屬性?!?28.730 total actual memory usage”表示該協(xié)議進行檢測時數(shù)據(jù)使用的內(nèi)存空間總字符為128.73 MB[18]。
圖7 協(xié)議驗證結(jié)果圖
本文在前人基于生物信息和傳統(tǒng)密碼學的研究基礎(chǔ)上,提出一種適用于無線體域網(wǎng)的動態(tài)口令雙向認證輕量級協(xié)議。通過理論證明和SVO邏輯推理方法驗證了WBAN_DPAP認證協(xié)議的安全屬性。使用SPIN模型檢測工具對協(xié)議進行建模實驗,實驗結(jié)果表明,WBAN_DPAP認證協(xié)議滿足安全性目標。
該協(xié)議將時間同步認證機制與一次性密碼相結(jié)合,使用時間戳和隨機數(shù)作為雙重身份驗證因素,采用非對稱加密算法對通信消息進行加密,整個方案安全性更高且輕量。下一步工作,繼續(xù)研究本文提出的無線體域網(wǎng)認證協(xié)議的資源占用率和能耗,在保證安全的前提下,進一步減少其資源消耗。