IKEv2协议的SPIN模型检测  

Model Checking of IKEv2 Protocol via SPIN

作　　者：陈大伟[1] 董荣胜[1] 郭云川[1] 古天龙[1] 

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

出　　处：《计算机工程》2006年第5期164-166,246,共4页Computer Engineering

基　　金：广西省自然科学基金资助项目(0542052)

摘　　要：基于模型检测技术,使用SPIN对IKEv2协议进行了建模和分析。应用Promela语言描述了协议模型,并用LTL规约了该协议需要满足的认证性和秘密性,最后对检测结果进行了分析。As one of the model checking tools, SPIN is applied to model and evaluate the IKEv2 protocol, where the Promela model is developed, and LTL （linear temporal logic） specifications of authentication and secrecy are given. The result shows that the tool works well.

关 键 词：IKE协议 模型检测 SPIN PROMELA 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]