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

A new method for analyzing and improving security protocols

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

By analyzing the process of security protocols, the definition of driving module （DM） is introduced, and then regular and penetrator DMs are formed according to the Strand Space Model （SSM）. Based on this, a DM-based model checking method is proposed. Theoretical analysis indicates that this method is prefect in terms of searching breadth and depth, and can avoid the state space explosion problem. Therefore, this method can be used not only to get the attack scenarios of a flawed security protocol, but also to prove that an unflawed security protocol is secure. Moreover, the Otway-Rees protocol and the TLS protocol are analyzed based on this method. As a result, various attack scenarios of the Otway-Rees protocol are discovered and two secure improved Otway-Rees protocols are put forward, and therefore the TLS protocol is proved to be secure.