随着计算机网络通信的迅猛发展,密码协议的重要性越来越得到重视。而在众多的验证方法中,模型检测方法在对密码协议的验证中体现出了它的优势。　　本课题研究的目的是采用模型检测技术对密码协议进行分析。文章介绍了密码协议研究的背景、概念和分类,给出了密码协议的系统模型,阐述了模型检测分析密码协议的理论技术。总结了验证密码协议的各种形式化方法后,详细研究了模型检测工具SPIN分析密码协议的方法,给出了SPIN对密码协议分析的原理,构造了系统验证模型。最后还对模型检测技术新的一个发展方向—“概率模型检测”进行了研究,归纳了几种概率模型和所使用的形式逻辑,采用PRISM概率符号模型检测工具对概率密码协议进行了分析,所取得的主要研究成果如下:　　(1)基于模型检测技术,使用SPIN对IKEv2协议进行了建模和分析。应用Promela语言描述了协议模型,并用LTL(Linear Temporal Logic)规约了该协议需要满足的认证性和机密性,发现了协议的两个攻击,然后对攻击产生的影响进行了讨论;　　(2)针对公平非否认协议给出了一种基于有限状态自动机的分析模型,并使用SPIN模型检测工具,对Zhou-Gollmann非否认协议进行了分析,验证结果查明该协议不满足公平性和机密性,为此对该协议进行了改进;　　(3)基于概率模型检测技术,建立概率非否认协议的有限状态自动机分析模型,使用概率模型检测工具PRISM模拟恶意实体能力和网络环境等不同情况,分析破坏协议公平性的概率分布。