基于符号模型检测的安全协议验证

摘要：

　　模型检测技术在安全协议验证领域取得了很大成果，但是存在状态空间爆炸问题。已经提出的小系统理论从理论上有效地解决了这个问题。使用符号模型检测工具SMV对NSPK协议进行了建模，对其安全性质进行了断言语言CTL描述并提交系统运行，发现了其已知的安全漏洞，证明了此种方法的有效性。

关键词： 安全协议 符号模型检测 安全漏洞 小系统理论

作者: 王政 郑君杰

作者单位: 总参大气环境研究所,北京,中国, 100001 解放军理工大学气象学院，南京，中国,2111101

会议类型: 国内会议

会议名称: 2011年青年通信国际会议(ICYC2011)

会议地点: 澳门

会议语种:中文

页码: 1-4

在线出版日期: 2011-07-22（万方平台首次上网日期，不代表论文的发表时间）