佘 葭 张 民

(华东师范大学计算机科学与软件工程学院 上海 200062)

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

佘 葭 张 民

(华东师范大学计算机科学与软件工程学院 上海 200062)

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

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

0 引 言

IEEE802.16m[1]是全球微波互联技术WiMAX[2]的新一代标准。WiMAX是一种支持无线数据长距离高速传输的电子通信技术，正逐步实现宽带业务的移动化。IEEE802.16m在MAC安全子层中定义了WiMAX的安全规范，其中包括对数据包进行加密的封装协议和提供密钥分发和安全访问控制的PKMv3协议。PKMv3协议在前两代密钥管理协议的基础上进行改进[3]，增加对消息的分级保护，采用更安全的AES加密算法，并支持基于EAP (Extensible Authentication Protocol)的认证方式和CMAC(Cipher-based Message Authentication)消息验证，减少了遭受攻击的可能性。

由于移动WiMAX网络比传统无线网络面临更多的威胁，针对密钥管理PKM协议安全性已有学者做了大量的研究工作。文献[4]利用BAN逻辑实现了对前两代密钥管理协议的分析，指出PKMv1协议中单向认证的缺陷和PKMv2协议中遭遇到的穿插攻击。……