摘要： 基于模型检测技术，使用SPIN 对IKEv2 协议进行了建模和分析。应用Promela 语言描述了协议模型，并用LTL 规约了该协议需要满足的认证性和秘密性，最后对检测结果进行了分析。
关键词:
IKE 协议；模型检测；SPIN；Promela
Abstract: 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
Key words:
IKE protocol; Model checking; SPIN; Promela
陈大伟，董荣胜，郭云川，古天龙. IKEv2 协议的SPIN 模型检测[J]. 计算机工程, 2006, 32(5): 164-166，246.
CHEN Dawei, DONG Rongsheng, GUO Yunchuan, GU Tianlong. Model Checking of IKEv2 Protocol via SPIN[J]. Computer Engineering, 2006, 32(5): 164-166，246.