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