论文部分内容阅读
非形式化方法很难保证认证协议的安全性，因此对于形式化方法的研究与应用具有重要的意义，模型检测技术就是其中的一种。该文介绍了使用模型检测工具SPIN和Promela语言对A（0）协议进行建模检测的方法，并从检测结果中发现了A（0）协议无法保证公开协商密钥证书新鲜性的缺陷。据此设计出了针对A（0）协议的新鲜性攻击方法，并提出了弥补其新鲜性缺陷的改进方案。由此可见，使用模型检测技术可以高效便捷地对认证协议进行分析。