随着网络技术逐步应用到许多重要部门,安全协议是否能达到所要求的安全目标是非常关键的问题。借助形式化的方法或者工具是分析和检验安全协议性质的一个重要技术手段。GSPM(Generic Security Protocol Model)是这样一种可以精确刻画安全协议的一般模型。本文就是在GSPM的基础上对安全协议的性质进行研究。首先,由于类型缺陷漏洞与协议的消息类型相关,并且GSPM对消息类型的匹配规则过于严格,导致类型缺陷漏洞无法通过该模型进行验证。所以,本文通过对GSPM语义的修改和对消息匹配语法做一定的弱化,使GSPM能正确检测类型缺陷漏洞。其次,在GSPM模型理论的基础上设计了一套分析安全协议的算法,包括消息推理算法,消息匹配算法和状态搜索算法。通过线性时序逻辑来表示安全协议的性质,例如保密性和认证性,并根据线性时序逻辑的特性设计了对应的检验算法。最后,本文介绍了一个自主开发的基于GSPM和上述检验算法的自动验证工具。这一工具能够将用户输入的安全协议及其安全目标自动翻译为GSPM语言;再根据GSPM的模型检测规则,通过特定的状态搜索算法,自动计算和判断安全性质是否满足,并将可能的漏洞告知用户。