安全协议是一种在不安全的公共网络上为完成某种不可泄漏的信息交换而建立的通信协议．所谓网络的不安全性，是指黑客的存在，他可以监听，阻止和伪造正在网上传输的信息，他们的标准模型称为Dolev-Yao模型[1].虽然安全协议使用密码系统来确保其安全性，但是，他们中的漏洞很多时候是由于其设计中可能的逻辑错误造成，而不是由于其加密算法不可靠(如[2]就是一个典型的例子)．并且安全协议验证问题是个公认的难题．因此，如何开发出相应的协议验证工具，使得协议的潜在攻击能自动地被发现，或者某些安全的属性可以被证明在无穷会话下都成立，是个研究的热点． 安全协议的自动验证问题，有两种方法，一种是基于证伪的，另一种是证明的．证伪的方法先假定一个协议的有穷会话，然后在此会话中搜索潜在的攻击漏洞，这种方法无法证明某些安全性质在协议的无穷会话中成立；证明的方法则弥补这个缺陷，它着眼于证明某些安全属性在协议的任意无穷会话中都成立．基于证伪的方法有很多相应的自动验证工具，而证明的方法也很多，但是他们比较难自动化实现，而且他们不适合验证大规模的协议如SET purchasephase protocol；另外一个缺陷就是他们无法验证BAN逻辑[3]中着重提出的认知规范，如“Alice知道Bob知道Alice说过某些信息”． 本文的内容是提出一种基于本地会话的安全协议验证逻辑LLS(Logic ofLocal Seesions)和相应的自动验证算法及工具简介．LLS基于安全协议的证明，并且着眼于上述的两个问题的解决．它可以实现协议的完全自动化验证并可以验证复杂协议的相关安全属性． 本文的主要工作如下： ●我们首先定义一个描述安全协议分析的加密信息交换(CryptographicMessage Exchange)模型并结合Dolev-Yao模型，探讨了里面的一些相应的重要性质．在此基础上，我们将给出了一个称为“实例化空间(InstantiationSpace)”的安全协议验证逻辑的语义模型． ●在实例化空间(Instantiation Space)语义模型基础上，我们提出了一系列与安全属性相关的LLS验证公理，并证明他们在此语义模型下的正确性．这些公理比现有的一些验证逻辑，如[4]中的谓词source以及[5]中的challenge-response axiom schema和send-receive axiom schema，能描述更一般的情形(详见备注5.1和5.2)． ●为了验证多层的认知规范，我们引入了可观察理论(Observation Theory)．这是一个符号化的Kripke模型，而且在这个理论基础上，多层的认知规范问题可以很方便地转化成SAT处理，为验证协议的多层认知规范提供了一个简洁和方便的符号化算法验证途径．我们还进一步研究了分布式知识(Distributed Knowledge)，公共知识Common Knowledge)等等的基于SAT的算法． ●由于本文的逻辑系统在算法上的可行性，对应的工具SPV(Security Pro-tocol Verifier)已经开发成功，并且可以验证复杂的协议．由于在此语义基础上的公理集是纯命题逻辑的，且所需要的验证目标可以很方便地转化成可满足性问题(SAT)，从而可以利用工业上快速高效的SAT求解器实现．使用SPV，我们可以高效验证复杂的包括工业级的安全协议性质，验证的规范包括在CAPSL (Common Authentication Protocol Specifica-tion Language(CAPSL)，http：//www．csl．sri．com/users/millen/eapsl/)中的如“PRECEDES P：Q | N，M”的规范，以及各种单层和多层的认知规范，如单层规范“Bob知道Alice说过某些消息”和多层规范“Alice知道Bob知道Alice说过某些信息”。