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