基于串空间和状态转换的认证协议分析方法

摘要

串空间是一种新兴的安全协议形式化分析模型.串空间模型中的理论证明方法虽然严谨,但难度很大.本文基于串空间模型,首先定义系统状态,并以Needham-Schroeder-Lowe公钥认证协议为例说明系统状态转换的分析过程.通过对状态转换过程中现实的跟踪考察,得出了有意义的结论.结合串空间模型,验证了该认证协议的安全性.这种分析认证协议的新方法简洁和高效,并易于实现自动化.