计算机应用与软件2017，Vol.34Issue(11)：270-277,8.DOI:10.3969/j.issn.1000-386x.2017.11.050
基于重写逻辑的PKMv3协议形式化建模与验证
FORMAL MODELING AND VERIFICATION OF PKMV3 PROTOCOL BASED ON REWRITING LOGIC
摘要
Abstract
IEEE802.16m standard defines PKMv3 (Privacy and Key management) protocol in MAC security sublayer 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语言/形式化验证Key words
IEEE 802.16m standard/PKMv3 protocol/Key management/Rewriting logic/Maude language/Formal verification分类
信息技术与安全科学引用本文复制引用
佘葭,张民..基于重写逻辑的PKMv3协议形式化建模与验证[J].计算机应用与软件,2017,34(11):270-277,8.基金项目
国家自然科学基金青年基金项目(61502171). （61502171）
