杜夢(mèng)瑤，王 崢，李 娜，強(qiáng) 彥

1.太原理工大學(xué) 信息與計(jì)算機(jī)學(xué)院，山西 晉中 030600

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

1 引言

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

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

本文對(duì)前人提出的無(wú)線(xiàn)體域網(wǎng)認(rèn)證協(xié)議的優(yōu)缺點(diǎn)進(jìn)行總結(jié)分析，針對(duì)人體生物信息的認(rèn)證方法和傳統(tǒng)密碼學(xué)的認(rèn)證方法不能滿(mǎn)足無(wú)線(xiàn)體域網(wǎng)環(huán)境的問(wèn)題，基于動(dòng)態(tài)口令（又稱(chēng)一次性口令，Dynamic Password，DP）的輕量、隨機(jī)性、動(dòng)態(tài)性和一次性[12]及非對(duì)稱(chēng)加密算法的高安全性，提出一種適用于無(wú)線(xiàn)體域網(wǎng)的動(dòng)態(tài)口令雙向認(rèn)證協(xié)議，并對(duì)協(xié)議采用SVO邏輯推理方法[13]和SPIN模型檢測(cè)實(shí)驗(yàn)方法進(jìn)行形式化驗(yàn)證分析。

2 WBAN_DPAP認(rèn)證協(xié)議

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

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

2.1 WBAN_DPAP協(xié)議注冊(cè)過(guò)程

WBAN_DPAP協(xié)議注冊(cè)過(guò)程的步驟如下：

（1）PS實(shí)體向MS實(shí)體發(fā)送注冊(cè)請(qǐng)求消息，執(zhí)行msg1。

msg1：PS(注冊(cè)請(qǐng)求)→MS

（2）MS實(shí)體收到消息后，執(zhí)行msg2。

msg2：MS(KMR)→PS

（3）PS實(shí)體收到消息后保存KMR，并計(jì)算EKMR(PID//KPR//PW)，執(zhí)行msg3。

msg3：PS(EKMR(PID//KPR//PW))→MS

（4）MS實(shí)體收到消息，用其私鑰進(jìn)行解密得到PID、KPR、PW并保存，同時(shí)產(chǎn)生隨機(jī)數(shù)MR并保存為MR′。計(jì)算EKPR(MID//MR)，執(zhí)行msg4。

msg4：MS(EKPR(MID//MR))→PS

（5）PS實(shí)體對(duì)msg4進(jìn)行解密并保存MID、MR。

WBAN_DPAP認(rèn)證協(xié)議的注冊(cè)過(guò)程如圖1所示。

圖1 WBAN_DPAP協(xié)議注冊(cè)過(guò)程

2.2 WBAN_DPAP協(xié)議認(rèn)證過(guò)程

WBAN_DPAP協(xié)議認(rèn)證過(guò)程的步驟如下：

（1）PS實(shí)體輸入PID、PW，提取當(dāng)前時(shí)間戳T1，產(chǎn)生隨機(jī)數(shù)PR并保存為PR′。計(jì)算(EKMR(PID//H(MR//PW)//PR//T1)//T1)，執(zhí)行Msg1。

Msg1：PS(EKMR(PID//H(MR//PW)//

（2）MS實(shí)體在T?1時(shí)刻收到消息。若T?1-T1≤ΔT，則接收認(rèn)證請(qǐng)求，否則拒接登錄認(rèn)證。

（3）MS計(jì)算 DKMS(EKMR(PID//H(MR//PW)//PR//T1))，得到 PID、A=H(MR//PW)、PR、T1，首先檢查解密得到的時(shí)間戳與未加密時(shí)間戳是否一致，若不一致，則認(rèn)為認(rèn)證失敗。其次檢查醫(yī)療服務(wù)端是否保存PID所對(duì)應(yīng)的PW，若不存在，則認(rèn)證失敗，否則計(jì)算B=H(MR′//PW)。最后進(jìn)行驗(yàn)證，若A=B，則PS為合法實(shí)體，若不相等，MS拒接其認(rèn)證請(qǐng)求，認(rèn)證結(jié)束。

（4）若PS為合法實(shí)體，MS提取當(dāng)前時(shí)間戳T2，產(chǎn)生隨機(jī)數(shù)MR并保存為MR′以供PS下次驗(yàn)證，計(jì)算 EKPR(MID//H(PW//PR)//MR//T2)//T2，執(zhí)行Msg2。

Msg2：MS(EKPR(MID//H(PW//PR)//

（5）PS實(shí)體在T?2時(shí)刻收到消息。若T?2-T2≤ΔT，則接收認(rèn)證請(qǐng)求，否則拒絕登錄認(rèn)證。

（6）PS計(jì)算 DKPS(EKPR(MID//H(PW//PR)//MR//T2))，得到 MID、C=H(PW//PR)、MR、T2，首先檢查解密得到的時(shí)間戳與未加密時(shí)間戳是否一致，若不一致，則認(rèn)證失敗。其次計(jì)算D=H(PW//PR′)，最后進(jìn)行驗(yàn)證，若C=D，則MS為合法實(shí)體，否則認(rèn)證結(jié)束。

WLAN_DPAP認(rèn)證協(xié)議的認(rèn)證過(guò)程如圖2所示。

圖2 WBAN_DPAP協(xié)議認(rèn)證過(guò)程

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

3.1 基于SVO邏輯的WBAN_DPAP協(xié)議分析

1994年，Syverson P和van Oorschot P C提出SVO邏輯，其標(biāo)志著B(niǎo)AN及BAN類(lèi)邏輯的成熟[14]。SVO邏輯可以有效地發(fā)現(xiàn)協(xié)議設(shè)計(jì)中的漏洞和安全漏洞，并在認(rèn)證協(xié)議的形式化分析中發(fā)揮重要作用。

SVO邏輯包含2個(gè)初始規(guī)則和20條公理，本文協(xié)議認(rèn)證過(guò)程使用的包括必要性規(guī)則Nec、源關(guān)聯(lián)公理Ax4、接受公理Ax7、Ax8、看見(jiàn)公理Ax10、說(shuō)過(guò)公理Ax14、新鮮性公理Ax17、Nonce驗(yàn)證公理Ax19，具體如下：

必要性規(guī)則Nec：|-φ?|-P believes φ

Nec規(guī)則表明，如果φ是一個(gè)定理，則P believes φ也是一個(gè)定理。

源關(guān)聯(lián)公理Ax4：

PKσ(Q,K)∧R received X∧SV(X,K,Y)?Q said Y

Ax4表明，如果R收到X，且簽名驗(yàn)證通過(guò)，則可推理出Q說(shuō)過(guò)Y。

接收公理Ax7：

P received(X1,X2,…,Xn)? P received Xi

Ax7表明，主體接收到一個(gè)消息，也同時(shí)接收了該消息的連接項(xiàng)。

接收公理Ax8：

Ax8表明，如果主體擁有解密密鑰，可以獲得被加密前的消息。

看見(jiàn)公理Ax10：P received X?P sees X

Ax10表明，一個(gè)主體能看見(jiàn)所有它接收到的。

說(shuō)過(guò)公理Ax14：

Ax14表明，一個(gè)主體只能說(shuō)他所擁有的。

新鮮性公理Ax17：fresh(Xi)?fresh(X1,X2,…,Xn)Ax17表明，若 Xi是新鮮的，則其級(jí)聯(lián)(X1,X2,…,Xn)是新鮮的。

Nonce驗(yàn)證公理Ax19：

Ax19表明，如果X是新鮮的，且主體說(shuō)過(guò)X，就意味著主體最近說(shuō)過(guò)，也即在當(dāng)前時(shí)期內(nèi)說(shuō)過(guò)。

使用SVO邏輯對(duì)協(xié)議的形式化分析分為三個(gè)步驟，即給出協(xié)議初始化假設(shè)、列出協(xié)議目標(biāo)和進(jìn)行推理證明[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})

給出主體對(duì)接收到的消息的理解

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é)議目標(biāo)

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）

綜上所述，目標(biāo)T1可由式（7）、（13）得到；目標(biāo)T2可由式（8）、（14）得到。

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

本協(xié)議是基于動(dòng)態(tài)口令和非對(duì)稱(chēng)密碼學(xué)的無(wú)線(xiàn)體域網(wǎng)認(rèn)證協(xié)議。不斷變化的因素將作為動(dòng)態(tài)因子加入到認(rèn)證過(guò)程中形成動(dòng)態(tài)口令，計(jì)算量小，與靜態(tài)口令相比具有隨機(jī)性、動(dòng)態(tài)性、一次性。非對(duì)稱(chēng)加密不需要在通信前同步密鑰，與對(duì)稱(chēng)加密相比安全性更好。因此，WBAN_DPAP協(xié)議是輕量的并且具有高安全性。具體分析如下：

（1）實(shí)現(xiàn)雙向認(rèn)證。在協(xié)議認(rèn)證過(guò)程中，當(dāng)MS計(jì)算 B=H(MR′//PW)與 PS發(fā)送的 A=H(MR//PW)相等時(shí)，PS是合法的；當(dāng)PS計(jì)算D=H(PW//PR′)與MS發(fā)送的C=H(PW//PR)相等時(shí)，MS是合法的。若有其中一方結(jié)果不相等，則實(shí)體為非法用戶(hù)，由此可實(shí)現(xiàn)協(xié)議實(shí)體的雙向認(rèn)證。

（2）阻止重放攻擊。協(xié)議認(rèn)證過(guò)程包含的隨機(jī)數(shù)PR、MR，時(shí)間戳T1、T2均為一次有效的動(dòng)態(tài)因子，保證了消息的不可重用。即使被攔截，攻擊者獲取消息并進(jìn)行重放也將花費(fèi)一定時(shí)間，時(shí)延超過(guò)ΔT，實(shí)體拒絕接受認(rèn)證請(qǐng)求。因此可以抵抗重放攻擊。

（3）阻止偽裝攻擊。攻擊者偽裝合法實(shí)體進(jìn)行攻擊，包括偽裝PS實(shí)體和偽裝MS實(shí)體兩種情況。如果攻擊者試圖偽裝PS實(shí)體登錄醫(yī)療服務(wù)端獲取服務(wù)，則必須計(jì)算對(duì)應(yīng)的A=H(MR//PW)。由于攻擊者未在服務(wù)器端注冊(cè)，無(wú)法獲得第一次認(rèn)證所需的MR，因此不能偽裝成PS實(shí)體。若攻擊者嘗試偽裝MS實(shí)體獲取用戶(hù)敏感資源或數(shù)據(jù)，必須計(jì)算對(duì)應(yīng)的C=H(PW//PR)，由于攻擊者不可能得到MS的私鑰，無(wú)法解密PS實(shí)體發(fā)送的消息也就無(wú)法獲得隨機(jī)數(shù)PR，故無(wú)法偽裝為MS實(shí)體。因此協(xié)議能夠有效阻止偽裝攻擊。

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

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

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

4.1 SPIN模型檢測(cè)工具

Promela語(yǔ)言解析器SPIN（Simple Promela Interpreter）是由美國(guó)貝爾實(shí)驗(yàn)室Gerard J.Holzmann開(kāi)發(fā)的用于驗(yàn)證通信協(xié)議的模型檢測(cè)工具。工具采用深度優(yōu)先搜索遍歷狀態(tài)空間，以Promela作為建模語(yǔ)言，使用線(xiàn)性時(shí)態(tài)邏輯（Linear Temporal Logic，LTL）公式描述系統(tǒng)需求。SPIN模型檢測(cè)工具可以提供系統(tǒng)語(yǔ)言用于直觀(guān)準(zhǔn)確地描述系統(tǒng)模型而不考慮具體實(shí)現(xiàn)細(xì)節(jié)，功能強(qiáng)大而簡(jiǎn)明地描述系統(tǒng)應(yīng)滿(mǎn)足的屬性，提供了一套驗(yàn)證系統(tǒng)建模邏輯一致性及系統(tǒng)是否滿(mǎn)足所要驗(yàn)證性質(zhì)的方法。SPIN的協(xié)議驗(yàn)證模型如圖3所示。

圖3 SPIN協(xié)議驗(yàn)證模型

如圖3所示，SPIN的協(xié)議驗(yàn)證模型包括三個(gè)階段：設(shè)計(jì)階段、建模階段以及驗(yàn)證階段。在協(xié)議設(shè)計(jì)階段，根據(jù)無(wú)線(xiàn)體域網(wǎng)環(huán)境的特點(diǎn)設(shè)計(jì)一種適用于無(wú)線(xiàn)體域網(wǎng)的認(rèn)證協(xié)議；協(xié)議建模階段包括兩方面，一方面使用Promela語(yǔ)言編寫(xiě)描述系統(tǒng)行為的模型，另一方面采用LTL公式表達(dá)系統(tǒng)要求的安全性屬性；在協(xié)議驗(yàn)證階段，使用SPIN對(duì)協(xié)議進(jìn)行分析，經(jīng)語(yǔ)法分析沒(méi)有錯(cuò)誤后對(duì)系統(tǒng)交互進(jìn)行模擬，直到確認(rèn)協(xié)議設(shè)計(jì)擁有預(yù)期的行為。如果SPIN在驗(yàn)證過(guò)程中發(fā)現(xiàn)模型不滿(mǎn)足LTL公式描述的目標(biāo)屬性，則表明所驗(yàn)證的協(xié)議存在缺陷或攻擊，這時(shí)跟蹤trail文件可以得出反例，可由人工進(jìn)行診斷，返回設(shè)計(jì)階段找出錯(cuò)誤原因[16]。

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

本次協(xié)議的SPIN檢測(cè)分析實(shí)驗(yàn)環(huán)境為：Windows10操作系統(tǒng)、SPIN版本為6.4.9、iSpin版本為1.1.4，TclTk版本為8.5。

用Promela對(duì)WBAN_DPAP協(xié)議的實(shí)體進(jìn)行建模以模擬協(xié)議運(yùn)行過(guò)程。PS、MS和入侵者Intruder三者身份分別用AgentP、AgentM、AgentI表示；通信對(duì)象partner包括 PS、MS 和Intruder；Msg1和Msg2為協(xié)議認(rèn)證過(guò)程中兩個(gè)不同的消息，分別表示W(wǎng)BAN_DPAP協(xié)議中實(shí)體PS和MS發(fā)送的消息；statusP、statusM表示協(xié)議認(rèn)證執(zhí)行結(jié)束后MS和PS的狀態(tài)，為布爾類(lèi)型值。MS、PS的建模如圖4所示[17]。

圖4 PS與MS的通信建模示意圖

如圖4所示，主體PS選擇通信對(duì)象partner并向通道中發(fā)送消息Msg1，該消息由主體MS接收并選擇通信對(duì)象partner后回應(yīng)消息Msg2。雙方在協(xié)議順利完成，即沒(méi)有攻擊者參與的情況下將各自狀態(tài)statusP、statusM設(shè)置為OK。

對(duì)WBAN_DPAP協(xié)議進(jìn)行Promela描述后，為了驗(yàn)證建模的正確性及協(xié)議運(yùn)行的過(guò)程，使用SPIN模型檢測(cè)工具模擬協(xié)議各主體的通信行為，如圖5協(xié)議行為模擬圖所示，在沒(méi)有入侵者存在的情況下，可以成功地模擬協(xié)議執(zhí)行順序，達(dá)到協(xié)議所期望的目的。

圖5 無(wú)入侵者時(shí)議通信行為模擬圖

從圖5中可以看出，該協(xié)議共創(chuàng)建兩個(gè)進(jìn)程，從左至右分別為PS、MS兩個(gè)進(jìn)程，分別表示個(gè)人服務(wù)器和醫(yī)療服務(wù)端進(jìn)程。系統(tǒng)為每個(gè)進(jìn)程賦予一個(gè)唯一的進(jìn)程號(hào)Pid，PS實(shí)體進(jìn)程號(hào)為0，MS實(shí)體進(jìn)程號(hào)為1。PS首先向MS發(fā)送消息Msg1，MS收到消息后返回消息Msg2，由此可知協(xié)議執(zhí)行順序與協(xié)議設(shè)計(jì)一致。

在WBAN_DPAP協(xié)議中，PS與MS實(shí)體間完成相互認(rèn)證，需要滿(mǎn)足協(xié)議安全性的LTL公式表示如下：

其中，&&表示與運(yùn)算，[]P表示P在所有狀態(tài)點(diǎn)都成立，<>P表示P最終會(huì)在某些狀態(tài)點(diǎn)成立。

采用Dolev-Yao模型對(duì)非法攻擊者Intruder進(jìn)行建模。攻擊者在協(xié)議通信過(guò)程中竊取消息并進(jìn)行存儲(chǔ)，然后選擇一個(gè)消息接收者進(jìn)行消息的重放。攻擊者的Promela建模示意圖如圖6所示。

圖6 Intruder的通信建模示意圖

從圖中可以看出，攻擊者通過(guò)截獲PS與MS之間通信的消息達(dá)到攻擊目的。加入攻擊者模型后，對(duì)協(xié)議需滿(mǎn)足的LTL屬性進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如圖7所示。圖中“Full statespace search for”表示默認(rèn)為完全的狀態(tài)空間搜索?！癝tate-vector 64 byte，depth reached 26”表示完全描述一個(gè)全局系統(tǒng)的狀態(tài)需要64 Byte的內(nèi)存，最長(zhǎng)深度優(yōu)先搜索路徑包含26個(gè)從樹(shù)根開(kāi)始的轉(zhuǎn)移?！癳rrors：0”表示在這次搜索過(guò)程中沒(méi)有發(fā)生錯(cuò)誤，即協(xié)議滿(mǎn)足LTL公式描述的屬性?！?28.730 total actual memory usage”表示該協(xié)議進(jìn)行檢測(cè)時(shí)數(shù)據(jù)使用的內(nèi)存空間總字符為128.73 MB[18]。

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

5 結(jié)束語(yǔ)

本文在前人基于生物信息和傳統(tǒng)密碼學(xué)的研究基礎(chǔ)上，提出一種適用于無(wú)線(xiàn)體域網(wǎng)的動(dòng)態(tài)口令雙向認(rèn)證輕量級(jí)協(xié)議。通過(guò)理論證明和SVO邏輯推理方法驗(yàn)證了WBAN_DPAP認(rèn)證協(xié)議的安全屬性。使用SPIN模型檢測(cè)工具對(duì)協(xié)議進(jìn)行建模實(shí)驗(yàn)，實(shí)驗(yàn)結(jié)果表明，WBAN_DPAP認(rèn)證協(xié)議滿(mǎn)足安全性目標(biāo)。

該協(xié)議將時(shí)間同步認(rèn)證機(jī)制與一次性密碼相結(jié)合，使用時(shí)間戳和隨機(jī)數(shù)作為雙重身份驗(yàn)證因素，采用非對(duì)稱(chēng)加密算法對(duì)通信消息進(jìn)行加密，整個(gè)方案安全性更高且輕量。下一步工作，繼續(xù)研究本文提出的無(wú)線(xiàn)體域網(wǎng)認(rèn)證協(xié)議的資源占用率和能耗，在保證安全的前提下，進(jìn)一步減少其資源消耗。