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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社