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

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

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

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

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