基于SPI演算的移動(dòng)自主網(wǎng)絡(luò)安全路由協(xié)議分析.pdf

1、在移動(dòng)自主網(wǎng)絡(luò)中協(xié)議是主要的研究領(lǐng)域之一，由于移動(dòng)自主網(wǎng)絡(luò)的性質(zhì)與傳統(tǒng)有線網(wǎng)絡(luò)比較起來又形成了許多新的挑戰(zhàn)，已存在的路由協(xié)議大多是資源集中型的，不適合于移動(dòng)自主網(wǎng)的特點(diǎn)和應(yīng)用，針對移動(dòng)自主網(wǎng)的特點(diǎn)，應(yīng)用不同的方法來解決移動(dòng)自主網(wǎng)的路由協(xié)議已被提出，安全路由協(xié)議也正在研究和提出，IETF(互聯(lián)網(wǎng)絡(luò)工程任務(wù)組)針對此目標(biāo)也成立一個(gè)MANET工作小組。安全路由協(xié)議的分析是一個(gè)復(fù)雜的問題，安全路由協(xié)議的安全性滿足與否直接影響到移動(dòng)自主網(wǎng)的推廣與

2、應(yīng)用。在安全路由設(shè)計(jì)的早期工作中若沒有相應(yīng)的方法來檢測路由協(xié)議的安全性，潛在的協(xié)議漏洞沒有合適的方法來檢測，則網(wǎng)絡(luò)操作很容易被攻擊而不能工作，就會(huì)造成許多不必要的浪費(fèi)。針對此目的，目前已有許多推理方法應(yīng)用于安全路由協(xié)議的分析，但這些方法大都是模擬方法以及邏輯推理和狀態(tài)空間搜索，通過對有限的狀態(tài)、結(jié)點(diǎn)分析得出結(jié)論。這些方法至少得到下面這兩個(gè)不令人滿意的方面：(一)沒有明確的“安全”路由的定義，所以不同的作者應(yīng)用不同的方法來解釋安全性，并且

3、應(yīng)用不同的需要來設(shè)計(jì)他們的安全路由協(xié)議，結(jié)果不同的方法的屬性難以比較；(二)沒有嚴(yán)格的數(shù)學(xué)方法來證明一個(gè)提出的安全路由協(xié)議。事實(shí)上許多被提出的協(xié)議如SRP和Kerberos都有缺陷，在一定意義上都沒有達(dá)到作者所聲稱的安全屬性；明顯的原因是缺乏充分的證明技術(shù)。 應(yīng)用形式化分析安全路由的方法還很少，應(yīng)用進(jìn)程代數(shù)的來分析的方法更少。應(yīng)用進(jìn)程代數(shù)的方法來分析安全路由的安全性，能克服非形式化中不必要的人為干預(yù)和經(jīng)驗(yàn)推理，能嚴(yán)格按照數(shù)學(xué)的語

4、法、語義來實(shí)現(xiàn)安全目標(biāo)的分析。 本文研究基于SPI演算的移動(dòng)自主網(wǎng)絡(luò)的安全路由協(xié)議分析是把進(jìn)程代數(shù)中SPI演算引入到MANET中，并進(jìn)行安全路由協(xié)議分析，主要是由于SPI演算具有豐富的語法、語義和成熟的推理過程，使得安全路由協(xié)議的分析有一個(gè)嚴(yán)格的算法過程。 對著名的SRP路由協(xié)議我們用SPI演算來分析其過程，在本文提出的攻擊者模型下，在相關(guān)的安全目標(biāo)下，SRP路由協(xié)議暴露出一定的脆弱性，我們分析其脆弱性的原因，指出設(shè)計(jì)S