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

计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (5): 158-161.

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

吴昌,肖美华

南昌大学信息工程学院，南昌 330031

收稿日期:2007-06-05 修回日期:2007-08-20 出版日期:2008-02-11 发布日期:2008-02-11
通讯作者: 吴昌

Effective model checking of IKEv2 protocol based on SPIN

WU Chang,XIAO Mei-hua

College of Computer Information and Engineering，Nanchang University，Nanchang 330031，China

Received:2007-06-05 Revised:2007-08-20 Online:2008-02-11 Published:2008-02-11
Contact: WU Chang

摘要/Abstract

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

关键词: IKEv2, 模型检测, SPIN, Promela, IP隧道

Abstract: This paper first gives a simple introduction of the Internet Key Exchange Protocol IKEv2，then conducts a modeling and analysis of the protocol by using the famous model checking tool SPIN.The author finds the existing modeling method hardly applicable because of the highly complex structure of IKEv2 protocol，and that it can only be used for some simple protocols due to its poor readability，low automatization and verification efficiency.Thus the paper proposes another method of modeling which overcomes all the above mentioned disadvantages and which is particularly useful for complicated protocols.At last，the verification of the IKEv2 protocol model based on SPIN shows that this protocol is incapable of resisting initiative attack.Based on this discovery，two charts are given describing the attack and a personal view is presented to improve IKEv2 protocol’s ability to protect the identity of initiator.

Key words: IKEv2, model checking, SPIN, Promela, IP Tunnel

吴昌,肖美华. 基于SPIN的IKEv2协议高效模型检测[J]. 计算机工程与应用, 2008, 44(5): 158-161.

WU Chang,XIAO Mei-hua. Effective model checking of IKEv2 protocol based on SPIN[J]. Computer Engineering and Applications, 2008, 44(5): 158-161.

[1]	杜梦瑶，王峥，李娜，强彦. 适用于无线体域网的动态口令认证协议[J]. 计算机工程与应用, 2020, 56(14): 68-73.
[2]	杨文霞，王峥，李娜，马建芬. 轻量级移动支付协议LMPP的安全性分析与改进[J]. 计算机工程与应用, 2019, 55(16): 88-93.
[3]	李茜1，王峥1，马建芬1，李娜2. 轻量级移动支付协议公平性分析[J]. 计算机工程与应用, 2018, 54(19): 82-87.
[4]	李前利，江华. 命题μ-演算局部模型检测高效算法设计[J]. 计算机工程与应用, 2017, 53(9): 51-56.
[5]	秦嫚蔓，王峥，王莉. 基于SPIN的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.
[6]	吕江华1，刘志锋1，徐亚涛2，周从华1. 基于属性的访问控制策略的正确性验证[J]. 计算机工程与应用, 2016, 52(18): 98-103.
[7]	夏春蕊1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 动态环境下基于概率模型检测的路径规划方法[J]. 计算机工程与应用, 2016, 52(12): 5-11.
[8]	黄延凯，周宇，魏欧. 新型属性图文法反应式规约验证方法[J]. 计算机工程与应用, 2016, 52(12): 15-18.
[9]	王铭1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 非确定性环境中移动机器人避障策略的验证 ——基于形式化建模和概率分析[J]. 计算机工程与应用, 2016, 52(10): 31-38.
[10]	张舒青，徐中伟，陈祖希. 基于项重写系统的联锁系统模型检测方法研究[J]. 计算机工程与应用, 2014, 50(3): 49-54.
[11]	王昌达1，2，董雪刚1，周从华1，2. 基于UCON的网络银行在线支付及其安全性分析[J]. 计算机工程与应用, 2014, 50(16): 90-94.
[12]	佟超，王建新，齐建东. 基于形式化规约的缺陷规则库构建与检测方法[J]. 计算机工程与应用, 2014, 50(13): 66-72.
[13]	尤启房，杨晋吉. SIP协议的SPIN模型检测[J]. 计算机工程与应用, 2014, 50(13): 87-89.
[14]	吕威，黄志球，陈哲，阚双龙，魏欧. ESpin*：基于SPIN的Eclipse模型检测环境[J]. 计算机工程与应用, 2013, 49(7): 45-51.
[15]	陈娟娟，魏欧，黄志球，陈哲. 基于双格的多值模型的精化关系与对称化简[J]. 计算机工程与应用, 2013, 49(22): 40-45.