随着科学的发展和社会的进步，信息技术的不断向前发展，计算机互联网及其分布式系统的应用变得越来越广泛，密码协议在人们日常生活生产中的运用越来越受到关注，人们对密码协议的可靠性和安全性的要求越来越高。任何不可预测的错误都会产生极其严重的后果，而模型检测就是一种能保证协议系统在设计时就证明是正确的，在其设计的过程中就发现是否有错的自动化验证有力技术。这一检测技术的基本原理就是用状态迁移系统来表示系统的行为，以模态或时序逻辑来对系统的性质进行描述。这样，系统是否具备所期望的性质，以及状态迁移系统是否是公式的一个模型，就转化为了一个数学公式，密码协议的安全问题就转化为一个数学问题。它通过系统模型的构建，来检测所期望的性质是否满足所建的模型，如不满足，就会给出相应的反例。本文的主要工作是采用系统验证工具SPIN首先对LEAP进行形式化分析研究，然后分别采用SPIN和AVISPA对其改进协议——LEAP+A，LEAP+B进行了验证，分别用Promela和HLPSL对其进行建模，找出针对这些协议的攻击，获得攻击者的相关信息，查看其中存在的漏洞，同时对以上主要项目的结构，原理和操作过程进行了描述和论证，对消除这一漏洞的方案进行了研究改进与分析，以使其最大限度的杜绝这类攻击。