基于顏色Petri網(wǎng)的無(wú)線Mesh網(wǎng)路由安全建模與驗(yàn)證.pdf

1、隨著3G網(wǎng)絡(luò)與無(wú)線局域網(wǎng)的普及,無(wú)線網(wǎng)絡(luò)通信技術(shù)已經(jīng)在我們的日常生活中無(wú)處不在了。無(wú)線Mesh網(wǎng)(Wireless Mesh Network)簡(jiǎn)稱WMN作為一種新型的無(wú)線網(wǎng)絡(luò),由于其自組織,自適應(yīng),成本低,多跳,與其他網(wǎng)絡(luò)兼容好等特點(diǎn)逐漸成為下一代無(wú)線通信的核心技術(shù)。盡管現(xiàn)在的無(wú)線網(wǎng)絡(luò)中有很多安全機(jī)制來(lái)保障網(wǎng)絡(luò)安全,但由于無(wú)線 Mesh網(wǎng)自身的特點(diǎn),這些安全機(jī)制不能完全地應(yīng)用到無(wú)線Mesh網(wǎng)中。路由安全是無(wú)線Mesh網(wǎng)安全的一個(gè)重要方面

2、,網(wǎng)絡(luò)的安全傳輸,離不開(kāi)路由協(xié)議的安全保障,惡意節(jié)點(diǎn)通過(guò)攻擊路由協(xié)議,假冒正常的節(jié)點(diǎn)并且插入偽造路由信息來(lái)攻擊網(wǎng)絡(luò),一旦路由協(xié)議受到攻擊,其余的安全措施都變得毫無(wú)意義。
　　安全協(xié)議的形式化驗(yàn)證方法是指用數(shù)學(xué)或者邏輯模型對(duì)所建立的模型進(jìn)行分析驗(yàn)證,從而在理論上證明其安全性。顏色Petri網(wǎng)是一種圖形化的建模語(yǔ)言,采用顏色 Petri網(wǎng)對(duì)安全問(wèn)題進(jìn)行建模分析具有很多獨(dú)特的優(yōu)點(diǎn)。比如,顏色Petri網(wǎng)有自動(dòng)化分析工具如CPN Tool

3、;可以采用狀態(tài)空間分析和關(guān)聯(lián)矩陣分析;用顏色 Petri網(wǎng)建模可以有效地驗(yàn)證安全協(xié)議的安全性,顏色 Petri網(wǎng)不但可以檢測(cè)出模型中存在攻擊,當(dāng)安全協(xié)議中沒(méi)有攻擊時(shí),顏色Petri網(wǎng)可以有效地證明其安全性。因此研究基于顏色Petri網(wǎng)的無(wú)線Mesh網(wǎng)安全協(xié)議建模和驗(yàn)證具有重要的理論意義和應(yīng)用價(jià)值。
　　本文通過(guò)分析研究現(xiàn)有無(wú)線 Mesh網(wǎng)路由協(xié)議的運(yùn)行機(jī)制和各種形式化驗(yàn)證方法,首次提出了用顏色 Petri網(wǎng)對(duì)無(wú)線 Mesh網(wǎng)路由協(xié)

4、議 HWMP進(jìn)行建模和安全驗(yàn)證。通過(guò)對(duì)HWMP路由協(xié)議進(jìn)行建模分析,Petri網(wǎng)模型可以有效地模擬仿真HWMP路由協(xié)議按需路由建立過(guò)程。用狀態(tài)空間方法和CPN Tool仿真實(shí)驗(yàn)分析該模型,可以證明該模型中是否存在黑洞攻擊。對(duì)于存在黑洞攻擊的模型,通過(guò)研究現(xiàn)有的基于密碼機(jī)制的安全路由方案和基于信任和檢測(cè)機(jī)制的安全路由方案,本文提出了一種基于公開(kāi)密鑰加密機(jī)制的安全路由算法,用NS2對(duì)基于公開(kāi)密鑰機(jī)制的安全方案進(jìn)行仿真實(shí)驗(yàn),實(shí)驗(yàn)結(jié)果說(shuō)明該安全