论文部分内容阅读
IEEE802.16m标准在MAC安全子层定义了密钥管理PKMv3协议,用于认证和授权信息的传输以及密钥的交换。由于宽带无线网络具有易遭受攻击的特性,引入入侵者模型分析密钥管理协议的安全机制。利用一种基于重写逻辑的形式化建模语言Maude,实现对PKMv3网络环境中的通信主体以及系统状态的建模,并利用其自带的模型检测工具验证协议的安全特性。验证结果表明,PKMv3协议能保证密钥的机密性以及认证的可靠性,但仍有可能遭遇到中间人攻击破坏消息传输的完整性。