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

• 作者: 佘葭 张民
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: IEEE802.16m标准 PKMv3协议 密钥管理 重写逻辑 Maude语言 形式化验证
• 年，卷（期）: 2017,（11）
• 所属期刊栏目: 安全技术
• 页码范围: 270-277
• 页数: 8页
• 分类号: TP311.5
• 字数: 7545字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2017.11.050

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	佘葭	华东师范大学计算机科学与软件工程学院	1	0	0.0	0.0
2	张民	华东师范大学计算机科学与软件工程学院	1	0	0.0	0.0