本文为多智能体系统定义了一个称之为知识结构的逻辑框架，来进行智能体的知识推理.在知识推理过程中，使用”变量忘记”(VariableForgetting)来作为基本操作，并证明算法上可以用可满足性求解器来(SATsolver)实现.在我们的框架中，我们定义了智能体的可观察变量和最弱充分条件这两个概念.并证明了给定一个背景知识库△，和一组可观察变量Oi，对于每个智能体i来说，”i知道一个事实”可以定义为在背景知识库△下，i在Oi上的最弱充分条件.并对多智能体系统中嵌套知识的验证进行了讨论，随后将把此理论应用于安全协议验证。 基于近年来网络的发展与运用，使得网络安全问题日益引起人们的关注。在网络信息交互中，各种安全服务都是基于安全协议之上的，这就使得安全协议的地位更是十分重要，如何验证安全协议的安全性自然也就得到了很大的关注。过去数十年中，所采用的安全协议大多数却并不那么安全，在安全协议的形式化验证逻辑出现以前，安全协议的设计很容易出现漏洞，其中一个很重要的原因是，没有完善的协议正确性的概念，以及没有一个简单实用的逻辑来验证安全协议的正确性。 基于以上，本人已经实现了可以自动进行安全协议验证和分析的工具：SPV。SPV协议描述语言定义的初衷是尽量简单，即接近协议的文字描述，并参考当今其它安全协议验证工具的描述语言，如FDR的Casper。现今，安全协议验证的工具有很多，各有各的长处和缺点，主要可分为使用模型检测方法，定理证明方法和以上两种方式的结合。本工具SPV是面向证明的，且可自动实现，是一个目前比较强大的安全协议验证工具。