随着互联网在人们的生活中应用的越来越广泛,网络安全也变得愈加重要。安全协议作为信息安全的重要组成部分,对其进行分析具有重要的研究价值。目前分析安全协议的方法多种多样,模型检测作为一种形式化分析方法被广泛的应用于安全协议的分析。本文以模型检测器生成的反例为基础,对安全协议进行分析得到协议的攻击路径。模型检测相比于其他形式化方法具有很多优势。模型检测是一个高度自动化的技术,将使用者从繁杂的公式推理中解放出来。当输入模型违反系统规约时,模型检测器会产生一个从系统的初始状态到违反规约状态的路径,即反例。现有的模型检测器会产生多个违反系统规约的反例,然而其中很多反例都对应同一条错误路径,仅仅是在实例数据取值上存在不同。模型检测器产生的冗杂的反例集合给反例的分析带来了困难。在模型检测器检测协议模型的过程中,协议的建模显得尤为重要。本文以NSPK协议为例,使用模型检测器SPIN的建模语言promela对其进行建模,同时分析出该协议模型需要满足的安全性质,使用SPIN对协议模型进行检测后得到多个反例。为了解决模型检测器生成的众多反例间的数据相似性问题,本文提出使用反例的等价类对多反例进行精简的方法。该方法保证每个反例的等价类都只包含一个反例,使得精简后的反例集合中的每个反例都代表一条不同的反例路径,大大减少了反例的数量,提高了系统的运行效率,为多反例的分析打好了基础。在传统的基于单反例的协议分析的方法中,由于单个反例含有的信息有限,研究人员往往不能准确地找到系统错误。为了解决这个弊端,本文使用精简后的多反例集合对安全协议进行分析,充分利用了多反例包含的信息。我们使用Tarantula方法统计反例中语句出现的频率,计算各个语句的可疑度,并找到最有可能包含协议模型错误的反例,最终根据该反例得出安全协议的攻击路径。与原本的模型检测器SPIN相比,本文的方法在SPIN的基础上增加了多反例精简和多反例分析安全协议的功能。以NSPK协议为例,本文的方法将SPIN产生的1809个反例精简到13个,并且将系统的运行时间由0.67秒提高到0.31秒。最终,根据反例的分析结果发现协议中存在未添加协议通信双方标识符的漏洞并给出了改进意见。