论文部分内容阅读
通过对协议执行过程的分析，给出了驱动模块（Driving Module，DM）的定义。然后，结合串空间模型构建了常规者DM和攻击者DM，并在此基础上提出了一种分析会话密钥分配协议的新攻击构造法——基于DM的模型检验方法。定理证明和实例分析表明，该方法的搜索广度和深度都是完善的，而且可以避免状态空间爆炸问题。