適用于無線體域網(wǎng)的動態(tài)口令認證協(xié)議

杜夢瑤，王 崢，李 娜，強 彥

1.太原理工大學 信息與計算機學院，山西 晉中 030600

2.國網(wǎng)山西省電力公司，太原 030024

1 引言

無線體域網(wǎng)（Wireless Body Area Network，WBAN）是指以人體為核心，由一系列嵌入式或者可穿戴傳感器節(jié)點和個人智能設(shè)備（如智能手機、PDA等）組成的無線通信網(wǎng)絡(luò)。個人服務器收集傳感器獲取的生理信息后，通過無線局域網(wǎng)傳遞至醫(yī)療服務端，由醫(yī)療服務端對患者的病情進行診治[1]。由于無線網(wǎng)絡(luò)的開放性，無線體域網(wǎng)在給人類帶來醫(yī)療幫助的同時，存在的安全問題也日益突出。身份認證一方面可以防止非法用戶登錄服務端享受資源和服務，同時另一方面也可以防止攻擊者假冒合法醫(yī)療服務端獲取病人的敏感數(shù)據(jù)[2-3]。因此，無線體域網(wǎng)認證協(xié)議的安全性問題成為近幾年來無線體域網(wǎng)領(lǐng)域研究的熱點[4]。

現(xiàn)有的WBAN身份認證方案主要分為兩類，基于人體生物信息的認證方案和基于傳統(tǒng)密碼學的認證方案[5]。朱淑文等人于2018年設(shè)計了用心電特征作為認證私鑰的雙向認證協(xié)議，實現(xiàn)了用戶與醫(yī)療服務端的相互認證[6]，但心電特征較難進行提取。Dodangeh P等人于2018年設(shè)計了整個無線體域網(wǎng)網(wǎng)絡(luò)架構(gòu)的安全方案，使用生物識別技術(shù)作為認證和密鑰交換的一部分，通過BAN邏輯驗證方案能夠抵御各種攻擊[7]，但生物識別技術(shù)存在偶然性大、誤差性大的問題。因此，總體來說，基于人體生物特征信息的身份認證方案存在生物信息難提取、較大偶然性和較大誤差性的缺陷，所以這種身份認證方法有待進一步商榷[8]。陳少輝于2015年在無證書公鑰密碼體制的基礎(chǔ)上提出一種新的基于無對的無證書簽名認證協(xié)議，但該方案存在用戶與服務器認證復雜、速度慢的缺陷[9]。Yeh H L等人于2011年在分析Das等人提出的無線體域網(wǎng)認證方案存在內(nèi)部攻擊和偽造攻擊的基礎(chǔ)上，提出一種基于ECC機制的認證協(xié)議[10]，但后被指出該協(xié)議不能有效完成雙向認證[11]。文獻[8]中，彭彥彬等人基于挑戰(zhàn)應答S/Key，SAS和SAS-2認證協(xié)議低成本的優(yōu)點，通過引入設(shè)備標志、減少哈希運算與消息傳輸次數(shù)等方法，提出一種端到端的醫(yī)療無線體域網(wǎng)認證方案，該方案經(jīng)測試各項資源占用和能耗指標總體上小于挑戰(zhàn)應答協(xié)議，但該協(xié)議不能抵御拒絕服務器攻擊。

本文對前人提出的無線體域網(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模型檢測實驗方法進行形式化驗證分析。

2 WBAN_DPAP認證協(xié)議

本文提出的無線體域網(wǎng)的動態(tài)口令認證協(xié)議WBAN_DPAP（Wireless Body Area Network_Dynamic Password Authentication Protocol）分為兩個階段：協(xié)議注冊階段和協(xié)議認證階段。注冊階段只在客戶第一次登錄醫(yī)療服務端時執(zhí)行，認證階段在每次登錄醫(yī)療服務端時執(zhí)行。協(xié)議由兩個實體組成：個人服務器實體和醫(yī)療服務端實體。為了方便協(xié)議描述及形式化分析，表1給出協(xié)議過程中使用的具體符號定義。

表1 WBAN_DPAP協(xié)議符號定義表

2.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é)議注冊過程

2.2 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ī)療服務端是否保存PID所對應的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é)議認證過程

3 WBAN_DPAP協(xié)議安全性分析

3.1 基于SVO邏輯的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）得到。

3.2 WBAN_DPAP協(xié)議其他安全性

本協(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ī)療服務端獲取服務，則必須計算對應的A=H(MR//PW)。由于攻擊者未在服務器端注冊，無法獲得第一次認證所需的MR，因此不能偽裝成PS實體。若攻擊者嘗試偽裝MS實體獲取用戶敏感資源或數(shù)據(jù)，必須計算對應的C=H(PW//PR)，由于攻擊者不可能得到MS的私鑰，無法解密PS實體發(fā)送的消息也就無法獲得隨機數(shù)PR，故無法偽裝為MS實體。因此協(xié)議能夠有效阻止偽裝攻擊。

（4）阻止拒絕服務器攻擊。假設(shè)協(xié)議過程中沒有加入時間戳，PS實體和MS實體收到消息未加判斷即進行私鑰解密操作，容易導致耗盡資源而拒絕服務。WBAN_DPAP協(xié)議中加入時間戳，實體收到消息后首先進行判斷，若時延超過ΔT，則拒絕認證，因此協(xié)議能有效抵御拒絕服務器攻擊。

（5）阻止口令離線攻擊。在整個協(xié)議交互過程中，PS和MS實體之間的認證消息是由隨機數(shù)、時間戳等因子經(jīng)過復雜的數(shù)學運算和加密運算得到的，消息間不存在運算關(guān)系，且消息中運用的散列函數(shù)是單向的安全散列函數(shù)。若試圖使用窮舉法，巨大的計算量將會使攻擊者束手無策。

4 基于SPIN的WBAN_DPAP協(xié)議分析

4.1 SPIN模型檢測工具

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)應滿足的屬性，提供了一套驗證系統(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è)計擁有預期的行為。如果SPIN在驗證過程中發(fā)現(xiàn)模型不滿足LTL公式描述的目標屬性，則表明所驗證的協(xié)議存在缺陷或攻擊，這時跟蹤trail文件可以得出反例，可由人工進行診斷，返回設(shè)計階段找出錯誤原因[16]。

4.2 WBAN_DPAP協(xié)議的SPIN檢測分析

本次協(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后回應消息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兩個進程，分別表示個人服務器和醫(yī)療服務端進程。系統(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)空間搜索。“State-vector 64 byte，depth reached 26”表示完全描述一個全局系統(tǒng)的狀態(tài)需要64 Byte的內(nèi)存，最長深度優(yōu)先搜索路徑包含26個從樹根開始的轉(zhuǎn)移。“errors：0”表示在這次搜索過程中沒有發(fā)生錯誤，即協(xié)議滿足LTL公式描述的屬性。“128.730 total actual memory usage”表示該協(xié)議進行檢測時數(shù)據(jù)使用的內(nèi)存空間總字符為128.73 MB[18]。

圖7 協(xié)議驗證結(jié)果圖

5 結(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é)議的資源占用率和能耗，在保證安全的前提下，進一步減少其資源消耗。