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

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

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

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