基于strand空间模型的安全协议分析与设计方法研究

论文摘要

因特网因其开放的协议彻底改变了计算机网络,同时也带来了新的风险和威胁。保护计算机网络最好的方法就是使用快速的自动化程序阻止攻击者的入侵。手工的不能防止未知类型攻击的方式是不能起到充分保护的作用的。使用基于共享攻击信息以及机构间合作的主动安全管理的方法可以解决这个问题。安全区域协作是一个建立在可信区域相互合作和协同的框架,它能够保护系统免遭潜在的攻击并通过交换安全信息和区间合作来预报和响应攻击。在这种动态的强安全体系结构中,为了保护网络中传送的区域策略免受攻击,需要建立安全通信系统,密码算法和安全协议是其核心。然而,攻击一个成熟的密码算法的代价比攻击一个有缺陷的安全协议所需的代价要巨大的多,往往个人或小团体难以完成,安全协议往往是攻击者的首先攻击目标。因此,分析、设计安全有效的安全协议是计算机通讯领域中一个极为重要的研究课题。 安全协议是很多分布式系统安全的基础,它负责密钥分发和身份认证,安全协议自身的漏洞会对通信的安全造成严重的威胁。现有的许多协议在设计上普遍存在着某些安全缺陷,安全协议的形式化分析检验技术就成为目前研究的热点。但现有的各种方法主要用于分析某个具体的安全协议的安全性,而不是致力于在设计之初就确保协议的安全性。因此使用形式化方法指导安全协议的设计,对于满足复杂任务的密码协议有着重要的意义。 在形式化方法中,基于Strand空间模型的安全协议分析,可以利用该模型中包含的确切的因果关系信息,使对协议安全性质的证明十分简洁。认证检验是Thayer开发出的手工验证密码协议的方法,可以通过使用加密和随机数达到认证和新鲜性,同时他也提出了使用认证检验这种安全协议的形式化分析方法来指导安全协议设计的可能性,并对现有的一些协议作了再现。 本文通过对基于Strand空间模型理论的研究,提出围绕认证检验在安全通信或电子商务中建立具体情况下特定安全目标的协议,设计的过程既是通过strand空间和认证检验对可信主体证明的过程。 本文第四部分创建了ATSP（an Authentication Test-based Secure Protocol）作为利用认证检验技术设计安全协议的实例。首先确立明确的设计目标,即在一

论文目录

• 摘要
• ABSTRCT
• 1 绪论
• 1.1 计算机网络信息安全问题与安全协议
• 1.1.1 安全问题
• 1.1.2 安全协议
• 1.2 安全协议的安全性与形式化方法
• 1.2.1 安全协议的脆弱性
• 1.2.2 安全协议安全性分析与形式化方法
• 1.3 研究工作概要与论文安排
• 1.3.1 目前相关的工作
• 1.3.2 课题内容与特点Strand
• 2 Strand空间模型
• 2.1 消息项
• 2.2 Strand、Strand空间和Bundle
• 2.2.1 Strand和Strand空间
• 2.2.2 Bundle
• 2.3 利用Strand进行协议说明
• 2.4 入侵者模型
• 3 基于Strand空间模型的安全协议的分析与设计
• 3.1 可入侵密钥和安全密钥
• 3.2 认证检验
• 3.2.1 输出检验与输入检验
• 3.2.1.1 输出检验
• 3.2.1.2 输入检验
• 3.2.1.3 自发检验
• 3.2.2 利用输出检验的认证检验
• 3.2.3 利用输入检验的认证检验
• 3.3 认证检验证明协议的正确性
• 3.4 认证检验指导安全协议设计
• 3.4.1 安全协议设计原则
• 3.4.2 安全协议设计的形式描述语言
• 3.4.3 安全协议的基本假设
• 3.4.4 strand空间模型指导安全协议设计
• 4 基于strand空间的认证检验在安全协议设计中的应用
• 4.1 ATSP协议目标
• 4.1.1 协议参与者
• 4.1.2 协议目标
• 4.2 认证检验
• 4.2.1 strand空间
• 4.2.2 新鲜性
• 4.2.3 诚实理想
• 4.3 认证检验与协议设计
• 4.3.1 有效负荷和机密性
• 4.3.2 设计两方子协议
• 4.3.2.1 认证Ⅰ
• 4.3.2.2 完成不可否认性
• 4.3.2.3 完成认证Ⅱ
• 4.3.3 区分子协议
• 4.4 正确性
• 4.4.1 子协议的正确性
• 4.4.2 子协议的独立
• 4.5 三方协议
• 4.5.1 三角形消息结构
• 4.5.2 直线版本
• 4.5.3 ATSP协议应用
• 4.5.4 ATSP的三方目标
• 5 结束语
• 参考文献
• 致谢
• 攻读学位期间发表的学术论文目录