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