一种分析和改进安全协议的新方法

分析安全协议的执行过程,给出驱动模块(Driving Module,DM)的定义,利用串空间模型构建常规DM和攻击DM,由此给出一种基于驱动模块的模型检验方法。理论分析显示,该方法搜索广度和深度完善,能避免状态空间爆炸问题,可用于获得有缺陷安全协议的攻击剧本,并证明无缺陷安全协议的安全性。用该方法分析OtwayRees协议和TLS协议,获得了Otway-Rees协议的攻击剧本,得出了Otway-Rees协议的两个安全改进版本,说明了TLS协议的安全性。

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

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