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

摘要

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

目录

文摘

英文文摘

原创性声明和关于论文使用授权的说明

1前言

2 Strand空间模型

3基于Strand空间模型的安全协议的分析与设计

4基于strand空间的认证检验在安全协议设计中的应用

5结束语

参考文献

致谢

攻读硕士期间发表的学术论文目录