论文部分内容阅读
现代密码协议作为网络安全通信系统的核心技术，其重要性不言而喻。然而，如何分析密码协议的安全性，从而证明密码协议的有效性?如何设计密码协议，从而确保所设计协议的安全性?这些则都是需由密码协议形式化方法来解决的问题。密码协议的形式化方法作为密码协议分析和设计的理论基础，自Dolev和Yao的开创性工作以来，目前已有了较大的发展，形成了两大流派，其中典型的有StrandSpace模型理论和预言机模型理论等。然而，在如何应用抽象的形式化理论或方法来研究现行通信系统中大型、复杂并行系统的密码协议，发现其安全缺陷或证明其安全性?在如何扩展现有形式化理论，使之能够解决网络中出现的新的威胁?以及在如何应用形式化理论指导密码协议的设计等几个方面还有待进一步的研究。鉴于此，本文基于StrandSpace模型理论和预言机模型理论，针对上述三个方面的问题进行了深入的研究，并提出了一些有效的解决方案，得到了一些研究成果。论文的研究内容主要包括以下三个方面：
首先，研究了如何应用StrandSpace模型理论和预言机模型理论分析现行复杂系统中的密码协议，指出了这些密码协议存在的安全缺陷，并基于形式化理论分析的结果提出了对这些协议的改进方案，最后基于形式化理论论证了这些改进方案的安全性。本文所研究的密码协议具有普遍的理论意义和现实的应用意义。其中对于CCITTX.509认证协议及简单认证密钥交换算法(Diffie-Hellman密钥交换算法的一个变种)的研究具有普遍的理论意义。而对于基于SmartCard的密码认证协议及高效匿名拍卖协议的研究，则解决了网络中最新的电子商务应用问题，具有现实的应用意义。
第一，本文基于StrandSpace模型，在协议的保密性和协议的认证性两方面，对CCITTX.509认证协议进行了形式化分析，得出了BAN逻辑没有得到的协议保密性缺陷和相同的协议认证正确性缺陷，并给出了相应的攻击方法。在此基础上提出了一种改进的X.509认证协议，并采用StrandSpace模型形式化证明了该改进X.509协议的保密性和认证正确性。
第二，基于StrandSpace模型及AuthenticationTest方法形式化分析了基于SmartCard的密码认证协议，指出了该协议存在的安全缺陷，给出了相应的协议攻击手段。在此基础上提出了对该协议的改进方案，并基于AuthenticationTest方法形式化分析了改进方案，证明了改进方案的认证正确性。
第三，基于AuthenticationTest方法形式化分析了高效匿名拍卖协议的初始化阶段，指出了该协议初始化阶段存在的安全缺陷，并给出了对于协议初始化阶段的攻击手段，该攻击将使得后续的拍卖协议失效。在此基础上提出了一种改进的初始化协议以防止类似的攻击，并且基于StrandSpace模型理论及AuthenticationTest方法形式化分析了改进的初始化拍卖协议，证明了该改进的初始化协议中竟拍者和拍卖人之间的安全认证特性，从而保证了整个高效匿名拍卖协议的安全有效性。
第四，简单认证密钥交换算法作为Diffie-Hellman密钥交换算法的一个变种，通过增加两消息来防止中间人攻击，从而保证通信双方可靠地协商秘密会话密钥。然而，该算法却存在着一些安全缺陷。本文在分析该算法及相关改进算法的基础上，提出了一种新型增强简单认证密钥交换算法以克服这些安全缺陷。同时在已有预言机模型的基础上，给出了增强的语言机模型，并基于该增强的预言机模型，形式化分析了新型简单认证密钥交换算法，证明了该新型增强算法具备抗密码猜测攻击的能力，并具有完美的前向机密性。
其次，对于网络中新出现的协议攻击——拒绝服务攻击，目前为止还没有一种有效的形式化分析方法可以用来分析安全通信协议中的该类攻击。本文提出了一种新型形式化方法用以分析密码协议的拒绝服务攻击，以确定通信协议是否具有抵抗拒绝服务攻击的能力。本文首先应用赋权图的概念扩展StrandSpace模型，接着引入fail-stop协议的概念，由此提出两类DOStests(拒绝服务测试)方法，并基于两类DOStests提出了密码协议拒绝服务分析的新型形式化方法。最后，选取四个具有普遍意义的示例协议，即TCP三次握手协议，Intemet密钥交换协议(IKE)，高效抗DOS攻击安全密钥交换协议(JFK)和抗DOS攻击IKE协议，应用本文提出的新型形式化方法进行了协议分析，从而证明前两个协议易受DOS攻击，而后两个协议具备抗DOS攻击的能力。
最后，基于AuthenticationTest方法研究了密码协议的形式化设计方法，设计出了高效安全Internet密钥交换(ESIKE)协议。首先鉴于IKE协议中存在的一些安全缺陷，确定了ESIKE协议的安全目标。然后根据协议所需实现的安全目标，基于AuthenticationTest方法一步一步地完成了整个协议的设计。最后基于StrandSpace模型理论和AuthenticationTest方法形式化证明了ESIKE达到了所需的安全设计目标。ESIKE协议克服了IKE协议中存在的安全缺陷，同时提供对于会话密钥及安全关联SA的安全协商，提供了对于通信端点的身份保护，并且实现了协议发起者和响应者间的双向认证。该协议仅需三条消息，其实现更加简单高效。