作者：唐郑熠 李均涛 李祥新鲜性协议攻击模型检测spinpromela
摘要：非形式化方法很难保证认证协议的安全性，因此对于形式化方法的研究与应用具有重要的意义，模型检测技术就是其中的一种。该文介绍了使用模型检测工具SPIN和Promela语言对A（0）协议进行建模检测的方法，并从检测结果中发现了A（0）协议无法保证公开协商密钥证书新鲜性的缺陷。据此设计出了针对A（0）协议的新鲜性攻击方法，并提出了弥补其新鲜性缺陷的改进方案。由此可见，使用模型检测技术可以高效便捷地对认证协议进行分析。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
