当今，随着网络技术的迅猛发展和广泛应用，网络已经成为人们共享信息的主要方式，人们可以随时、随地以各种方式提供和接受信息。然而，网络技术是一把双刃剑，在给人们带来巨大便利的同时也给信息的安全造成巨大威胁。因此，在当今信息社会，信息安全的重要性与日俱增。而作为网络通信基础的安全协议是通信各方的桥梁。由此可见，协议安全是信息安全领域的重要课题。　　然而，设计一个健壮有效的安全协议非常困难，这不仅因为网络的复杂性还因为安全协议的多目标性。实践证明，设计和分析安全协议需要依靠形式化方法和理论。经过20多年的研究和发展，在安全协议的形式化方法和理论领域，百家争鸣，百花齐放。但是，现有的形式化理论和方法都不完善。因此，深入研究安全协议的形式化分析理论和方法意义重大。　　安全协议的形式化分析方法主要分为三类：基于推理结构的方法，又称形式逻辑方法，基于攻击结构的方法，又称模型检测方法，基于证明结构的方法。基于逻辑的形式化方法是最直接也是最简单的方法，已经被广泛研究和应用。Rubin博士提出的Rubin逻辑是第一个可以推理非单调协议的逻辑。与BAN类逻辑相比，Rubin逻辑有诸多优点。可以说，Rubin逻辑是安全协议分析中一个有潜力、有前途的方法。模型检测技术一般使用自动化工具，在自动程度方面表现良好。属于高级Petri网的有色Petri网已经被证明是一个适于安全协议建模的方法。尽管如此，使用有色Petri网分析安全协议仍然需要进一步研究。　　本文主要对安全协议的Rubin逻辑的形式化方法与基于有色Petri网的模型检测技术进行了深入研究，我们还系统研究了这两种方法在协议形式化分析中的应用。我们对Rubin逻辑进行了一系列扩展和改进。此外，我们还提出了两种基于有色Petri网的协议分析新方法。我们采用上述新方法分析了多个安全协议。总的来讲，从理论和实践两个层面上研究了安全协议的形式化分析。主要工作有以下几个方面：　　1.对安全协议的基本理论进行了研究，介绍了安全协议的基本概念，给出了一个安全协议模型，分析了安全协议的基本性质。指出了安全协议分析的复杂性。并着重对目前的安全协议分析形式化方法进行了分析和讨论。　　2.研究了基于逻辑的安全协议形式化分析方法，其中对ZQ逻辑和Rubin逻辑进行了着重的研究。介绍了BAN逻辑及其两个重要扩展GNY逻辑和SVO逻辑。提出了一个新的可追究和公平协议，这个协议是ISI支付协议的一个改进版本，并用ZQ逻辑分析了新的协议满足追究性和公平性。此外，应用Rubin逻辑分析了Andrew安全RPC协议及其两个改进协议，发现原始协议存在已知漏洞，并且发现G.Lowe修改后的协议仍然存在漏洞，随后，提出了一个新的改进，克服了所发现的漏洞。还应用Rubin逻辑分析了SSL协议的恢复一个已存在的会话模式。此类实用协议往往难以用BAN类逻辑来分析。分析发现，此模式下SSL协议能够实现建立新的安全连接的目标。这两个例子说明Rubin逻辑能够较好的克服BAN类逻辑的缺陷。　　3.着重研究了如何扩展Rubin逻辑，并提出了三个扩展。研究发现Rubin逻辑难以分析含有时间戳的消息，此外，Rubin逻辑不适用于分析非否认性、可追究性及公平性，而这三个性质都是电子商务协议强调的安全性质。由此，提出对Rubin逻辑的三个扩展。第一个扩展可用于分析含有时间戳的消息。采用ZQ逻辑的思想提出了第二个扩展，可用于分析非否认性。第三个扩展是在第二个基础上进行的，可以分析非否认性、可追究性和公平性，阐述了如何应用改进后的方法对电子商务协议进行分析。这三个扩展彼此联系，可以根据协议类型不同灵活使用。　　另一方面，采用扩展后的Rubin逻辑对三个分属不同类型的安全协议进行了分析。分析了采用时间戳的X.509认证协议，发现协议不仅不能实现它的三个目标而且还存在冗余。随后给出了两个改进，其中一个改进没用使用时间戳。此外，分析了MANET中一个安全路由协议——ARAN，尤其，分析了协议中证书废除这种非单调的知识。发现了该协议存在的一些问题，并提出一个改进。还分析了Zhou-Gollman协议这一经典的电子商务协议。与其他方法不同之处在于，不仅分析了该协议的可追究性和公平性，还分析了其机密性，完整性和新鲜性。发现该协议可以满足完整性，但是不能实现机密性，交易双方也很难确定消息的新鲜性。实例分析表明，扩展后的Rubin逻辑不论在分析认证协议还是分析电子商务协议中都表现良好。　　4.研究了有色Petri网的基本理论及其一个自动化工具CPNTools。阐述了Petri网及有色Petri网的形式化定义。分析讨论了有色Petri网的动态特性。此外对CPNTools的应用接口及如何使用这一工具对有色Petri网进行建模和分析进行了探讨。　　5.重点研究了使用有色Petri网的协议模型检测技术，提出了两种分别适用于分析认证协议和电子商务协议的有色Petri网新方法。先是给出了一个网上阅卷流程的分层有色Petri网模型，并分析了该模型的并发、冲突和关系依赖。该建模方法可以作为安全协议建模的基础。在对当前流行的基于有色Petri网协议分析方法研究基础之上，提出了一个采用有色Petri网和CPNTools的认证协议分析方法。该方法的主要贡献在于入侵者有色Petri网模型的建立，该模型是开放的，可以融合多种攻击策略，这对于避免状态空间爆炸有良好作用。随后运用新方法对Andrew安全RPC协议的一个改进版本进行了分析，同样发现了一个G.Lowe找到的攻击。此外，提出了一个用于分析电子商务协议的融合ZQ逻辑及有色Petri网的新方法，新方法无需建立争端仲裁模型。应用新方法分析了ISI支付协议，发现该协议的一个不安全的状态，分析得到协议不能满足可追究性和公平性。新方法目的在于建立充分小的模型，避免传统方法指数级的状态搜索。该方法同样基于ZQ逻辑，是模型检测技术与形式逻辑结合的新尝试。