摘要: 认知逻辑的Kripke语义已经被成功应用到通信协议的推理分析中 (例如, 交替位协议(Alternating Bit Protocol) 的分析, 及最近的对TCP 的分析). 因为信息交换本质上可以看成是个认知过程, 用认知逻辑可以很方便地表达. 然而, 这些应用都假设网络是安全的，无黑客的存在.由Burrows, Abadi 和Needham提出的BAN逻辑及类BAN逻辑曾在应用认知逻辑验证安全协议上作出了尝试. 然而, 他们不是在协议本身上进行分析, 而是需要用户对协议理想化 (idealizations) 的结果上进行分析, 而这种所谓的理想化过程无法直接转化为算法. 并且他们只是用认识逻辑描述协议的规范, 但没有给出相应的算法, 即给出一个具体的协议，如何自动生成公理集并自动验证他满足一些认知规范.为了弥补这个缺陷,　本文给出了一个对安全认证协议进行验证的基于认知逻辑理论的模型.　我们将使用一类特殊的等价的Kripke语义, 即知识结构. 这种语义结构有别于传统的基于运行轨迹（trace）的语义, 他是基于每个智能体的观察（Observation）的语义. 这样使得知识算子的计算成为了可能. 并且我们发现，其逻辑计算, 可以直接转成可满足性问题（SAT）进行处理, 从而可以利用工业上高效的SAT求解器来计算.为了使协议的验证过程全自动, 我们给出了对任意协议的处理算法, 即给出一个协议, 如何具体生成相关的信息集合, 如何生成变量和所有的公理集. 我们此理论上已经开发出一个完全自动化的安全协议验证工具SPV (Security Protocol Verifier). 要验证的规范可以带有嵌套知识算子, 并且此工具是基于证明的, 而不是象别的很多方法那样是基于证伪的, 即找漏洞. 而且SPV直接对输入的协议进行处理, 不需要用户对协议理想化 (idealizations) 抽象后处理. 实验结果表明, 这种基于SAT的方法是高效的. 为了验证更多的性质, 我们的公理集中加入了一些新的特性, 如动态性, 使我们可以推导协议的每个执行步所得到的知识；还有秘密性, 我们在公理中加入那些处理智能体间共享秘密的公理. 而且, 我们对协议的运行环境进行了不同的假设, 提出了各种信息交换系统模型（Message-passing System）.本文的未来工作, 是进一步丰富这套公理模型, 从而可以处理更多更复杂的安全协议特性, 如匿名性, 非抵赖性等等. 以及在语义上进行深入研究讨论.