串空间和认证测试在协议分析中的应用

摘要：

串空间模型是一种新兴的密码协议形式化分析工具.分别采用串空间模型争认证测试这两种前沿的形式化分析方法对X.509协议的认证性进行了分析,指出了该协议在认证正确性方面存在的缺陷.然后针对分析结论提出了改进协议,并使用认证测试方法证明了改进的协议能够实现认证的正确性.通过比较发现应用认证测试方法分析安全协议,比单纯应用串空间模型更为简洁和直观.

关键词：安全协议、串空间、认证测试、x.509

所属期刊栏目：24

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金69873040;基于时间自动机的模型验证理论及应用研究2006520015

在线出版日期：2009-02-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：179-181