移動adhoc網(wǎng)絡(luò)安全路由協(xié)議分析方法研究.pdf

1、移動ad hoc網(wǎng)絡(luò)已經(jīng)成為一個熱門的研究領(lǐng)域，在很多方面都有著廣泛的應(yīng)用。由于其自身網(wǎng)絡(luò)特點，移動ad hoc網(wǎng)絡(luò)容易受到各種攻擊，路由協(xié)議作為網(wǎng)絡(luò)最重要的基本功能，更容易成為攻擊者的目標。近年來，學者們已經(jīng)提出多個移動ad hoc網(wǎng)絡(luò)安全路由協(xié)議，但是這些協(xié)議的安全性大多通過直接觀察或者網(wǎng)絡(luò)仿真等非形式化方法進行分析，所以，很多安全路由協(xié)議后來都被發(fā)現(xiàn)存在安全漏洞。
　　目前已經(jīng)有學者開始嘗試使用形式化方法分析移動ad hoc

2、網(wǎng)絡(luò)路由協(xié)議的安全性，本文主要對目前的這些形式化方法進行研究，特別是針對基于模擬模型的方法和具有自動化分析能力的形式化方法。論文工作主要圍繞國家自然科學基金重點項目(U1135002)的研究任務(wù)進行展開，研究內(nèi)容概括為如下幾個部分：
　　首先研究了基于模擬模型的針對按需源路由協(xié)議分析的ABV模型。指出ABV模型實際上要分析的網(wǎng)絡(luò)環(huán)境允許存在多個惡意節(jié)點，并且可以共謀，但是該模型中以不合理的理由將這些惡意節(jié)點合并，限制了惡意節(jié)點的攻

3、擊能力，巧妙地回避了本來在ABV模型中要解決的關(guān)鍵問題。證明了endairA協(xié)議安全性證明過程中存在錯誤，在ABV模型下可證明安全的路由協(xié)議不能保證可以抵御wormhole攻擊。指出了ABV模型回避了協(xié)議的鄰居發(fā)現(xiàn)過程，定義安全路由的目標為發(fā)現(xiàn)plausible route，在實際網(wǎng)絡(luò)拓撲下不一定是存在的，且plausible route的定義回避了惡意節(jié)點可以表現(xiàn)成多個標識的情況，證明了ABV模型中plausible route的定義

4、減弱了模型的分析能力，在ABV模型下可證明安全的路由協(xié)議不能保證可以抵御Sybil攻擊。發(fā)現(xiàn)了一種針對endairA協(xié)議的隱蔽信道攻擊，該攻擊完全是在ABV模型的假設(shè)下進行的，使得endairA協(xié)議接受非plausible route，從而說明該協(xié)議即使在ABV模型下也是不安全的，證明了ABV模型對隱蔽信道攻擊的分析并不完全，該模型下可證明安全的路由協(xié)議，仍然易受新的隱蔽信道攻擊，不能滿足其安全目標。
　　其次研究了基于模擬模型的

5、針對按需距離矢量路由協(xié)議分析的擴展ABV模型。證明了擴展ABV模型敵手節(jié)點的合并減弱了模型的分析能力，在擴展ABV模型下可證明安全的路由協(xié)議不能保證抵御wormhole攻擊；模型中正確系統(tǒng)狀態(tài)的定義減弱了模型的分析能力，在擴展ABV模型下可證明安全的路由協(xié)議不能保證抵御Sybil攻擊；分析了擴展ABV模型下ARAN協(xié)議安全性證明過程中的錯誤，并給出一個攻擊實例，表明該模型下可證明安全的ARAN協(xié)議仍然存在安全漏洞。
　　最后研究了