网络的最大特点是共享,相伴产生的安全问题也成为人们不得不面对的问题,特别是用来保证信息传输安全的网络安全协议的安全性显得尤为重要,常被人们称为安全之上的安全。因此对安全协议进行分析,查找其漏洞和不足是学术界和工业界共同关注的课题。传统的形式化验证技术主要有逻辑推理,但该方法不能做到完全自动化验证,对于稍微复杂的系统,自动化的推理就难以胜任。人为的推理过程十分繁琐,费时费力,效率较低,因此该方法在实际应用中很有限。　　 本文在谓词抽象和小系统理论的基础上,运用状态空间抽象方法和形式化验证技术中的模型检测技术对SSL3.0的握手协议进行系统建模,使用新型符号模型检测工具NuSMV描述系统性质,最后通过验证给出的反例找到协议可能会受到的攻击。本文的主要内容包括:　　 (1)介绍模型检测技术、抽象解释理论、谓词抽象理论和小系统模型理论的基本概念,详细阐述其对系统模型的具体验证过程,由此分析此方法在应用中的特点；然后介绍线性时态逻辑和计算树逻辑两种对系统性质的描述方式,并从各自的语义出发进行比较,阐述其各自适用的范围；最后总结安全协议模型检测分析的现状及问题。　　 (2)给出一种处理安全协议状态迁移系统的有效的抽象方法。该方法建立在谓词抽象和小系统模型理论的基础之上,首先对安全协议的无穷状态进行谓词抽象,精简系统规模,然后在抽象后的状态空间中建立协议运行的小系统模型,通过确定协议运行的主体、各主体运行的次数等假设条件,进一步构建安全协议的抽象模型。在此模型上进行安全协议的形式化验证,比单独依靠谓词抽象和小系统理论更加有效、快捷。　　 (3)运用基于谓词抽象和小系统模型理论的组合抽象方法对SSL3.0握手协议的原型系统进行模型检测。首先使用本文给出的组合抽象方法对SSL3.0握手协议进行系统建模,然后运用计算树逻辑公式CTL对协议系统的性质进行正面描述,最后运行模型检测工具NuSMV2.5.2,得出验证结果。如果所建立的模型不满足性质,NuSMV将给出对应的反例,通过对反例的解读,找到协议模型的漏洞所在,并给出相应的完善协议的改进方法。