移动ad hoc网络安全路由协议分析方法研究
发布时间：2018-11-06 20:52
【摘要】：移动ad hoc网络已经成为一个热门的研究领域,在很多方面都有着广泛的应用。由于其自身网络特点,移动ad hoc网络容易受到各种攻击,路由协议作为网络最重要的基本功能,更容易成为攻击者的目标。近年来,学者们已经提出多个移动ad hoc网络安全路由协议,但是这些协议的安全性大多通过直接观察或者网络仿真等非形式化方法进行分析,所以,很多安全路由协议后来都被发现存在安全漏洞。目前已经有学者开始尝试使用形式化方法分析移动ad hoc网络路由协议的安全性,本文主要对目前的这些形式化方法进行研究,特别是针对基于模拟模型的方法和具有自动化分析能力的形式化方法。论文工作主要围绕国家自然科学基金重点项目(U1135002)的研究任务进行展开,研究内容概括为如下几个部分:首先研究了基于模拟模型的针对按需源路由协议分析的ABV模型。指出ABV模型实际上要分析的网络环境允许存在多个恶意节点,并且可以共谋,但是该模型中以不合理的理由将这些恶意节点合并,限制了恶意节点的攻击能力,巧妙地回避了本来在ABV模型中要解决的关键问题。证明了endairA协议安全性证明过程中存在错误,在ABV模型下可证明安全的路由协议不能保证可以抵御wormhole攻击。指出了ABV模型回避了协议的邻居发现过程,定义安全路由的目标为发现plausible route,在实际网络拓扑下不一定是存在的,且plausible route的定义回避了恶意节点可以表现成多个标识的情况,证明了ABV模型中plausible route的定义减弱了模型的分析能力,在ABV模型下可证明安全的路由协议不能保证可以抵御Sybil攻击。发现了一种针对endairA协议的隐蔽信道攻击,该攻击完全是在ABV模型的假设下进行的,使得endairA协议接受非plausible route,从而说明该协议即使在ABV模型下也是不安全的,证明了ABV模型对隐蔽信道攻击的分析并不完全,该模型下可证明安全的路由协议,仍然易受新的隐蔽信道攻击,不能满足其安全目标。其次研究了基于模拟模型的针对按需距离矢量路由协议分析的扩展ABV模型。证明了扩展ABV模型敌手节点的合并减弱了模型的分析能力,在扩展ABV模型下可证明安全的路由协议不能保证抵御wormhole攻击;模型中正确系统状态的定义减弱了模型的分析能力,在扩展ABV模型下可证明安全的路由协议不能保证抵御Sybil攻击;分析了扩展ABV模型下ARAN协议安全性证明过程中的错误,并给出一个攻击实例,表明该模型下可证明安全的ARAN协议仍然存在安全漏洞。最后研究了基于模型检测的按需源路由协议的形式化分析方法及其自动化实现。使用SPIN工具自动分析了SRP、Ariadne和endairA等协议,通过网络拓扑建模和自动生成,可以全面分析在不同网络拓扑下协议的安全性。通过自动分析,发现了针对SRP、Ariadne和endairA协议的有效攻击方法,表明了基于模型检测及SPIN工具自动分析安全路由协议的方法是有效的。
[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.
【学位授予单位】：西安电子科技大学
【学位级别】：博士
【学位授予年份】：2014
【分类号】：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.
【学位授予单位】：西安电子科技大学
【学位级别】：博士
【学位授予年份】：2014
【分类号】：TN929.5
【相似文献】
相关期刊论文 前10条
1 张君毅;杨义先;;针对安全路由协议的抢先重放攻击研究[J];无线电工程;2008年09期
2 朱敏;;移动Ad Hoc网络的安全问题和解决方案[J];南通航运职业技术学院学报;2010年04期
3 缪成蓓;白光伟;顾跃跃;沈航;;SZM-LEACH:一种层簇式的WSN安全跨区多跳路由协议[J];微电子学与计算机;2011年07期
4 刘洋;田波;;无线Ad Hoc环境下EIGRP的安全加固[J];信息安全与通信保密;2007年07期
5 宋志贤;喻继q，
本文编号：2315441
本文链接：https://www.wllwen.com/kejilunwen/wltx/2315441.html
