Ad hoc網(wǎng)絡協(xié)議安全性的形式化驗證研究.pdf

1、無線移動Adhoc網(wǎng)絡(MANET，以下簡稱AdHoc網(wǎng)絡)作為沒有基礎設施的網(wǎng)絡，在軍事和民用方面具有廣闊的應用前景，是目前網(wǎng)絡研究中的熱點問題。隨著近年對Adhoc網(wǎng)絡安全的研究，相關的Adhoc網(wǎng)絡協(xié)議也在不斷的改進和完善中，網(wǎng)絡中的攻擊者以及協(xié)議無窮多個會話的并發(fā)交疊運行使得協(xié)議運行時往往難以實現(xiàn)它的設計目標，對協(xié)議的安全性分析和驗證顯得至關重要。形式化的方法已被證明是分析和驗證安全協(xié)議的有效手段，但常規(guī)的形式化方法，如Need

2、ham等人提出的BAN邏輯以及后來改進的AT邏輯及SVO邏輯、Perti模型、有限狀態(tài)模型(FSM)及隨機預言機模型等方法大都是理想狀態(tài)空間的理論推導，邏輯性、理論性都較強，驗證過程需要很長的推理步驟，為了直觀而又嚴密的驗證協(xié)議，我們采用了AVISPA協(xié)議驗證工具。 本文以Adhoc網(wǎng)絡協(xié)議安全性的形式化驗證為研究對象，以有效的形式化驗證方法為主要研究內容。本文的創(chuàng)新點如下： 1、通過分析比較幾種常用的形式化分析方法的優(yōu)

3、點與缺點，選擇AVISPA工具集作為協(xié)議安全的形式化分析工具。 2、針對相關文獻上討論的ARAN協(xié)議能否防御內部節(jié)點攻擊的問題，采用HLSPL語言對ARAN協(xié)議建立了抽象模型，利用AVISPA工具集形式化驗證分析了ARAN協(xié)議的安全性問題，證實了ARAN協(xié)議在存在惡意節(jié)點攻擊的情況下能夠成功抵御這類攻擊。 3、隨著網(wǎng)絡編碼技術在Adhoc網(wǎng)絡中的應用，網(wǎng)絡編碼協(xié)議的安全性驗證也成為一個新的研究課題。針對網(wǎng)絡編碼同態(tài)簽名方