基于Maude的PKMv3协议形式化建模与验证

发布时间：2018-01-13 08:05

本文关键词：基于Maude的PKMv3协议形式化建模与验证　出处：《华东师范大学》2017年硕士论文　论文类型：学位论文

【摘要】：随着科技的发展,人们对无线宽带技术的需求日益增加。全球无线微波载入技术 WiMAX(Worldwide Interoperability for Microwave Acess)是基于无线城域网络的新技术,实现了宽带接入技术和移动服务的相互结合。IEEE802.16m标准是在IEEE802.16e基础上的补充标准,定义了新一代WiMAX技术规范。由于无线系统使用完全开放和未实施保护的无线通信信道,因此需要在无线通信技术中实施可信和强健的安全加密保护实现通信的机密性,隐私性和完整性。IEEE802.16m标准在MAC安全子层中定义了密钥管理PKMv3协议,实现基站与手机端间的双向认证以及安全密钥分发。在PKMv3协议中,基站作为服务端,手机站作为客户端,双方通过X.509数字证书实现身份验证,建立授权密钥,并通过安全组件协商,实现安全参数交换,最终通过密钥材料的传输,生成传输密钥以加密后续的通讯消息。PKMv3是改进后的第三代密钥管理协议,目前已有大量研究指出前两代协议中出现较多安全漏洞,并且针对第三代协议的研究仍然不够完善。因此,分析PKMv3协议的具体执行流程以及验证协议的安全特性十分关键。本文对安全协议的研究采用形式化建模的方式。安全协议的形式化方法采用数学模型,实现对协议结构以及通信过程的模拟,并通过有效的程序分析验证系统所满足的性质条件。Maude是基于重写逻辑的形式化建模语言,它定义了简洁且无二义性的语法,并且提供多种检测方法,适合作为编程语言,算法的分析工具以及系统建模工具。本文通过Maude定义的可执行形式化规范,实现对PKMv3协议中各执行阶段的建模。不同于现有的研究工作,本文考虑到协议执行过程中密钥的周期性质,在协议模型中加入时间机制模拟密钥重认证的过程,同时引入攻击者模型,模拟入侵者在网络中窃取,重放以及伪造消息的过程。基于编写完成的PKMv3协议可执行规范,本文通过LTL模型检测工具实现对协议连续性,密钥活性,认证密钥以及传输密钥生命周期等时间相关性质的检测;并通过穷尽空间状态查找指令实现对协议中机密性,认证性,完整性以及可用性等安全性质的验证。验证结果表明,PKMv3协议模型能够满足协议标准中的各项时间特性,但可能会遭遇到入侵者攻击,从而无法保证协议的完整性以及可用性。针对协议中的安全漏洞,本文在协议各阶段提出相应的解决方案,进而重新改写协议模型,证明改进后协议所满足的安全特性。
[Abstract]:With the development of science and technology. The demand for wireless broadband technology is increasing. Global Wireless Microwave loading Technology WiMAX. Worldwide Interoperability for Microwave Acess is a new technology based on wireless metropolitan area network. Realizing the combination of broadband access technology and mobile service. IEEE 802.16m standard is a supplementary standard based on IEEE802.16e. A new generation of WiMAX technical specifications is defined. Due to the use of fully open and unprotected wireless communication channels in wireless systems. Therefore, it is necessary to implement trusted and robust secure encryption in wireless communication technology to realize the confidentiality of communication. The privacy and integrity. IEEE 802.16m standard defines the key management PKMv3 protocol in the MAC security sublayer. In the PKMv3 protocol, the base station serves as the server, the mobile phone station as the client, and both sides implement authentication through X. 509 digital certificate. The authorization key is established, and the security parameters are exchanged through the negotiation of the security components. Finally, the key material is transmitted. Generation of transmission keys to encrypt subsequent communication messages .PKMv3 is an improved third-generation key management protocol. At present, a large number of studies have pointed out that there are many security vulnerabilities in the previous two protocols. And the third generation protocol research is still not perfect. It is very important to analyze the implementation process of PKMv3 protocol and the security characteristics of verification protocol. In this paper, the formal modeling method is adopted for the research of security protocol and the mathematical model is used for the formal method of security protocol. The simulation of protocol structure and communication process is realized, and the property condition that the system meets is verified by effective program analysis. Maude is a formal modeling language based on rewriting logic. It defines concise and non-ambiguous syntax, and provides a variety of detection methods, suitable for programming language. Algorithm analysis tools and system modeling tools. This paper uses the executable formal specification defined by Maude to model the execution stages of PKMv3 protocol. It is different from the existing research work. In this paper, considering the periodic nature of key during protocol execution, we add a time mechanism to the protocol model to simulate the process of key reauthentication. At the same time, we introduce an attacker model to simulate the intruders stealing in the network. Based on the completed PKMv3 protocol executable specification, this paper implements the protocol continuity and key activity through the LTL model checking tool. The detection of time related properties such as authentication key and transmission key life cycle; The security properties of the protocol such as confidentiality, authentication, integrity and availability are verified by exhaustive spatial state lookup instructions. The verification results show that. The PKMv3 protocol model can satisfy the time characteristics of the protocol standard, but it may be attacked by intruders, which can not guarantee the integrity and availability of the protocol. In this paper, the corresponding solutions are proposed in each phase of the protocol, and then the protocol model is rewritten to prove the security characteristics of the improved protocol.
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TN918

【相似文献】