安全协议,是指在通信协议中应用密码学的手段隐藏或获取信息,达到认证以及消息正确发送的目的的协议。而随着互联网的迅猛发展,安全协议的安全性成为网络安全的关键。虽然安全协议是安全专家精心设计并仔细检查过的,但由于协议之间消息交互存在着复杂的关系和制约,而且大部分的安全协议运行在复杂的分布式网络环境中,因此,通常安全协议都存在一些不容易发现的安全漏洞。模型检测的基本思想是用状态转移系统S表示系统的行为,用模态时序逻辑公式F描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态转移系统S是否是公式F的一个模型?”,用公式表示为S|–F。本文主要将基于时序认知逻辑的模型检测的思想运用到安全协议的检测中,主要内容包括:首先,用Spi演算来描述协议主体的行为,然后通过本文提出的规则,将其转换成一个状态转移系统,作为本文的模型M。其次,对K算子进行了重新定义,加入到CTL当中,形成了KCTL逻辑,然后用KCTL公式F来描述协议应满足的性质,并给出了KCTL逻辑的模型检测算法。最后,验证性质公式F在模型M上是否满足。本文以著名TMN协议为例,对本文提出的方法进行了验证,找出了协议的漏洞,证明了本文提出的方法的有效性。本文还设计了一个验证系统,给出了系统的模块构成和主要算法的思想。此外,作为对KCTL的扩充,本文还提出了μ-BDI逻辑,并给出了μ-BDI逻辑的模型检测算法。