在本文中，我们探讨了有关两种安全协议形式化理论的若干问题，其中，工作重点集中在对三方认证密钥交换协议的形式化分析上。 网络技术具有快速实现信息共享的特点，这大大提高了人们通信的效率，给人们的生活、学习和工作带来了巨大的改观。但与此同时，人们对网络本身具有的公开性和匿名性所带来的日益严重的信息安全问题也深感不安。 为了解决网络的信息安全问题，人们设计了许多用于开放网络的安全协议来解决各种安全应用问题。所谓安全协议，就是两个或两个以上的参与者采取一系列步骤来完成某项特定的安全任务。它包含三层含义：1．协议需要至少两个参与者。2．参与者之间执行的是消息处理和消息交换交替进行的一系列步骤。3．通过协议执行必须能够完成某种安全任务。 由于每个安全协议都是为了某种安全应用而精心设计的，协议中的各条消息间有着微妙的相互制约关系，因此若采用人工方式对协议进行安全性分析，往往不能发现协议存在的问题，所以必须借助于形式化的方法来完成。形式化方法是一种用于描述系统性质的数学方法，它主要用于发现一个系统中的歧义性、不一致性与不完备性。该系统可以大到一个企业级的软硬件系统，也可以小到有若干条消息组成的协议。对安全协议使用形式化的方法，可挖掘出协议消息所表示的内在含义，对协议的正确性进行验证。通过验证，不仅可证明协议是否符合预期的安全目标，而且对不符合安全目标的协议可分析其缺陷之所在，进而为协议的设计提供有力的支持。 目前在安全协议形式化的研究领域有两种截然不同的理论：符号理论与计算理论：