基于SPIN的IKEv2协议高效模型检测

• 作者: 吴昌 肖美华
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: IKEv2 模型检测 SPIN Promela IP 隧道
• 年，卷（期）: 2008,（5）
• 所属期刊栏目: 网络、通信与安全
• 页码范围: 158-161
• 页数: 4页
• 分类号: TP393.08
• 字数: 3854字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2008.05.051

摘要

论文先简单介绍了互联网密钥交换协议IKEv2,然后利用著名的模型检测工具SPIN对其进行了建模和分析.在建模的过程中,作者发现现有的建模方法很难对结构复杂的协议IKEv2进行建模,而且用现有的建模方法建立的模型可读性差、自动化程度不高,验证效率也比较低,因此现有的建模方法只适用于对简单协议进行建模.针对这些不足之处,提出了一种程序可读性、自动化程度及验证效率均较好的建模方法,而且这种建模方法特别适合对复杂的安全协议进行建模.最后利用SPIN对IKEv2协议的模型进行了验证,发现IKEv2协议不能抵御主动攻击,并给出了两个攻击序列图.针对IKEv2协议不能保护发起者身份的缺陷,提出了自己的一种改进意见.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖美华	南昌大学信息工程学院	27	313	8.0	17.0
2	吴昌	南昌大学信息工程学院	2	18	2.0	2.0