基于前推的密码协议形式化分析方法

作     者：闫靖晨 高宏彪 程京德 Yan Jingchen;Gao Hongbiao;Cheng Jingde

作者机构：埼玉大学信息与计算机科学系 

出 版 物：《信息安全研究》 (Journal of Information Security Research)

年 卷 期：2017年第3卷第5期

页      面：462-468页

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：密码协议 形式化分析 定理证明 模型检测 前推 

摘      要：在高度信息化社会,各种安全的密码协议是保证网络空间中众多应用所必须的安全性以及公平性的必要技术手段.由于密码协议的安全漏洞会给网络空间应用带来严重的安全问题,甚至造成不可估量的损失,因此密码协议的安全性分析成为重要课题.目前,作为基于证明的形式化分析方法,定理证明方法和模型检测方法被广泛用于密码协议形式化分析.这些方法是通过预先列举出安全性目标,然后证明和检测密码协议是否满足这些目标,进而证实密码协议是否隐含有安全漏洞.基于证明的密码协议形式化分析方法在原理上的缺点是,如果预先列举的安全性目标有遗漏,那么有些安全漏洞则不可能被发现.基于前推的密码协议形式化分析方法不需要预先列举安全性目标,而是通过对参与者和攻击者的行为来进行基于逻辑系统的前推,推测针对密码协议所有可能出现的攻击来发现安全漏洞,从而保证密码协议的安全性.介绍了一种具体方法,根据各种密码协议的特点对密码协议和攻击者行为进行形式化,用形式化的结果来进行基于逻辑系统的前推,并通过分析推导出的逻辑公式找到所有成功的攻击,进而发现密码协议的安全漏洞.