基于模型檢測的無線體域網安全協議形式化驗證

基于模型檢測的無線體域網安全協議形式化驗證

陳鐵明，虞震波，王婷，方趙林

(浙江工業大學 計算機科學與技術學院，浙江 杭州 310023)

摘要：在研究無線體域網(WBAN)安全屬性的基礎上，為了對無線體域網安全協議進行安全分析，保證協議設計之初的安全性，提出并實現了一種基于模型檢測的無線體域網安全協議形式化分析和驗證方法.基于模型檢測工具PAT研究建模語言CSP#及其擴展方法，提出一種支持網絡節點可移動的抽象建模數據結構，便于對WBAN協議的形式化建模；根據Dolev-Yao模型，結合WBAN節點位置的可移動性，建立攻擊者抽象模型.以Chitra等提出的基于雙天線的WBAN安全協議為例，在PAT工具中應用筆者提出的方法對其進行建模并加以分析驗證，體現了方法的實用性. 2) CU與待認證傳感器節點的建模如下：

關鍵詞：無線體域網；模型檢測；安全協議；PAT；CSP#；線性時序邏輯

收稿日期：2015-04-17

基金項目：國家自然科學基金資助項目(61103044)

作者簡介：陳鐵明(1978—)，男，浙江諸暨人，副教授，博士，研究方向為網絡信息安全，E-mail:tmchen@zjut.edu.cn.

中圖分類號：TP309.7

文獻標志碼：A

文章編號：1006-4303(2015)05-0497-06

Abstract:Based on the research of wireless body area network (WBAN) security attributes, a formal analysis and verification method for WBAN security protocols is proposed and implemented in this paper. The method can ensure the security of WBAN protocols in the early stage of protocol design. First, the modeling language CSP# which is supported by the model checker PAT is extended with an abstract modeling data structure supporting the node mobility, which could simplify the modeling of WBAN protocols. Then, an abstract attacker model is established through the combination of Dolev-Yao model and WBAN node mobility. Finally, the WBAN security protocol proposed by Chitra et al. is modeled and verified using our method embedded in PAT, which reflects the usability and efficiency of this method.

Keywords:wireless body area networks; model checking; security protocols; PAT; CSP#; linear temporal logic

Formal verification of wireless body area network security

protocols based on model checking

CHEN Tieming, YU Zhenbo, WANG Ting, FANG Zhaolin

(College of Computer Science and Technology, Zhejiang University of Technology, Hangzhou 310023, China)

隨著無線通信技術和無線傳感技術的不斷發展，無線傳感器網絡的研究和應用獲得了巨大成功[1-4].無線體域網(Wireless body area network, WBAN)是無線傳感網在智能定位、醫學領域的分支，主要應用于人體區域,負責采集人體機能數據以供醫療分析[5].安全協議作為構成無線傳感網絡的關鍵部分，其數據的安全性、認證的可靠性是制約WBAN正常通信的最重要因素.自從Dolev和Yao提出將模型檢測技術應用于安全協議分析和驗證[6]，模型檢測技術以其簡潔明了的建模過程和高度自動化的分析驗證成為了當前主流的形式化分析技術[7].Aladdin等通過時序Petri網對網絡協議進行建模，確保了協議的正確可靠[8].Kashif等使用SPIN模型[9]檢測工具對WSN路由協議進行形式化分析，發現了攻擊漏洞[10].Lowe利用進程代數使用CSP(Communicating sequential process)方法[11]對NSPK協議進行了形式化分析，發現了一個十幾年來未知的攻擊.2015年Wang等使用模型檢測技術對WBAN的MAC層安全協議做了形式化分析[12].然而目前對WBAN安全協議的形式化分析工作仍比較少，因此對WBAN安全協議進行形式化分析驗證的重要性不言而喻.

上述方法均采用某種形式化建模語言實現對安全協議的形式化描述，進而被相應支持該形式化語言的工具接受并實現自動化模型檢測過程.雖然模型檢測工具的自動化驗證程度高，分析過程嚴謹，但是系統建模的過程仍比較復雜，需要具有專業知識經驗的人工支持，建模過程的好壞直接影響到驗證結果的正確性.因此面向不同應用領域定制開發專用的建模語言也是一種發展趨勢.利用新型模型檢測工具PAT(Process analysis toolkit)框架[13]的高度可擴展性，提出一個基于數據結構的CSP#語言擴展模塊，提高WBAN安全協議的形式化建模和分析效率，實現了一種面向WBAN位置相關安全協議的專用建模與驗證方法.

1PAT模型檢測工具

PAT是由新加坡國立大學PAT研究小組自主開發的一套模型檢測工具，支持并發、實時系統、UML狀態機等系統的建模驗證，能夠對CSP#，RTS，LTS等多種語言進行模擬驗證和反例生成.

PAT是一個可擴展、模塊化的通用架構，其系統框架[14]如圖1所示，整個框架分為4層，這種分層架構方便了模塊的擴展，并將建模驗證過程分為3步：編譯、抽象和驗證.從圖1中可以看出：最上層的建模層(Modeling layer)，包含了多個不同領域、不同目標系統的建模模塊，可以使用某種建模語言(如CSP#)對不同的系統進行建模；第二層是抽象層(Abstraction layer)，能夠對上層已經建模完成的系統進行抽象分析，包括對不同系統的數據、環境等的抽象；第三層是中間呈現層(Intermediate representation layer)，負責將輸入的系統模型轉化為一種中間狀態(如標簽遷移系統LTS)，以對應底層不同的模型檢測算法；底層是分析層(Analysis layer)，包含模型檢測技術的關鍵算法，如死鎖檢測算法、LTL性質檢測算法等.

PAT工具具有如此良好的擴展性，因此可以利用建模層的抽象功能對建模層語言模塊進行抽象，擴展PAT的CSP#模塊(即并行模塊)，方便WBAN領域安全協議的建模驗證.抽象后的語言模塊能夠自動轉化為PAT已經支持的語言，從而簡化系統描述和實現過程，使得建模過程更人性化、更易使用.借助PAT工具良好的擴展性，可方便對WBAN安全協議的建模.

圖1　模型檢測工具PAT的系統框架圖 Fig.1　The system framework of PAT

2無線體域網節點位置建模

2.1基于雙天線的無線體域網協議

無線體域網節點位置隨著人的移動而變化，且傳感器節點體積小、容量和能源有限，很容易受到外界的攻擊，導致WBAN安全問題層出不窮.為此，Javali等首次提出了基于雙天線的無線體域網安全認證方案[15]，該方案基于接受信號強度(Received signal strength, RSS)，利用雙天線本身位置的分離性，能夠有效的將攻擊手段排除在其射頻范圍外.

該方案模型假設有一個雙天線的可信任實體節點CU和若干個單天線的待認證節點，圖2給出了CU和傳感器節點布置圖.圖中節點E為攻擊者節點，B為誠實實體節點，A1和A2分別代表CU的兩條天線.從圖2中可以看出：節點E到A1,A2的距離分別為e1,e2，節點B到A1,A2距離為d1,d2.

圖2　無線體域網安全認證協議模型節點布置圖 Fig.2　The node layout of WBAN security authentication protocol model

節點E與可信任節點CU之間的通信過程如下：

1) CU→E:Probe={IDcu}

2) E→CU:Resp[0]={IDE,P0,L0,K0}

…

i) E→CU:Resp[i]={IDE,Pi,Li,Ki}

…

n) E→CU:Resp[n]={IDE,Pn,Ln,Kn}

其中：Pi為發送方發送消息時的能量；Ki為隨機數；Li為發送方的位置信息.

首先CU給傳感器節點向其射頻范圍內廣播一個探測包Probe用以發現未認證節點，傳感器節點收到探測包后發送一個響應包Resp[i]，包含節點此時的發送能量，位置信息以及隨機數，CU收到響應包后，計算包的RSSI(Receivedsignalstrengthindication)值為

其中：di為此時傳感器節點與CU的距離；α為節點間的距離能量指數.

計算A1和A2的RSSI平均值RDavg，計算公式為

其中：j={1,2,…,n}，n為p和q之間的較小值.

4) CU將RDavg和RSSI門檻值RDth進行比較，將小于RDth的傳感器節點視為攻擊者節點，大于RDth的傳感器節點則為誠實節點.最后CU給誠實節點發送AssocResp[ACCEPT]消息.

2.2支持節點可移動的抽象方法

由于人的日常行為使WBAN節點位置經常發生移動，要求在建模過程中考慮節點可能移動到的位置，加大了建模的復雜度.利用CSP#語言的擴展性對節點的移動進行抽象，可以有效提高建模的準確率，下面采用二維坐標對傳感節點的位置信息進行抽象：

public class Location: ExpressionValue {

public intx; //節點位置x坐標

public inty; //節點位置y坐標

public int CalculateDistance(Location){…}

…

};

類Location中包含節點的二維坐標，并通過自定義函數CalculateDistance()計算兩個節點間的歐氏距離，從而判斷節點位置是否移動或超出射頻范圍.例如，假設節點A和B的位置信息分別為(xa,ya)，(xb,yb)，R表示節點傳輸距離，當((xa-xb)(xa-xb)+(ya-yb)(ya-yb))>R·R時，說明節點A和B間的距離超出了節點的射頻范圍.

知識集類KnowledgeSet用于存儲協議執行過程中的數據信息，如：ID，隨機數等會直接影響協議能否正常執行的變量.其中內置SortedListlist用于存儲某個節點的知識，并隨著協議執行不斷更新，UnitType表示知識類型，Object表示知識內容.比如SortedList存儲了節點E的位置信息.UnitType枚舉了協議中所有的常量，枚舉類型保證了協議執行過程中變量的值不會沖突.

public class KnowledgeSet : ExpressionValue {

public SortedList list;

public bool Add(UnitType, Object); //增加知識集

public Object Get(UnitType); //提取知識集

…

};

在上述抽象的基礎上，封裝成WSNNode結構，擴展PAT建模層的CSP#語言模塊，加入新的函數庫和語義，WSNNode類圖如圖3所示.

圖3　面向WBAN傳感節點建模的WSNNode類圖 Fig.3　The class diagram of WBAN sensor model

WSNNode結構代表傳感器節點，其中包含了協議正常執行的所有信息，包括節點ID、傳輸半徑、位置信息、知識集信息、隨機數等內容.WSNNode結構和新函數庫的設計極大地簡化了WBAN安全協議的建模與驗證.

3形式化建模與驗證

3.1WBAN協議形式化建模及性質描述

3.1.1協議誠實實體節點建模

采用有窮狀態機描述協議中信任節點CU在協議執行過程中的狀態遷移情況，如圖4所示.

圖4　協議信任節點CU的狀態轉換圖 Fig.4　The State transition diagram of trusted sensor CU

圖4中idle為CU的初始狀態；當CU廣播一個探測包后自動跳轉到State1狀態，并等待有未認證的傳感器節點回送ACK確認消息；收到ACK確認消息后跳轉到State2狀態，判斷響應節點是否在其射頻范圍內；若在其射頻范圍內，則與響應節點重復交互n次消息，這n次消息由CU的兩條天線A1和A2隨機接收，結束交互后跳轉到State3狀態；State3狀態將計算著n次消息RSSI值的平均值RDavg，并跳轉到State4狀態；State4狀態將RSSI平均值與門檻RDth進行比較，若RDavg>RDth則該傳感器節點為合法節點，認證結束，跳轉到idle狀態；否則，認證失敗，重新跳轉到idle狀態.

需要注意的是，在認證過程中，響應節點可能會移動節點位置，同樣信任節點CU在認證過程中也會移動節點位置.

下面介紹如何利用基于CSP#擴展的利用抽象節點可移動的建模方法對協議信任節點CU進行建模.先對接下來需要涉及的CSP#語言語法進行簡單說明：P()=Exp代表一個進程或某主體的行為，其中()內可帶參數，Exp代表過程描述，例如P()=e→P()代表進程P循環執行事件e；事件e可帶參數，例如e.exp1.exp2，其中exp1和exp2為變量；符號?和!代表輸入輸出通道，其中?為接受消息，!為發送消息；[]代表選擇，例如公式P[]Q表示可能執行P，也可能執行Q.

1) 定義兩個全局消息通道，作為協議中實體間消息傳遞的載體：

channel ca 0;

channel cb 0;

其中：通道ca用于承載CU廣播探測包的消息；通道cb用于傳遞CU與待認證傳感器節點的n條重復消息，由于這n條消息的格式相同，故用同一通道代替.

PInitPre(NodeCU, Loc) =//初始化CU節點信息

IntruderInitial {

Node_A1.addItem(NodeCU, Loc, LCU_A1);

Node_A2.addItem(NodeCU, Loc, LCU_A2);

} -> PInit ();

PInit()=//開始執行協議

ca! Node_A1. everyone -> PInit() []

ca! Node_A2. everyone -> PInit() []

ca? Node_A1. to1 -> PInit() []

ca? Node_A2. to1 -> PInit() []

cb! Node_A1. tox. Power. Loc. Nonce -> PInit()[]

cb! Node_A2. tox. Power. Loc. Nonce -> PInit();

變量LCU_A1與LCU_A2分別代表了CU的兩條天線，其位置坐標距離相差1 cm.LE代表攻擊節點的位置信息.用一個枚舉類型來初始化各個節點的ID信息，以避免重復ID的現象.

3.1.2節點可移動的攻擊者建模

對攻擊者E的建模最為復雜.結合攻擊者位置的可移動性以及攻擊者可以利用改變發送功率的方式偽造信號強度，對Dolev-Yao模型[16]進行擴展，攻擊者節點應具有以下能力：

1) 可以竊聽并截獲協議執行過程中節點傳輸的消息，以竊取CU的正常通信范圍.

2) 可以冒充協議誠實節點發送消息.

3) 根據截獲的消息，動態增長自己的知識集(KnowledgeSet對象)，從而產生新的攻擊消息.

4) 利用節點可移動性，在誠實節點射頻范圍外利用功率大、收發能力強的收發器向周圍節點發送信息，誘使周圍節點認為攻擊節點在其射頻范圍內.

使用基于CSP#擴展抽象節點可移動的建模方法對攻擊者E建模，主要分為兩大部分：一、對網絡中的消息進行截獲，破壞誠實節點與CU的正常通信，以及竊取正常節點的信息；二、攻擊者移動位置，偽裝成誠實節點與CU通信.關鍵代碼如下：

PIntruderPre(NodeE, Loc) =

IntruderInitial {

NodeE.addItem(NodeE, Loc);

} -> PIntruder();

PIntruder() =

cA?ID_X . to1 ->//截獲并存儲消息

InterceptChanA {

…//截獲通道ca中的探測包并保存.

NodeE.addItem(…) ;

}-> PIntruder() []

cA?ID_X . to1. PowerX. LocX. NonceX ->

InterceptChanA {

…//截獲通道cb中的認證消息并保存.

NodeE.addItem(…) ;

}-> PIntruder() []

//重放截獲的消息或根據獲取知識產生新消息

cA! NodeE. tox -> PIntruder() []

cB! NodeE. tox. Power. Loc. Nonce -> PIntruder() ;

攻擊者節點通過NodeE.addItem()函數將截獲的消息存入知識集KnowledgeSet對象中，隨后從知識集KnowledgeSet中任意選取ID、能量值、位置信息、隨機數組合成一個節點Node發送到通道中，攻擊者將枚舉所有可能的組合.

為了抽象節點的射頻范圍內的所有移動可能性，在初始階段定義了信任節點CU和攻擊者E的傳輸距離RadiusCU和RadiusE，給出如下PAT模型用于自動生成所有可能的節點位置：

[]x1:{0…RadiusCU};y1:{0…RadiusCU};x2:{0…RadiusE};y2:{0…RadiusE}

@(PInitPre(NodeCU,newLocation(x1,y1))|||PIntruderPre(NodeE,newLocation(x2,y2)))

其中：符號[]表示x,y每次在其取值范圍內任取一個值；|||表示協議發起方與接收方并發執行.

針對位置可移動的情況，攻擊者節點對位置的選擇不局限于其自身的可移動范圍RadiusE.在最后的實驗結果中我們可以看到，若RadiusE與CU的射頻范圍RadiusCU有重疊則攻擊者可冒充誠實節點與CU通信，所以攻擊者的行為是不確定的，它的執行是無限循環上述代碼，枚舉所有可能的狀態，從而能夠搜索整個狀態空間.

3.1.3LTL性質描述

采用線性時序邏輯[17](Linear temporal logic, LTL)對協議屬性進行規范描述.為了更方便的描述協議性質，對CSP#擴展定義如下變量：

#defineiniRunningEU(req_CU==true)；//當攻擊者節點偽裝成誠實節點給信任節點CU回送ACK確認消息時置true.

#defineresCommitEU(ack_2_E==true)；//當CU與節點E完成n次消息交互，并完成認證時置true.

#defineMoveInRadius(OutRadius==true)；//當攻擊者節點移入CU的射頻范圍時置true.

協議的認證性是指確認對方的真實身份，并保證其真實身份與消息中所聲稱的身份相一致.分析Chitra等提出的WBAN安全協議時，采用文[15]的方法進行檢測：當攻擊者E收到信任節點CU廣播的探測包，則待認證的響應方E必須回送一個確認消息，同時開始認證過程，此時攻擊者E的位置必定在CU的射頻范圍內.因此可用LTL公式G:[](MoveInRadius→<>!(iniRunningEU→resCommitEU))表示協議的認證性.其中<>表示最終(eventually)，[]表示一直(always)，!表示否定.若公式G不滿足，則表示有攻擊者闖入CU的射頻范圍內，并認證成功.

3.2實驗結果與分析

將WBAN安全認證協議的抽象CSP#模型和上一小節描述的LTL性質導入PAT工具中進行模擬驗證.結果顯示公式G驗證失敗，其反例路徑如圖5所示.

圖5　反例路徑圖 Fig.5　The path diagram of counter-example

反例路徑中間欄是被攻擊者截獲或篡改的消息，節點CU的兩條天線初始位置分別為(0,0)和(0,1)，節點E的初始位置為(0,6)，在與CU進行認證的過程中位置移動到(0,4)，此時節點E已移入CU的射頻范圍，并在射頻范圍內停留足夠長的時間，從而滿足文[15]對認證性的描述并完成認證.說明此種基于雙天線的WBAN安全協議存在缺陷：無法抵御可移動攻擊者的入侵.結合原始協議可以得出驗證失敗的原因：當節點E移入CU的射頻范圍內時，CU計算出的RSSI值大于RSSI門檻值RDth，若節點E在CU的射頻范圍內的時間足夠長，則n次消息認證的RSSI平均值RDavg將大于RDth，最終認證成功.

4結論

在PAT工具的基礎上，提出了一種支持節點可移動的抽象建模數據結構，擴展了CSP#語言模塊.對Chitra等提出的安全認證方案進行建模和分析，發現若可移動攻擊者的移動范圍與信任節點CU的射頻范圍有交集，則有被攻擊的可能.研究發現：對建模過程進行抽象能夠有效降低建模的復雜性，更直觀地發現協議存在的問題，體現了抽象方法的實用性.因此下一步的研究將在更高層次抽象建模語言和模塊，針對無線體域網領域開發專用建模語言，并研究抽象描述語言和CSP#的自動轉換，實現模型檢測真正的自動化.

參考文獻：

[1]陳鐵明,江頡,王小號,等.一種改進的基于位置的攻擊容忍WSN安全方案[J].傳感技術學報,2012,25(4):545-551.

[2]陳慶章,張海洋,陳辰,等.基于WSN的人體姿態辨識系統設計[J].浙江工業大學學報,2014,42(6):591-593.

[3]周曉,李杰,邊裕挺.基于無線傳感網絡的環境溫度檢測系統設計[J].浙江工業大學學報,2013,41(4):440-443.

[4]陸歡佳,俞立,董齊芬,等.基于無線傳感網的樓宇環境檢測系統設計[J].浙江工業大學學報,2011,39(6):683-687.

[5]JURIK A, WEAVER A. Remote medical monitoring[J]. Computer,2008,41(4):96-99.

[6]NOVOTNY M. Formal analysis of security protocols for wireless sensor networks[J]. Tatra Mountains Mathematical Publications,2010,47(1):81-97.

[7]林惠民,張文輝.模型檢測：理論、方法與應用[J].電子學報,2002,30(12A):1907-1912.

[8]ALADDIN M, THOMAS B, ARMAND T. Network protocol modeling: a time Petri net modular approach[C]//16th International Conference on Software, Telecommunications and Computer Networks. Split: IEEE Press,2008:273-277.

[9]HOLZMANN G J. The spin model checker primer and reference manual[M]. New Jersey: Addison Wesley,2003.

[10]JAVED K, KASHIF A, TROUBITSYNA E. Implementation of spin model checker for formal verification of distance vector routing protocol[J]. International Journal of Computer Science and Information Security,2010,8(3):1-6.

[11]LOWE G, ROSCOE B. Using CSP to detect errors in the TMN protocol[J]. IEEE Transactions on Software Engineering,1997,23(10):659-669.

[12]WANG Y Y, DONG H L, YU Y T, et al. Analyzing IEEE802.15.6 protocol with stochastic model checking[J]. Journal of Computational Information Systems,2015,11(3):935-947.

[13]SUN J, LIU Y AND DONG J S. Model checking CSP revisited: introducing a process analysis toolkit[J]. Communications in Computer and Information Science,2009,17(7):307-322.

[14]LIU Y, SUN J, DONG J S. Developing model checkers using PAT[C]//8th International Symposium on Automated Technology for Verification and Analysis. Sydney: Springer Press,2010:371-377.

[15]JAVALI C, REVADIGAR G, LIBMAN L, et al. SeAK: secure authentication and key generation protocol based on dual antennas for wireless body area networks[C]//10th International Workshop. Oxford: Springer Press,2014:74-89.

[16]DOLEV D, YAO A C. On the security of public key protocols[J]. IEEE Transactions on Information Theory,1981,29(2):350-357.

[17]BAIER C, KATOEN J P, LARSEN K G. Principles of model checking[M]. Cambridge: The MIT Press, 2008.

(責任編輯：劉巖)