互联网密钥交换协议的SMV分析  

Formal Analysis of the Internet Key Exchange Protocol Via SMV

作　　者：常亮[1] 古天龙[1] 郭云川[1] 

机构地区：[1]桂林电子工业学院计算机系,桂林541004

出　　处：《计算机工程与应用》2005年第19期154-157,173,共5页Computer Engineering and Applications

摘　　要：该文基于SMV对新版本的互联网密钥交换协议(IKEv2)进行了分析。在对IKEv2协议进行形式建模,以及应用CTL对相应的安全性质进行形式描述的基础上,利用SMV分析了协议的认证性、秘密性和完整性,发现了两个攻击,并对这两个攻击所产生的影响进行了讨论。In this paper,a formal model for the draft of Internet Key Exchange(IKEv2) Protocol is developed.Some desired properties of IKEv2 Protocol are specified using Computational Tree Logic(CTL).Through the symbolic modelchecker-SMV,the authentication,secrecy,and integrity of this protocol are analyzed,and two attacks are discovered.

关 键 词：IKE协议 模型检测 SMV 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]