随着网络技术的应用逐步渗透到许多关键部门，以及电子商务的兴起与广泛应用，信息安全已变得日益重要。安全协议是信息安全的基础，但其正确性和安全性却不容乐观，已有的安全协议往往被证实并不如设计所期望的那样安全．即使不考虑与实现相关的协议缺陷和密码系统被成功破译的可能性，复杂的网络环境还是使得攻击者可利用安全协议自身的缺陷来实施各种各样的攻击．因此，安全协议是否能达到它所要求的安全目标是非常关键的问题。 对安全协议的分析和验证是保证所设计的协议满足其安全性的重要技术手段，而借助形式化的方法或工具分析安全协议是非常必要而且行之有效的．安全协议的形式化分析已有二十多年的历史，已逐渐成为安全协议研究的热点。近十几年来，世界各国学者对其进行了广泛和深入的研究，尤其是美国和欧洲的一些国家在这一关键领域投入了大量的研究经赞和力址．同时，安全协议设计和分析也引起了国内研究人员的高度重视．虽然安全协议形式化研究领域取得了可喜的成果，但尚有诸多问题亟待解决，譬如，如何精确刻画安全协议，如何扩充现在已经成热的理论或方法去研究更多的安全性质，如何使安全性质在统一的框架下进行分析和验证等等。 安全协议是一个典型的并发分布式系统，而进程演算是一个强有力的并发分布式系统建模工具，具有强大的描述能力和严格的语义，能够精确刻画安全协议中各个参与者之间的交互行为．利用进程演算对安全协议进行分析和验证时，既可以借鉴其作为代数模型的基本验证理论与方法，又可以使用其作为抽象程序设计语言的程序分析方法．然而，由于进程演算固有的缺乏数据结构支持的特点，难以建模主体拥有的知识以及知识推理，以至于只能分析很少的安全性质,另一方面，基于知识和信念的逻辑推理方法可以为协议消息和主体建模，但是缺乏推导主体行为的机制．而且，协议的理想化过程过于依赖分析者的直觉，其困难常常导致分析结论的错误．所以，我们将进程演算和知识推理二者实现优势互补，以进程演算为基础，嵌入消息知识推理系统，为安全协议建模和分析．本文的主要成果和创新如下： 1．本文详细探讨了安全协议形式化分析的各种方法，尤其是基于进程演算的各种分析手段，并做了两个实例研究：一是在对spi演算进行适当扩展的基础上分析了 Kerberos协议的认证性，二是以Applied π-演算为基础分析了iKP协议的认证性和匿名性。 2．以进程演算为基础，结合协议主体知识的逻辑推理以弥补进程演算固有的缺乏数据结构支持的特点，建立一个适合于安全协议形式化分析的一般模型GSPM,它可以精确刻画安全协议，在统一的框架下形式化描述和验证各种安全性质．GSPM 中的进程演算部分描述了协议参与主体的演化行为，逻辑部分使用了一系列推理规则推理主体的知识．嵌入的知识推理系统具有可扩展性，可以加入新的推理规则更深入地分析安全协议．此外，GSPM不为攻击者行为单独建模，既最大化了攻击者能力，又简化了协议的分析过程。 3．以GSPM为基础分析验证安全性质 (a)基于GSPM，定义了一步可达关系和多步可达关系两个概念，利用可达关系概念形式化地描述了安全协议的保密性，并以TMN协议为例作了实例研究． (b)在给出了GSPM的LTS操作语义的基础上，形式化地定义了安全协议的认证性，并以NSPK协议为例作了实例研究． (c)基于GSPM的变体GSPM，采用博弈思想形式化地定义了公平交换协议的非否认性和公平性，并以一种认证邮件机制-MD机制为例作了实例研究． (d)对其它安全性质的形式化描述进行了讨论． 4．在GSPM的变体GSPM+的基础上提出了一个环境敏感的抽象互模拟等价关系，形式化地定义了保密性和认证性，并做了简单的实例分析． 5．引入了符号化技术解决GSPM中等待输入消息时导致的无限分叉问题．在等待输入一个匹配项时，将环境能产生的消息项分成有限类，产生有限个替换，选择某个替换进行迁移，并把替换记录在迁移过程中，非常技巧性地将迁移过程中可能产生的无穷分叉变成了有限分叉．我们分别在以GSPM为基础的可达关系、LTS 和博弈语义中引入符号化技术，并以实例分析作了说明．符号化技术的采用为我们正在开发的自动验证工具奠定了基础．