移動(dòng)ad hoc網(wǎng)絡(luò)安全路由協(xié)議分析方法研究
發(fā)布時(shí)間：2018-11-06 20:52
【摘要】：移動(dòng)ad hoc網(wǎng)絡(luò)已經(jīng)成為一個(gè)熱門的研究領(lǐng)域,在很多方面都有著廣泛的應(yīng)用。由于其自身網(wǎng)絡(luò)特點(diǎn),移動(dòng)ad hoc網(wǎng)絡(luò)容易受到各種攻擊,路由協(xié)議作為網(wǎng)絡(luò)最重要的基本功能,更容易成為攻擊者的目標(biāo)。近年來,學(xué)者們已經(jīng)提出多個(gè)移動(dòng)ad hoc網(wǎng)絡(luò)安全路由協(xié)議,但是這些協(xié)議的安全性大多通過直接觀察或者網(wǎng)絡(luò)仿真等非形式化方法進(jìn)行分析,所以,很多安全路由協(xié)議后來都被發(fā)現(xiàn)存在安全漏洞。目前已經(jīng)有學(xué)者開始嘗試使用形式化方法分析移動(dòng)ad hoc網(wǎng)絡(luò)路由協(xié)議的安全性,本文主要對(duì)目前的這些形式化方法進(jìn)行研究,特別是針對(duì)基于模擬模型的方法和具有自動(dòng)化分析能力的形式化方法。論文工作主要圍繞國(guó)家自然科學(xué)基金重點(diǎn)項(xiàng)目(U1135002)的研究任務(wù)進(jìn)行展開,研究?jī)?nèi)容概括為如下幾個(gè)部分:首先研究了基于模擬模型的針對(duì)按需源路由協(xié)議分析的ABV模型。指出ABV模型實(shí)際上要分析的網(wǎng)絡(luò)環(huán)境允許存在多個(gè)惡意節(jié)點(diǎn),并且可以共謀,但是該模型中以不合理的理由將這些惡意節(jié)點(diǎn)合并,限制了惡意節(jié)點(diǎn)的攻擊能力,巧妙地回避了本來在ABV模型中要解決的關(guān)鍵問題。證明了endairA協(xié)議安全性證明過程中存在錯(cuò)誤,在ABV模型下可證明安全的路由協(xié)議不能保證可以抵御wormhole攻擊。指出了ABV模型回避了協(xié)議的鄰居發(fā)現(xiàn)過程,定義安全路由的目標(biāo)為發(fā)現(xiàn)plausible route,在實(shí)際網(wǎng)絡(luò)拓?fù)湎虏灰欢ㄊ谴嬖诘?且plausible route的定義回避了惡意節(jié)點(diǎn)可以表現(xiàn)成多個(gè)標(biāo)識(shí)的情況,證明了ABV模型中plausible route的定義減弱了模型的分析能力,在ABV模型下可證明安全的路由協(xié)議不能保證可以抵御Sybil攻擊。發(fā)現(xiàn)了一種針對(duì)endairA協(xié)議的隱蔽信道攻擊,該攻擊完全是在ABV模型的假設(shè)下進(jìn)行的,使得endairA協(xié)議接受非plausible route,從而說明該協(xié)議即使在ABV模型下也是不安全的,證明了ABV模型對(duì)隱蔽信道攻擊的分析并不完全,該模型下可證明安全的路由協(xié)議,仍然易受新的隱蔽信道攻擊,不能滿足其安全目標(biāo)。其次研究了基于模擬模型的針對(duì)按需距離矢量路由協(xié)議分析的擴(kuò)展ABV模型。證明了擴(kuò)展ABV模型敵手節(jié)點(diǎn)的合并減弱了模型的分析能力,在擴(kuò)展ABV模型下可證明安全的路由協(xié)議不能保證抵御wormhole攻擊;模型中正確系統(tǒng)狀態(tài)的定義減弱了模型的分析能力,在擴(kuò)展ABV模型下可證明安全的路由協(xié)議不能保證抵御Sybil攻擊;分析了擴(kuò)展ABV模型下ARAN協(xié)議安全性證明過程中的錯(cuò)誤,并給出一個(gè)攻擊實(shí)例,表明該模型下可證明安全的ARAN協(xié)議仍然存在安全漏洞。最后研究了基于模型檢測(cè)的按需源路由協(xié)議的形式化分析方法及其自動(dòng)化實(shí)現(xiàn)。使用SPIN工具自動(dòng)分析了SRP、Ariadne和endairA等協(xié)議,通過網(wǎng)絡(luò)拓?fù)浣：妥詣?dòng)生成,可以全面分析在不同網(wǎng)絡(luò)拓?fù)湎聟f(xié)議的安全性。通過自動(dòng)分析,發(fā)現(xiàn)了針對(duì)SRP、Ariadne和endairA協(xié)議的有效攻擊方法,表明了基于模型檢測(cè)及SPIN工具自動(dòng)分析安全路由協(xié)議的方法是有效的。
[Abstract]:The mobile ad hoc network has become a popular research field, and has a wide application in many aspects. Because of its own network characteristics, the mobile ad hoc network is vulnerable to various attacks, and the routing protocol is the most important basic function of the network, and is more likely to be the target of the attacker. In recent years, many mobile ad hoc network security routing protocols have been proposed, but the security of these protocols is mostly analyzed by non-formal methods such as direct observation or network simulation. At present, some scholars have tried to use the formal method to analyze the security of the routing protocol of the mobile ad hoc network. This paper mainly studies the present formal methods, in particular to the method based on the simulation model and the formal method with the capability of automatic analysis. The paper mainly focuses on the research task of the National Natural Science Foundation of China (U1135002), and the content of the research is summarized as follows: First, the ABV model for the on-demand source routing protocol analysis based on the simulation model is studied. it is pointed out that the abv model actually requires a plurality of malicious nodes to be analyzed in the network environment and can be conspired, but the malicious nodes are combined in an unreasonable way in the model, so that the attack capability of the malicious nodes is limited, The key problem to be solved in the ABV model is skillfully avoided. It is proved that there is an error in the security certification process of the endairA protocol, and under the ABV model, it is proved that the secure routing protocol can not be guaranteed to resist the world attack. It is pointed out that the ABV model avoids the neighbor discovery process of the protocol, defines the target of the security route as the discovery of the plausible route, does not necessarily exist under the actual network topology, It is proved that the definition of the plausible route in the ABV model has reduced the analytical capability of the model, and under the ABV model, it is proved that the secure routing protocol can not be guaranteed to resist the Sybil attack. A covert channel attack for the endairA protocol is found, which is carried out completely under the assumption of an ABV model, so that the endairA protocol accepts the non-plausible route, thus indicating that the protocol is not safe even under the ABV model, and it is proved that the analysis of the attack of the hidden channel by the ABV model is not complete, The model can prove that the secure routing protocol is still vulnerable to new covert channel attacks and cannot meet its security objectives. Secondly, the extended ABV model for the on-demand distance vector routing protocol analysis based on the simulation model is studied. It is proved that the combination of the extended ABV model and the enemy's hand node has reduced the analysis ability of the model, and under the extended ABV model, it is proved that the secure routing protocol cannot guarantee the resistance to the world attack; the definition of the correct system state in the model reduces the analytical capability of the model, In the extended ABV model, it is proved that the secure routing protocol is not guaranteed to resist the Sybil attack, and the error in the process of the security certification of the ARAN protocol under the extended ABV model is analyzed, and an attack case is given, which shows that the secure ARAN protocol still has a security hole under the model. At last, the formal analysis method and the automatic realization of the on-demand source routing protocol based on the model detection are studied. Using the SPIN tool, the protocols such as SRP, Ariadne and endairA are automatically analyzed, and the security of protocols under different network topologies can be comprehensively analyzed by network topology modeling and automatic generation. Through the automatic analysis, the effective attack method for SRP, Ariadne and endairA protocol is found, which shows that the method of automatic analysis of the secure routing protocol based on the model detection and the SPIN tool is effective.
【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2014
【分類號(hào)】：TN929.5
[Abstract]:The mobile ad hoc network has become a popular research field, and has a wide application in many aspects. Because of its own network characteristics, the mobile ad hoc network is vulnerable to various attacks, and the routing protocol is the most important basic function of the network, and is more likely to be the target of the attacker. In recent years, many mobile ad hoc network security routing protocols have been proposed, but the security of these protocols is mostly analyzed by non-formal methods such as direct observation or network simulation. At present, some scholars have tried to use the formal method to analyze the security of the routing protocol of the mobile ad hoc network. This paper mainly studies the present formal methods, in particular to the method based on the simulation model and the formal method with the capability of automatic analysis. The paper mainly focuses on the research task of the National Natural Science Foundation of China (U1135002), and the content of the research is summarized as follows: First, the ABV model for the on-demand source routing protocol analysis based on the simulation model is studied. it is pointed out that the abv model actually requires a plurality of malicious nodes to be analyzed in the network environment and can be conspired, but the malicious nodes are combined in an unreasonable way in the model, so that the attack capability of the malicious nodes is limited, The key problem to be solved in the ABV model is skillfully avoided. It is proved that there is an error in the security certification process of the endairA protocol, and under the ABV model, it is proved that the secure routing protocol can not be guaranteed to resist the world attack. It is pointed out that the ABV model avoids the neighbor discovery process of the protocol, defines the target of the security route as the discovery of the plausible route, does not necessarily exist under the actual network topology, It is proved that the definition of the plausible route in the ABV model has reduced the analytical capability of the model, and under the ABV model, it is proved that the secure routing protocol can not be guaranteed to resist the Sybil attack. A covert channel attack for the endairA protocol is found, which is carried out completely under the assumption of an ABV model, so that the endairA protocol accepts the non-plausible route, thus indicating that the protocol is not safe even under the ABV model, and it is proved that the analysis of the attack of the hidden channel by the ABV model is not complete, The model can prove that the secure routing protocol is still vulnerable to new covert channel attacks and cannot meet its security objectives. Secondly, the extended ABV model for the on-demand distance vector routing protocol analysis based on the simulation model is studied. It is proved that the combination of the extended ABV model and the enemy's hand node has reduced the analysis ability of the model, and under the extended ABV model, it is proved that the secure routing protocol cannot guarantee the resistance to the world attack; the definition of the correct system state in the model reduces the analytical capability of the model, In the extended ABV model, it is proved that the secure routing protocol is not guaranteed to resist the Sybil attack, and the error in the process of the security certification of the ARAN protocol under the extended ABV model is analyzed, and an attack case is given, which shows that the secure ARAN protocol still has a security hole under the model. At last, the formal analysis method and the automatic realization of the on-demand source routing protocol based on the model detection are studied. Using the SPIN tool, the protocols such as SRP, Ariadne and endairA are automatically analyzed, and the security of protocols under different network topologies can be comprehensively analyzed by network topology modeling and automatic generation. Through the automatic analysis, the effective attack method for SRP, Ariadne and endairA protocol is found, which shows that the method of automatic analysis of the secure routing protocol based on the model detection and the SPIN tool is effective.
【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2014
【分類號(hào)】：TN929.5
【相似文獻(xiàn)】
相關(guān)期刊論文 前10條
1 張君毅;楊義先;;針對(duì)安全路由協(xié)議的搶先重放攻擊研究[J];無線電工程;2008年09期
2 朱敏;;移動(dòng)Ad Hoc網(wǎng)絡(luò)的安全問題和解決方案[J];南通航運(yùn)職業(yè)技術(shù)學(xué)院學(xué)報(bào);2010年04期
3 繆成蓓;白光偉;顧躍躍;沈航;;SZM-LEACH:一種層簇式的WSN安全跨區(qū)多跳路由協(xié)議[J];微電子學(xué)與計(jì)算機(jī);2011年07期
4 劉洋;田波;;無線Ad Hoc環(huán)境下EIGRP的安全加固[J];信息安全與通信保密;2007年07期
5 宋志賢;喻繼q，
本文編號(hào)：2315441
本文鏈接：http://sikaile.net/kejilunwen/wltx/2315441.html
最近更新
教材專著
