安全协议,是以密码学为基础的信息交换协议。由于安全目标本身的复杂性、协议运行环境的复杂性以及攻击者模型的复杂性等多方面的原因,有必要借助形式化的分析方法或工具来完成对安全协议的分析和验证。在所有形式化方法中,模型检测是最具工业前景的技术,被用于验证系统性质。SPIN是一款卓越的模型检测工具,具有很强的系统建模能力,且在验证效率上的表现也十分出众,因此被许多学者与专家推崇和使用。本文详细介绍了SPIN模型检测技术的理论基础、SPIN模型检测工具的安装和使用方法、SPIN所使用的建模语言Promela语言及其细节、线性时序逻辑的语法和语义,并讨论了Dolev-Yao攻击者模型的通用建模方法。本文所做的主要工作和创新之处主要有以下几个方面:1.讨论了模型检测的原理,及其在安全协议自动验证中的应用。2.在Windows环境下,搭建了模型检测工具SPIN的运行平台,为今后同类研究的实验工作提供了基础。3.对SPIN的建模语言Promela进行了全面的介绍,详细讲述了它的简单和复合数据类型、运算符、通道机制以及各种流程控制语句,特别着重介绍了Promela语言的一些细节。这为今后同类研究工作应用Promela语言提供了参考。4.讨论了安全协议验证工作中,具有重要意义的Dolev-Yao攻击者模型,并给出了形式化定义,以及行为刻画的框架。这为今后同类研究在建立相同的攻击者模型时,提供了统一的框架与标准,大大减少了人为刻画的成分。5.以两个具有不同运行目标的安全协议—NSPK协议和A(0)协议为对象,遵循本文提出的DY模型的描述框架,以Promela语言实现了DY模型,以及协议主体,并进行了自动验证。验证结果成功地检测出了这两个协议的漏洞,与已有的工作相比,本文的工作得出的攻击过程更为精简。