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