鉴别协议在网络安全中占有很重要的地位,而对于鉴别协议的设计和分析都是很困难的。如果通过验证已有的攻击手段来分析鉴别协议,最主要的问题是我们无法穷尽所有的攻击类型。所以我们求助于形式化的方法。模型检测技术已经被证实是比较成功的协议分析的方法。我们采用模型检测工具NuSMV去验证鉴别协议,NuSMV支持线性时序逻辑。另外,我们采用了Gavin Lowe的研究成果,即如果要验证的协议满足一些前提条件并且在小系统模型上没有攻击,那么在任意的系统上都没有攻击,也即,对这个协议来说,模型检测是完备的。我们修改了一些协议,使其满足“一些前提条件”,然后在小系统模型上进行验证。通过修改、验证协议的过程,我们提出了一种新的鉴别协议设计方法。用这种方法设计出来的鉴别协议在小系统模型上如果是安全的,那么我们确信它是安全的。并且,我们在这个设计思想指导下设计了一个新的Test协议,使用NuSMV验证,验证的结果它是安全的。