节点文献
无线网络协议的形式化分析与设计
Formal Analysis and Design of Wireless Network Protocols
【作者】 杨超;
【导师】 马建峰;
【作者基本信息】 西安电子科技大学 , 密码学, 2008, 博士
【摘要】 随着信息技术和网络技术的飞速发展,信息网络的广泛应用已成为社会进步和发展的重要标志之一。传统有线网络由于受环境条件的制约,在物理、逻辑和成本方面普遍存在着一系列问题,发展可行的无线通信网络技术作为现有网络的扩充已成为数据网络发展的重要方向。而解决数据安全的安全协议和解决路径选择的路由协议则是构建无线网络体系结构的两大基石,具有非常重要研究意义。本论文分别对可证明安全的认证及密钥交换安全协议和无线Mesh网络路由协议的分析与设计进行了比较深入的研究,研究内容包括:安全协议形式化分析与设计理论的研究;Internet密钥交换协议的分析与设计;无线Mesh网络的双向认证和漫游接入协议的分析与设计以及无线Mesh网络混合路由协议的设计、仿真分析与性能比较。主要研究成果有:1.介绍了CK安全模型和UC安全模型的基本概念、安全理论和形式化方法,分析了这些安全模型的安全属性,归纳总结了可证明安全模型下安全协议设计的一般性方法和步骤。2.对Internet密钥交换协议IKEv2进行了安全分析,并针对其存在的认证失败和发起者主动身份保护问题提出了改进方案。新的方案通过对通信对方的身份进行签名来实现有效的身份认证,同时还能够保证通信双方对交互消息内容的不可否认性,实现对协议发起者的主动身份保护。3.针对IEEE 802.11s规范的接入认证协议不支持双向的802.1X认证端口开放,基于“通用可组合”的安全模型与DH交换,利用组合与信任传递技术设计了一种新的接入认证协议,实现了申请者S和认证服务器AS之间的双向认证。针对Mesh节点漫游接入的特殊安全需求,提出了一种新的无线Mesh网漫游接入认证协议,可以较好的支持Mesh网络的漫游场景,满足接入的安全需求,并能为移动用户提供身份保护。4.针对无线Mesh网络路由协议存在的一些诸如效率较低,扩展性不强等问题,提出了一种新的Mesh网络多径路由协议。新协议结合了分布式路由与集中式路由的优点,将数据链路层的平面路由方法拉伸成类似于IP路由的多级路由框架,提高了协议的执行效率,增强了Mesh网络的可扩展性和可用性。仿真分析表明,新协议在多个性能参数上优于原有协议。
【Abstract】 With the rapid growth of information and network technologies, information networks have been an important mark of development and advancement of the modern society. But there exist some common problems in physics, logic and cost of the traditional networks for the restriction of environmental conditions. So, developing the feasible Wireless Communication network technologies to extend the current networks have become the important study direction of data networks. However, wireless networks face great challenges in security and path selection. So, security protocols and routing protocols are the base of constructing the architecture of wireless networks and have very important research significance.This work makes a comparative deep research on the provably secure authentication and key exchange protocols, and wireless mesh network routing protocols, including provably secure theories for authentication and key exchange, authentication protocols in the Internet, authentication and key exchange protocols for access and roaming in wireless mesh networks, and hybrid wireless mesh routing protocols. The main results are as following:1. we introduce the basic concept, secure theories and formalization method of the Canetti-Krawczyk (CK) and Universally Composable(UC) security model. Based on systematic analyzing the secure attributes of these security models, we summarize the general methods and steps for analysis and design of security protocols in the provably security models.2. The security of the new Internet Key Exchange Protocol (IKEv2) is analyzed. The result shows that IKEv2 has some problems of authentication failure and initiator’s identity exposure, so improvements are given. By using“alias”and involving the peer’s identity in signature, the new protocol can realize the efficient authentication and active identity protection to the initiator. Moreover, the non-repudiation of the peers for their interactions is also achieved.3. The authentication protocol of Wireless Mesh Networks does not support the 802.1X-based mutual authentications. To solving this problem, a new authentication protocol is proposed, which is based on the basic idea of DH exchange, the technology of trust transfer and the combination characteristic of UC security model. The new protocol provides mutual authentication for Wireless Mesh Networks and it is provably secure with the UC model. According to the special security demand of wireless mesh networks, a new roaming authentication protocol that satisfies the UC-security is proposed. Such protocol guarantees the confidentiality of user’s identity and works well in the roaming environment of mesh networks.4. Low efficiency and poor expansibility are the essential problems of routing protocol in wireless mesh networks. On the basis of the distributed and centralized routing protocol, a new protocol WMRP (Wireless Mesh Route Protocol) is proposed. Such protocol extends the flat routing mechanism to the class routing architecture which is similar to the IP routing and improves the efficiency and expansibility of routing protocol greatly. Through the network simulation and performance evaluation, the result shows that the new routing protocol has advantages in performance over the existing protocol.
【Key words】 Provable Security; Formal Analysis; Cryptography Protocol; Mesh Roating Protocol; Network Simulation;