无线体域网中的认证与密钥交换协议研究

发布时间：2018-02-16 11:45

本文关键词： 密钥管理安全协议无线体域网 BAN逻辑 AES　出处：《西安电子科技大学》2014年硕士论文　论文类型：学位论文

【摘要】：无线传感器网近年来取得了飞速发展,在军事、商业、医疗等方面发挥着巨大作用,与此同时无线传感器网在医疗方面的分支——无线体域网应运而生,无线体域网是指附着在人体上的一种网络,由若干个微型的具有通信功能的普通传感器和一个主传感器节点组成。无线体域网属于无线网络范畴,而无线网络的开放性、移动性和拓扑的动态性使其存在很多安全隐患,网络中信息交互过程易受到非法攻击,因此要采用相关的密码技术来保证其通信安全。安全协议是以密码技术为基础的消息交换协议,其目的是在网络环境中提供各种安全服务。通过安全协议可以进行实体之间的认证、在实体之间安全地分配密钥或其它各种秘密、确认收发消息的来源等。安全协议包括认证与密钥交换协议等,是网络安全的重要组成部分和理论保证。对认证与密钥交换协议的设计分析一直都是安全领域的研究热点,本文根据无线体域网特点设计了新的应用于该网络的认证与密钥交换协议,对新协议进行了形式化和非形式化分析证明,并在软件环境下进行了仿真测试。研究内容分为以下三方面:1.根据无线体域网标准给出的网络拓扑结构设计了分层的网络模型,并针对该模型提出了三种认证与密钥交换协议。网络中的每个普通节点分别和控制节点享有一对预共享密钥。三个协议采用了不同的认证发起方式:协议I是由二级节点发起认证,由控制节点选择一级认证节点并生成会话密钥;协议II则是在一级节点和二级节点协同的情况下由一级节点发起广播认证并生成会话密钥;协议III是由二级节点发起认证并生成会话密钥,一级节点充当中继,不做解密而是直接转发二级节点发送的信息。协议分别实现了在不同场景下无线体域网节点之间的选择认证,高效简洁地生成了不同级别节点之间的会话密钥。2.对安全协议的分析证明方法有形式化和非形式化两类,事实表明许多安全协议经过非形式化分析后仍然存在漏洞,有的甚至在应用了多年后才发现其漏洞,形式化分析方法则比较全面和有效。本文简述了形式化和非形式化分析方法,介绍了形式化分析方法中的BAN逻辑,重点采用BAN逻辑对三个无线体域网协议分别进行了分析,在给出BAN逻辑的初始化条件和证明规则情况下,利用逻辑推理规则推导出协议需要达到的最终信仰,结果表明协议安全有效,符合无线体域网安全要求。3.对协议的运行时间进行了测试。介绍了对称加密标准AES的加解密过程,给出了协议在使用AES算法的情况下,无线体域网认证与密钥交换协议的时间测试结果,本文采用C语言实现了仿真,在VS2010环境下分别测试了每个协议的运行时间,测试结果表明协议均有良好的执行效率。
[Abstract]:Wireless sensor network (WSN) has made rapid development in recent years and has played a great role in military, commercial, medical and so on. At the same time, the wireless body area network (WLAN), the branch of wireless sensor network (WSNs), has emerged as the times require. Wireless body area network (WLAN) is a kind of network attached to human body, which is composed of several miniature common sensors with communication function and one main sensor node. Wireless body area network belongs to the category of wireless network, and the wireless network is open. Because of the mobility and topology dynamics, there are many security risks, and the process of information exchange in the network is vulnerable to illegal attacks. Therefore, it is necessary to adopt the relevant cryptographic technology to ensure the security of its communication. The security protocol is a message exchange protocol based on cryptographic technology. The purpose is to provide a variety of security services in the network environment. Through security protocols, authentication between entities can be carried out, and keys or other secrets can be safely distributed among entities. The security protocols, including authentication and key exchange protocols, are important components and theoretical guarantees of network security. The design and analysis of authentication and key exchange protocols have always been the focus of research in the field of security. In this paper, a new authentication and key exchange protocol is designed according to the characteristics of the wireless body area network, and the formal and non-formal analysis of the new protocol is given. The research is divided into the following three aspects: 1. According to the wireless body area network standard, the hierarchical network model is designed. According to the model, three authentication and key exchange protocols are proposed. Each common node in the network and the control node have a pair of pre-shared keys respectively. The three protocols adopt different authentication initiation methods: protocol I is composed of. The secondary node initiates authentication, The first level authentication node is selected by the control node and the session key is generated. Protocol III is authenticated by the secondary node and generates the session key, and the primary node acts as the relay. Instead of decrypting, the protocol directly forwards the information sent by the secondary nodes. The protocol implements the selection authentication between the nodes of the wireless body area network in different scenarios. Efficient and concise generation of session keys between different levels of nodes. There are formal and non-formal methods to prove security protocols. The fact shows that many security protocols still exist vulnerabilities after non-formal analysis. Some even found the flaw after many years of application, but the formal analysis method is more comprehensive and effective. This paper briefly describes the formal and non-formal analysis methods, and introduces the BAN logic in the formal analysis method. Three wireless body area network protocols are analyzed with BAN logic. Under the condition of initializing BAN logic and proving rules, the final belief that the protocol needs to be achieved is deduced by using logic reasoning rules. The results show that the protocol is safe and effective and meets the security requirements of wireless body area network. The running time of the protocol is tested. The encryption and decryption process of symmetric encryption standard AES is introduced, and the protocol using AES algorithm is given. The time test results of wireless body area network authentication and key exchange protocol are simulated in C language. The running time of each protocol is tested in VS2010 environment. The test results show that the protocol has good execution efficiency.
【学位授予单位】：西安电子科技大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TN918.4

【参考文献】