基于重写逻辑的PKMv3协议形式化建模与验证  

FORMAL MODELING AND VERIFICATION OF PKMV3 PROTOCOL BASED ON REWRITING LOGIC

作　　者：佘葭 张民 

机构地区：[1]华东师范大学计算机科学与软件工程学院,上海200062

出　　处：《计算机应用与软件》2017年第11期270-277,共8页Computer Applications and Software

基　　金：国家自然科学基金青年基金项目(61502171)

摘　　要：IEEE802.16m标准在MAC安全子层定义了密钥管理PKMv3协议,用于认证和授权信息的传输以及密钥的交换。由于宽带无线网络具有易遭受攻击的特性,引入入侵者模型分析密钥管理协议的安全机制。利用一种基于重写逻辑的形式化建模语言Maude,实现对PKMv3网络环境中的通信主体以及系统状态的建模,并利用其自带的模型检测工具验证协议的安全特性。验证结果表明,PKMv3协议能保证密钥的机密性以及认证的可靠性,但仍有可能遭遇到中间人攻击破坏消息传输的完整性。IEEE802.16m standard defines PKMv3 （Privacy and Key management） protocol in MAC security sub- layer to realize the transmission of authentication information and exchange of secret key. Because of the vulnerability of broadband wireless network, intruder model is introduced to analyze the security mechanism of this key management protocol. Using a formal modeling language Maude which based on rewriting logic, we achieved the modeling of communication agent and system state in PKMv3 network environment. And Maude utilized formal verification tools to verify the security feature of this protocol. Verification result showed that PKMv3 protocol can guarantee the confidentiality of secret key and the reliability of authentication. However, it also showed that the protocol cannot prevent Man-in-the-Middle attack and the integrity of message transmission may be destroyed.

关 键 词：IEEE802. 16m 标准 PKMv3 协议 密钥管理 重写逻辑 MAUDE 语言 形式化验证 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]