节点文献

IKEv2协议的SPIN模型检测

Model Checking of IKEv2 Protocol via SPIN

推荐 CAJ下载
PDF下载
不支持迅雷等下载工具，请取消加速工具后下载。

【Author】 CHEN Dawei,DONG Rongsheng,GUO Yunchuan,GU Tianlong(Computer Department,Guilin University of Electronic Technology,Guilin 541004)

【机构】桂林电子工业学院计算机系；桂林电子工业学院计算机系桂林541004；桂林541004；

【摘要】基于模型检测技术,使用SPIN对IKEv2协议进行了建模和分析。应用Promela语言描述了协议模型,并用LTL规约了该协议需要满足的认证性和秘密性,最后对检测结果进行了分析。更多还原

【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.更多还原

【关键词】 IKE协议；模型检测； SPIN； Promela；
【Key words】 IKE protocol； Model checking； SPIN； Promela；

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

【文献出处】计算机工程 ,Computer Engineering , 编辑部邮箱 ,2006年05期

【分类号】TP311.52
【被引频次】20
【下载频次】209

知网节下载

节点文献中：

本文链接的文献网络图示:

本文的引文网络

节点文献