本文關(guān)鍵詞：基于Maude的PKMv3協(xié)議形式化建模與驗證　出處：《華東師范大學(xué)》2017年碩士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： IEEE802.16m標(biāo)準(zhǔn) PKMv3協(xié)議 密鑰管理 重寫邏輯 Maude語言 形式化驗證

【摘要】：隨著科技的發(fā)展,人們對無線寬帶技術(shù)的需求日益增加。全球無線微波載入技術(shù) WiMAX(Worldwide Interoperability for Microwave Acess)是基于無線城域網(wǎng)絡(luò)的新技術(shù),實現(xiàn)了寬帶接入技術(shù)和移動服務(wù)的相互結(jié)合。IEEE802.16m標(biāo)準(zhǔn)是在IEEE802.16e基礎(chǔ)上的補(bǔ)充標(biāo)準(zhǔn),定義了新一代WiMAX技術(shù)規(guī)范。由于無線系統(tǒng)使用完全開放和未實施保護(hù)的無線通信信道,因此需要在無線通信技術(shù)中實施可信和強(qiáng)健的安全加密保護(hù)實現(xiàn)通信的機(jī)密性,隱私性和完整性。IEEE802.16m標(biāo)準(zhǔn)在MAC安全子層中定義了密鑰管理PKMv3協(xié)議,實現(xiàn)基站與手機(jī)端間的雙向認(rèn)證以及安全密鑰分發(fā)。在PKMv3協(xié)議中,基站作為服務(wù)端,手機(jī)站作為客戶端,雙方通過X.509數(shù)字證書實現(xiàn)身份驗證,建立授權(quán)密鑰,并通過安全組件協(xié)商,實現(xiàn)安全參數(shù)交換,最終通過密鑰材料的傳輸,生成傳輸密鑰以加密后續(xù)的通訊消息。PKMv3是改進(jìn)后的第三代密鑰管理協(xié)議,目前已有大量研究指出前兩代協(xié)議中出現(xiàn)較多安全漏洞,并且針對第三代協(xié)議的研究仍然不夠完善。因此,分析PKMv3協(xié)議的具體執(zhí)行流程以及驗證協(xié)議的安全特性十分關(guān)鍵。本文對安全協(xié)議的研究采用形式化建模的方式。安全協(xié)議的形式化方法采用數(shù)學(xué)模型,實現(xiàn)對協(xié)議結(jié)構(gòu)以及通信過程的模擬,并通過有效的程序分析驗證系統(tǒng)所滿足的性質(zhì)條件。Maude是基于重寫邏輯的形式化建模語言,它定義了簡潔且無二義性的語法,并且提供多種檢測方法,適合作為編程語言,算法的分析工具以及系統(tǒng)建模工具。本文通過Maude定義的可執(zhí)行形式化規(guī)范,實現(xiàn)對PKMv3協(xié)議中各執(zhí)行階段的建模。不同于現(xiàn)有的研究工作,本文考慮到協(xié)議執(zhí)行過程中密鑰的周期性質(zhì),在協(xié)議模型中加入時間機(jī)制模擬密鑰重認(rèn)證的過程,同時引入攻擊者模型,模擬入侵者在網(wǎng)絡(luò)中竊取,重放以及偽造消息的過程�；诰帉懲瓿傻腜KMv3協(xié)議可執(zhí)行規(guī)范,本文通過LTL模型檢測工具實現(xiàn)對協(xié)議連續(xù)性,密鑰活性,認(rèn)證密鑰以及傳輸密鑰生命周期等時間相關(guān)性質(zhì)的檢測;并通過窮盡空間狀態(tài)查找指令實現(xiàn)對協(xié)議中機(jī)密性,認(rèn)證性,完整性以及可用性等安全性質(zhì)的驗證。驗證結(jié)果表明,PKMv3協(xié)議模型能夠滿足協(xié)議標(biāo)準(zhǔn)中的各項時間特性,但可能會遭遇到入侵者攻擊,從而無法保證協(xié)議的完整性以及可用性。針對協(xié)議中的安全漏洞,本文在協(xié)議各階段提出相應(yīng)的解決方案,進(jìn)而重新改寫協(xié)議模型,證明改進(jìn)后協(xié)議所滿足的安全特性。
[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.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：TN918

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 卿斯?jié)h;安全協(xié)議20年研究進(jìn)展[J];軟件學(xué)報;2003年10期

2 鄧帆;鄧少鋒;張文政;;安全協(xié)議的規(guī)范化設(shè)計[J];計算機(jī)工程與應(yīng)用;2011年18期

3 來學(xué)嘉;基于挑戰(zhàn)-響應(yīng)的認(rèn)證協(xié)議安全的必要條件(英文)[J];中國科學(xué)院研究生院學(xué)報;2002年03期

4 李莉;張煥國;王張宜;;一種安全協(xié)議的形式化設(shè)計方法[J];計算機(jī)工程與應(yīng)用;2006年11期

5 趙軍;;移動IPv6協(xié)議安全機(jī)制優(yōu)化[J];淮陰工學(xué)院學(xué)報;2008年01期

6 陶志紅,Hans KleineBu，

本文編號：1418148