一种分析会话密钥分配协议的新方法

A New Method for Analyzing Session Key Distributed Protocols

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

By analyzing the process of a security protocol, the definition of Driving Module（DM） is given. Then, regu- lar and penetrator DMs are formed according to the Strand Space Model（SSM）. Finally, a new method for analyzing session key distributed protocols is proposed based on these regular and penetrator DMs, i.e. a model checking method based on DMs. Theorem proofs and case analysis show that the search breadth and depth of this method is prefect, and it can avoid the state space explosion problem.