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