一种分析和设计安全协议的新逻辑

论文摘要

安全协议是一种面向应用层的协议,它为通信的实体打上包装,穿上盔甲,防止攻击者对敏感数据进行窃取,保证通信内容的完整性。不同的应用需求对安全协议的设计也提出了新的要求,如组通信、匿名通信、安全多方计算、不可抵赖的签名、盲签名、群盲签名和数字现金等安全技术都要依靠安全协议来实现,所以安全协议的安全性显得特别重要。 随着信息技术的发展,信息安全成为人们普遍关心的话题。人们已经逐渐习惯于在网上进行办公、交流,在网上进行着各种商品的交易,因此网络安全问题是当今的一个研究热点。怎样在不安全的环境中进行秘密通信?这个问题主要通过安全协议来解决,所以安全协议是网络安全成败的关键所在。 本文在分析了安全协议分析的现状和安全协议设计的现状的基础上,提出了一种可以用来分析和设计安全协议的新逻辑,并结合串空间模型来证明了新逻辑的正确性。最后以几个比较有代表性的例子来说明新逻辑的具体应用。具体来说,本文取得了下面一些成果: (1) 给出了新逻辑的构成,包括新逻辑的符号、新逻辑的推理规则和新逻辑的合成规则。其中推理规则是用来分析安全协议的,主要看安全协议能否达到最终目标,而合成规则是用来对安全协议进行设计的。 (2) 给出了新逻辑的语义。串空间模型是安全协议分析的一种重要工具,它具有良好的语义,但其分析过程难度较大。新逻辑分析安全协议的过程比较容易操作,但逻辑本身的语义不是很清晰。本文把新逻辑和串空间模型结合起来,给出了新逻辑的串空间语义,从而证明了新逻辑的正确性。 (3) 运用新逻辑来分析安全协议。用新逻辑的推理规则结合安全协议执行的初始条件以及安全协议执行的步骤,分析安全协议是否能达到目标,如果不能,那说明安全协议是存在缺陷或者漏洞的。 (4) 运用新逻辑来设计安全协议。从安全协议的目标出发,运用合成规则可以把安全协议要达到的目标分成许多子目标,然后分别考察各个子目标,直到各个子目标都满足为止。最后综合设计的整个过程给出安全协议的形式化描述。 (5) 新逻辑将安全协议的分析和设计过程纳入一个框架中进行,消除了用不同的方法来分析和设计安全协议可能导致的不一致性。

论文目录

• 第1章 绪论
• 1.1 安全协议研究的意义
• 1.2 安全协议的形式化分析和设计现状
• 1.2.1 安全协议的形式化分析现状
• 1.2.2 安全协议的形式化设计现状
• 1.3 安全协议的形式化分析和设计中存在的问题
• 1.4 本文的基本结构
• 第2章 基础知识
• 2.1 基本概念
• 2.2 安全协议的分类
• 2.2.1 密钥交换协议
• 2.2.2 认证协议
• 2.2.3 认证和密钥交换协议
• 2.2.4 电子商务协议
• 2.3 分析安全协议的方法
• 2.3.1 基于逻辑推理的分析方法
• 2.3.2 基于攻击结构的分析方法
• 2.3.3 基于证明结构的分析方法
• 2.4 设计安全协议的方法
• 2.4.1 Heintze-Tygar模型
• 2.4.2 Buttyan-Staaman模型
• 2.4.3 Rudolph抽象模型
• 2.4.4 Guttman-Thayer的认证测试方法
• 第3章 分析和设计安全协议的新逻辑
• 3.1 新逻辑的基本符号
• 3.2 新逻辑的推理规则
• 3.2.1 消息发送规则
• 3.2.2 随机数验证规则
• 3.2.3 仲裁规则
• 3.2.4 信任规则
• 3.2.5 消息接收规则
• 3.2.6 新鲜性规则
• 3.2.7 密钥对称规则
• 3.2.8 秘密对称规则
• 3.2.9 合理性规则
• 3.3 新逻辑的合成规则
• 3.3.1 几个定理
• 3.3.2 新逻辑的合成规则
• 3.4 分析和设计安全协议的步骤
• 3.4.1 分析协议的主要步骤
• 3.4.2 设计协议的主要步骤
• 第4章 分析和设计安全协议的新逻辑的语义
• 4.1 串空间模型的介绍
• 4.1.1 术语（term）和子术语（subterm）
• 4.1.2 strand、strandspace和bundle
• 4.1.3 攻击者的迹
• 4.2 新逻辑的串空间语义
• 4.2.1 基本语句的语义
• 4.2.2 几个公理
• 4.2.3 规则的证明
• 4.3 新逻辑与相关逻辑的比较
• 第5章 分析和设计安全协议的新逻辑的应用
• 5.1 Needham-Schroeder对称密钥协议的分析与设计
• 5.1.1 Needham-Schroeder对称密钥协议的描述
• 5.1.2 Needham-Schroeder对称密钥协议的分析
• 5.1.3 Needham-Schroeder对称密钥协议的重新设计
• 5.1.4 重新设计后的Needham-Schroeder对称密钥协议的分析
• 5.2 Denning-Sacco密钥分配协议的分析与设计
• 5.2.1 Denning-Sacco密钥分配协议描述
• 5.2.2 Denning-Sacco密钥分配协议的分析
• 5.2.3 Denning-Sacco密钥分配协议的重新设计
• 5.2.4 重新设计后的Denning-Sacco密钥分配协议的分析
• 结论
• 致谢
• 参考文献
• 攻读博士学位期间发表的论文及科研成果