如今中国已经进入了一个互联网+的时代,各行各业都搭上了互联网的快车。安全协议作为一个关系到互联网流通的信息安全的重要因素,变得举足轻重。目前分析协议的方法多种多样,模型检测作为一种形式化方法受到广泛关注和认可。本文在前人建模、验证的基础上,扩展出反例分析阶段。试图从反例角度出发,从反例中提取有效信息,通过分析反例来定位漏洞位置。模型检测方法具有两个主要的优点:第一,模型检测具有高度的自动化,可以使研究者从繁杂的搜索任务中解脱出来。第二,当系统或者协议不满足约定的性质时,模型检测工具可以返回一个源码级别的事件序列,既反例。但是随着功能的增加和完善,现有的系统和协议变得越来越复杂,与之对应的反例数量越来越多,内容也越来越复杂,因此对反例的分析也变得越来越困难。本文提出了消除众多相似反例的方法。在使用模型检测器对协议进行验证时候,我们发现会有大量的相似反例,他们体现了同一个安全漏洞,但我们仅仅需要一个此类的反例,过多的反例只会增加系统负担,给分析反例的过程带来干扰。本文通过引入节点权重方法来在反例生成时消除相似反例。为了保证去重效果又增加了反例生成后的消除过程。以此来保证反例集合中没有相似反例。反例中蕴含了丰富的有关漏洞的信息,为了能够快速的挖掘协议漏洞,我们提出了基于多反例的漏洞挖掘方法。在消除相似反例之后我们需要对反例进行分析,由于反例长度大,内容混杂,提取反例的有效信息就变得很困难。为了充分利用反例中的信息,在对众多反例中的语句分析时,我们采用了统计方法taratula和距离度量方法。Tarantula技术可以统计反例中出语句的频率,生成语句的怀疑度排序表,从表首依次分析这些语句。在对每个语句进行分析过程中,使用距离度量技术找到状态空间中与该反例最接近的成功执行路径,通过分析比较两者的差异,最终定位漏洞所在。本系统的建模、检测过程和漏洞挖掘都是基于模型检测工具spin及其图形界面工具ispin的。将以上算法融入整个系统,对spin和ispin做出改进。最后通过实验对本系统在功能和性能上做出评估。