论文部分内容阅读
为了实现对认证协议的自动验证,首先,通过对认证协议的协议主体行为分析,给出了驱动模型(Driving Module,DM)的定义。然后,根据串空间模型中的常规者串和攻击者串分别构建了常规者DM和攻击者DM。最后,提出了基于常规者DM和攻击者DM的自动验证算法。实例分析和定理证明表明,该算法的搜索过程不仅是全面和正确的,而且能有效地避免状态空间爆炸问题。