随着网络的发展,互联网络的安全问题变得越来越棘手,越来越重要,安全协议的安全性质也受到越来越多的挑战。安全协议是解决互联网络安全问题最有效的手段之一,使用安全协议在开放的互联网络上可以实现身份认证等多项安全功能。由于在计算机网络中,相互通信的双方不能通过生物特征识别对方,因而彼此的认证需要建立在密码体制的基础上。安全协议是建立在密码体制基础上的一种通信协议,它运行在计算机网络或分布式系统中,借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重要。然而,设计并投入实际应用的安全协议在运行时不一定能够真正实现它所声明的安全性质。许多协议在应用了很长一段时间后被发现存在安全漏洞。设计和开发高效的安全协议建模与验证的方法和工具是安全协议形式化研究领域的一个研究热点,也是验证复杂安全协议的关键环节。本文以Bruno Blanchet提出的Horn逻辑模型为基础,对反例构造算法和复杂协议验证方法进行了系统、深入的研究,主要工作包括以下几个方面:1.基于Horn逻辑的安全协议反例的自动构造算法。Bruno Blanchet提出了基于Horn逻辑的安全协议模型,该模型可高效地验证安全协议。为了将消息的角色信息保留在模型中,本文设计了相关的数据结构,给出了反例自动构造的算法实现,使验证工具能从不满足安全性质的消解序列中自动地构造出标准形式的反例,从而方便人们使用基于Horn逻辑的验证工具验证协议。2.不动点计算的不停机性预测。安全协议验证的不停机性源于不动点计算的不停机性。通过研究安全协议逻辑程序解形式不动点计算不终止的特征,本文给出了不动点计算不终止的预测方法。基于此方法,可以在协议验证时自适应地选择(精确或抽象)验证方法验证(停机或不停机的)安全协议。3.抽象与精化迭代验证框架。安全协议的正确性验证问题是不可判定的,使用抽象解释理论能够有效地验证安全协议。通过研究Horn逻辑模型中协议验证的特点,给出了安全协议基于抽象-精化的迭代验证理论框架。抽象验证保证停机,而精化过程可有效地去除虚假反例。因此,抽象-精化迭代框架可对Horn逻辑模型中验证过程不停机的安全协议进行有效验证。为了提高抽象模型的精度,本文进一步提出了局部抽象-精化迭代验证的理论框架。局部抽象可以提高整个验证过程的验证效率,为复杂协议的验证提供了有效的途径。4.时间敏感安全协议的建模与验证。通过将描述时间的事件加入到进程代数模型中,使得时间戳能方便有效地在协议模型中描述出来。将时间元素的线性约束加入到基于Horn逻辑的安全协议模型中,使得Horn逻辑模型能有效地处理时间约束信息。通过研究规则中各时间元素与消解的关系,找到了确定时间相关元素的时间先后关系的办法,提出了两阶段验证方法。一条规则是否可用,此时还需考察其所对应的约束系统是否可满足。因此,本文对该模型下的约束系统进行了研究,提出了一个高效判断其可满足性的判定算法,并证明了该算法是多项式时间算法。由于约束系统中存在大量冗余的不等式,本文还深入研究了该系统,针对其本身的特性,提出了约束的抽象理论简化约束系统,该方法能有效地降低时空开销。5.设计并实现了一个高效的安全协议验证工具SPVT-II。本文提出了不停机性预测和抽象-精化迭代验证框架的实现算法,在安全协议自动分析工具SPVT的基础上,结合抽象-精化迭代验证框架,设计并实现了一个自适应选择验证方法的高效的协议验证工具SPVT-II。该工具既能发现协议中可能的反例,也能尽可能地减少虚假反例的产生。6. Kerberos协议协议的分析与验证。本文通过对Kerberos协议进行分析,将公钥Kerberos协议的认证服务交换阶段进行了建模,并用SPVT-II对协议模型进行了自动化的验证。实验结果表明SPVT-II能自动发现PKINIT-26中认证服务阶段的攻击。