基于重写逻辑的PKMv3协议形式化建模与验证-计算机应用与软件.PDFVIP

第３４卷第１１期　　　 计算机应用与软件 Ｖｏｌ３４Ｎｏ．１１ ２０１７年１１月　　 ＣｏｍｐｕｔｅｒＡｐｐｌｉｃａｔｉｏｎｓａｎｄＳｏｆｔｗａｒｅ Ｎｏｖ．２０１７ 基于重写逻辑的ＰＫＭｖ３协议形式化建模与验证 佘　葭　张　民 （华东师范大学计算机科学与软件工程学院　上海２０００６２） 摘　要　　ＩＥＥＥ８０２．１６ｍ标准在ＭＡＣ安全子层定义了密钥管理ＰＫＭｖ３协议，用于认证和授权信息的传输以及 密钥的交换。由于宽带无线网络具有易遭受攻击的特性，引入入侵者模型分析密钥管理协议的安全机制。利用 一种基于重写逻辑的形式化建模语言Ｍａｕｄｅ，实现对ＰＫＭｖ３网络环境中的通信主体以及系统状态的建模，并利 用其自带的模型检测工具验证协议的安全特性。验证结果表明，ＰＫＭｖ３协议能保证密钥的机密性以及认证的可 靠性，但仍有可能遭遇到中间人攻击破坏消息传输的完整性。 关键词　　ＩＥＥＥ８０２．１６ｍ标准　ＰＫＭｖ３协议　密钥管理　重写逻辑　Ｍａｕｄｅ语言　形式化验证 中图分类号　ＴＰ３１１．５　　　　文献标识码　Ａ　　　　ＤＯＩ：１０．３９６９／ｊ．ｉｓｓｎ．１０００３８６ｘ．２０１７．１１．０５０ ＦＯＲＭＡＬＭＯＤＥＬＩＮＧＡＮＤＶＥＲＩＦＩＣＡＴＩＯＮＯＦＰＫＭＶ３ＰＲＯＴＯＣＯＬ ＢＡＳＥＤＯＮＲＥＷＲＩＴＩＮＧＬＯＧＩＣ ＳｈｅＪｉａ　ＺｈａｎｇＭｉｎ （ＩｎｓｔｉｔｕｔｅｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＳｏｆｔｗａｒｅＥｎｇｉｎｅｅｒｉｎｇ，ＥａｓｔＣｈｉｎａＮｏｒｍａｌＵｎｉｖｅｒｓｉｔｙ，Ｓｈａｎｇｈａｉ２０００６２，Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ　　ＩＥＥＥ８０２．１６ｍｓｔａｎｄａｒｄｄｅｆｉｎｅｓＰＫＭｖ３（ＰｒｉｖａｃｙａｎｄＫｅｙｍａｎａｇｅｍｅｎｔ）ｐｒｏｔｏｃｏｌｉｎＭＡＣｓｅｃｕｒｉｔｙｓｕｂ ｌａｙｅｒｔｏｒｅａｌｉｚｅｔｈｅｔｒａｎｓｍｉｓｓｉｏｎｏｆａｕｔｈｅｎｔｉｃａｔｉｏｎｉｎｆｏｒｍａｔｉｏｎａｎｄｅｘｃｈａｎｇｅｏｆｓｅｃｒｅｔｋｅｙ．Ｂｅｃａｕｓｅｏｆｔｈｅｖｕｌｎｅｒａｂｉｌｉｔｙｏｆ ｂｒｏａｄｂａｎｄｗｉｒｅｌｅｓｓｎｅｔｗｏｒｋ，ｉｎｔｒｕｄｅｒｍｏｄｅｌｉｓｉｎｔｒｏｄｕｃｅｄｔｏａｎａｌｙｚｅｔｈｅｓｅｃｕｒｉｔｙｍｅｃｈａｎｉｓｍｏｆｔｈｉｓｋｅｙｍａｎａｇｅｍｅｎｔ ｐｒｏｔｏｃｏｌ．ＵｓｉｎｇａｆｏｒｍａｌｍｏｄｅｌｉｎｇｌａｎｇｕａｇｅＭａｕｄｅｗｈｉｃｈｂａｓｅｄｏｎｒｅｗｒｉｔｉｎｇｌｏｇｉｃ，ｗｅａｃｈｉｅｖｅｄｔｈｅｍｏｄｅｌｉｎｇｏｆ ｃｏｍｍｕｎｉｃａｔｉｏｎａｇｅｎｔａｎｄｓｙｓｔｅｍｓｔａｔｅｉｎＰＫＭｖ３ｎｅｔｗｏｒｋｅｎｖｉｒｏｎｍｅｎｔ．ＡｎｄＭａｕｄｅｕｔｉｌｉｚｅｄｆｏｒｍａｌｖｅｒｉｆｉｃａｔｉｏｎｔｏｏｌｓｔｏ ｖｅｒｉｆｙｔｈｅｓｅｃｕｒｉｔｙｆｅａｔｕｒｅｏｆｔｈｉｓｐｒｏｔｏｃｏｌ．ＶｅｒｉｆｉｃａｔｉｏｎｒｅｓｕｌｔｓｈｏｗｅｄｔｈａｔＰＫＭｖ３ｐｒｏｔｏｃｏｌｃａｎｇｕａｒａｎｔｅｅｔｈｅ ｃｏｎｆｉｄｅｎｔｉａｌｉｔｙｏｆｓｅｃｒｅｔｋｅｙａｎｄｔｈｅｒｅｌｉａｂｉｌｉｔｙｏｆａｕｔｈｅｎｔｉｃａｔｉｏｎ．Ｈｏｗｅｖｅｒ，ｉｔａｌｓｏｓｈｏｗｅｄｔｈａｔｔｈｅｐｒｏｔｏｃｏｌｃａｎｎｏｔｐｒｅｖｅｎｔ ＭａｎｉｎｔｈｅＭｉｄｄｌｅａｔｔａｃｋａｎｄｔｈｅｉｎｔｅｇｒｉｔｙｏｆｍｅｓｓａｇｅｔｒａｎｓｍｉｓｓｉｏｎｍａｙｂｅｄｅｓｔｒｏｙｅｄ． Ｋｅｙｗｏｒｄｓ　　ＩＥＥＥ８０２．１６ｍｓｔａｎｄａｒｄ　ＰＫＭｖ３ｐｒｏｔｏｃｏｌ　Ｋｅｙｍａｎａｇｅｍｅｎｔ　Ｒｅｗｒｉｔｉｎｇｌｏｇｉｃ　Ｍａｕｄｅｌａｎｇｕａｇｅ　Ｆｏｒ ｍａｌｖｅｒｉｆｉｃａｔｉｏｎ 行改进［３］，增加对消息的分级保护，采用更安全的ＡＥＳ ０　引　言 加密算法，并支持基于 ＥＡＰ（ＥｘｔｅｎｓｉｂｌｅＡｕｔｈｅｎｔｉｃａｔｉｏｎ