摘要
分析安全协议的执行过程,给出驱动模块(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.
出处
《西安邮电大学学报》
2015年第5期17-23,共7页
Journal of Xi’an University of Posts and Telecommunications
基金
国家自然科学基金资助项目(61402367)
陕西省信息化技术研究计划资助项目(2013-008)
西安邮电大学青年教师科研基金资助项目(401-1201)
关键词
驱动模块
串空间模型
安全协议
模型检验
攻击剧本
driving module, strand space model, security protocols, model checking, attack scenarios