计算机网络正以惊人的速度向各个领域渗透,其中的安全问题也变得越来越突出和复杂,解决安全问题对许多网络应用来说已是头等大事。从目前解决安全问题的方式来看,安全协议是解决网络安全问题最有效的手段之一。如何保证安全协议的安全性是安全协议研究领域的一个关键问题。为了保证和验证安全协议的安全性,研究人员提出了形式化的方法。经过二十多年的发展,安全协议的形式化方法得到了快速的发展和广泛的应用,已经成为公认的,在安全协议验证和设计领域最为合理、有效的方法。形式化方法通过建立科学的理论模型,对安全协议进行严格的数学和逻辑推导,以此来证明安全协议的安全性或指出安全协议中存在的安全缺陷;同时,形式化方法还可用来指导安全协议的设计。虽然形式化方法已经成功地发现了许多安全协议的漏洞和攻击,但是,这些方法仍然存在很多问题。通过综合分析这些方法,我们发现,现有分析方法中有两个固有缺陷:一是没有明确的形式化的方法来统一描述多种安全属性;二是缺乏一般化的形式语言模型作为分析安全协议的统一框架。针对上述两个固有缺陷,我们从三个层面逐步深入地进行了研究:首先,我们深入研究了三类典型且重要的形式化分析方法:类BAN逻辑、串空间、SPI演算,分析了他们的固有缺陷,有效地改进了他们的部分缺陷。其次,我们提出了一种用有向图来描述协议运行的分析方法,该方法部分解决了目前协议分析方法共性问题中的第二个固有缺陷。最后,我们提出了一个安全协议的统一分析框架,在更高的抽象层次上对安全协议运行和安全属性及其验证方法进行形式化建模,并在这个框架指导下,基于符号迹的方法设计了一种新的协议分析方法,实例分析表明该方法是有效的。我们提出的安全协议统一分析框架是解决目前安全协议分析方法两个固有缺陷的一次有意义的尝试,取得了一定的科研成果。本文的主要创新点如下:(1)改进类BAN逻辑在“理想化协议”步骤和单调性信任关系方面的缺陷,提出了基于消息唯一起源的动态逻辑方法。通过消息唯一起源的概念,解决了“相信事情的发生”和“相信事情的真实性”两种不同信任的区别,在此基础上建立了动态逻辑方法。(2)定义了新的类BAN逻辑语义模型,分析了类BAN逻辑的本质缺陷。该模型定义了“可能世界”及“可达关系”的概念。在这种模态逻辑框架下,我们给出了类BAN逻辑的真值赋值函数。从理论上证明了类BAN逻辑的逻辑语义缺陷是不可逾越的。(3)提出了安全属性的统一形式化描述方法,尝试用匹配关系来描述安全属性。在研究过程中,我们对此做了进一步的改进,安全属性被最终定义为:实体的时序消息与属性消息之间的推导关系。该定义脱离具体协议,是对安全属性的抽象建模,因此,更具有普适性。(4)将进程演算与实体消息推理结合起来,采用匹配关系来描述安全属性,提出了组合分析方法。该方法一方面弥补了进程演算缺乏数据结构来表示实体知识的缺陷,另一方面明确指出了在符号迹的分析过程中,如何及何时进行带符号的消息推理。由于采用了与协议无关的安全属性形式化描述方法,该方法扩展性很强。(5)提出了安全协议有向图分析法,部分解决了当前分析方法在协议运行的形式化建模方面的缺陷。该方法将协议规范中的每个协议步骤分解为有序动作序列,给出协议的有向图生成规则以及能够准确地跟踪协议消息的多种构造途径的消息构造逆向搜索算法。(6)提出“安全属性建模+协议运行建模”模式的统一分析框架。在统一框架的基础上,采用时序消息的推导关系来描述安全属性,为符号迹方法增加时间概念和基于时间的消息推理规则,从而有效地构造了基于符号迹的安全协议分析方法。这种统一分析框架对于安全协议的设计和分析方法的设计具有十分重要的意义。