安全协议，又称密码协议，是指运行在计算机网络或者分布式系统环境下，依赖应用密码学技术完成身份认证、密钥分配或者电子交易等任务的协议。它的正确性是网络和分布式系统应用安全的基础，针对这些协议进行形式化分析长期以来一直是安全领域的重要研究课题。 安全协议形式化分析的目标是协议的关联性、保密性，以及与电子商务相关的不可否认性、公平性和时限性等，论文的研究工作主要针对其中的基本属性——关联性和保密性展开。大部分已有的分析方法或者采用信仰逻辑等推理技术，或者采用状态检测等定理证明技术，前者分析能力较弱，而后者存在状态爆炸问题。因此，目前研究的一个趋势是综合应用多种分析手段，取长补短，以达到最好的分析效果。与之相对应，论文提出了一种新的基于挑战一响应的分析方法，该方法采用线空间模型作为底层的语义模型、采用认证逻辑作为基本分析手段，并融合了Athena算法、认证测试等多种技术。全部研究内容可以划分为四个层面，分别是建立语义模型、提出分析手段、设计自动化工具和协议分析应用。 在语义模型方面，采用线空间模型作为底层语义模型，给出了协议关联性和保密性的明确的形式化定义。将保密性分析分解为显式泄密和隐性泄密问题，其中隐性泄密分析依赖于关联性的判断；而关联性的分析被总结为协议Strand之间的存在关系和Strand参数的一致性问题。 在分析手段方面，充分利用认证逻辑、Athena算法、认证测试等现有研究成果，并从中提取出新鲜性、唯一生成，测试和Nonce验证等共有的概念，指出安全协议本质上是协议主体采用密码学方法通过挑战一响应来对协议其他方的存在做出判断，同时完成一些数据如会话密钥的协商的过程，挑战一响应是协议分析中最小的有效单位。在此基础上，提出了一种新的形式化分析方法。 在自动化工具方面，采用Prolog语言设计并实现了一个基于认证逻辑的协议分析工具，可以有效推导并判断协议在特定的目标上是否满足需求，在自动化工具设计领域进行了初步但有益的尝试。 在协议分析应用方面，针对五个具有代表性的安全协议给出了形式化的分析。对于有缺陷的协议，给出了错误的根本原因和可能导致的攻击；对于正确的协议，给出了形式化的理论证明。通过实际应用，演示并验证了论文所提理论和方法的正确性和有效性。 总的来说，论文针对安全协议的形式化分析进行了深入的研究，提出的方法很好地解决了分析能力和易操作性之间的平衡问题，新的分析方法既具有线空间模型的分析能力，又具有认证逻辑方法的易用性。