信息对当代社会具有重要作用，信息安全依赖于安全协议的应用。对安全协议的分析是一项极有价值的工作。目前的安全协议验证工作主要采用各种形式化方法，如模态逻辑证明、定理证明理论以及模型检测方法。模态逻辑技术采用各种公式进行论述，验证是否能实现预期要求，操作流程比较简便，其中著名的方法有BAN逻辑、SVO逻辑、Kialar逻辑等；定理证明理论通过对各实体进行定义，利用命题证明检验缺陷的有无，其中应用较多的技术有Isabelle技术、串空间等。随着各种检测手段的发展，入侵技术也在不断更新，原有检测手段的不足逐渐显露出来。模态逻辑方式虽然易懂易用，可有时不能提供精确的表达，分析能力有限；定理证明方法较模态逻辑有了较大改进，验证过程更加严谨，但是检测内容主要集中在协议正确性方面，验证能力比较有限，证明过程不是很好理解，而且难以实现自动化。即便如此，这两种分析方法还是在协议验证中作出了重要贡献，检测能力比早期的人为判断有很大进步。模型检测方法的使用较晚，但应用已经比较广泛了。该方法最早被用于硬件验证，随着上世纪末被引入安全协议领域后，经历了一个飞速发展的阶段。模型检测技术根据系统模型和验证属性进行状态空间搜索，其优势在于自动化程度高，用模型检测工具进行自动分析，大大减少了人工干预，当验证属性不满足时能够提供相应的反例。本文首先介绍了密码学和安全协议的理论基础，重点介绍了形式化方法的理论和技术。接着介绍了模型检测技术的工作原理，对模型检测工具SMV的工作过程进行实例说明。之后，采用基于理论证明的串空间技术对Otway-Rees协议、NSPK协议进行分析。最后，本文利用模型检测工具SMV对Otway-Rees协议、NSPK协议以及两种协议的修改版本进行了验证，检测协议中是否存在缺陷。经过检测，验证了先前理论对两种协议的分析，以及模型检测方法的有效性。