安全协议及其BAN逻辑分析研究

【作者】 杨世平；

【导师】 李祥；

【作者基本信息】 贵州大学 ， 计算机软件与理论， 2007， 博士

【摘要】 随着计算机网络的广泛应用和各种应用领域的不断扩大，信息的安全问题成为大家关注的焦点。信息安全(Information Security)问题从某种程度上已成为制约计算机网络应用的一个瓶颈。传统的对信息的安全性处理是依赖于好的加解密算法来保证。但是，随着网络应用的深入，仅仅依赖一个好的加解密算法已经不能很好地解决信息的安全问题，它需要安全理论、安全措施和安全技术来保证。在这些信息安全的理论、措施和技术中，安全协议起着至关重要的作用。在实际应用中，人们需要可信的机制来为通信的各方进行身份认证和分发密钥，这就迫使人们研究和设计出了各种安全协议(Security Protocol)。然而事与愿违，已有的安全协议往往被证实并不如它们的设计者所期望的那样安全，开放的、复杂的网络环境使得攻击者可利用安全协议设计中的缺陷和漏洞来实施各种各样的攻击，从而非法获取网络资源，窃取非授权使用的信息，危及到网络的安全和应用。因此，安全协议自身的安全性成了网络安全的关键问题之一。考量和分析一个安全协议的安全性称为安全协议的分析。目前，使用最为广泛的安全协议分析方法是各种形式化分析方法，即采用各种形式化的语言或模型，为安全协议建立模型，并按照规定的假设、分析和验证规则，验证安全协议的安全性。本文以如何保障安全协议的安全性为切入点，研究和分析了与安全协议息息相关的密码学的诸多问题，例如，对称密码体制、公钥密码体制、椭圆曲线密码体制、数字签名等基本算法。进一步讨论了具有代表性的认证协议，密钥管理和分配的方法等。研究和分析了安全协议的非形式化分析的方法和形式化分析方法，重点是对BAN逻辑的分析和讨论，并利用BAN逻辑分析了部分认证协议。本文通过BAN逻辑的实例分析，说明了BAN逻辑在分析认证协议中具有积极的作用，发现了认证协议中一些原来没有发现的漏洞和冗余。但是，文中通过对两个认证协议的分析，指出了BAN逻辑在对中间人攻击和口令猜测攻击的安全协议分析中存在的缺陷，并对被分析的认证协议进行了改进。最后提出了基于安全协议的电子公文安全流转方案和基于安全协议的消息交换方案。将椭圆曲线密码体制引入到消息交换方案中，减少了消息交换中数字签名和密钥协商的计算量，也利用椭圆曲线离散对数的难解性来增强了消息交换的安全性。更多还原

【Abstract】 Nowadays, information security has already become a bottleneck that restricts applications of computer network. The security of information needs not only some good encryption algorithms but also some security theories, security measures and security technologies. In these theories, measures and technologies, the security protocol is playing very important role. In practical applications, people requires credible mechanism to verify identity of communicating parties and distribute keys. This forces people to have to research and design various security protocols. Generally speaking, security protocols are protocols that use cryptography to distribute keys and authenticate principals and data over a network and are a basic guarantee of secure communication through open and unprotected network. But proved by practice, design and analysis of security protocol has been recognized as much more difficult than initially thought and needs a rigorous formal approach to provide credible analysis guarantee. The complicated network environment makes the attackers to enable realizing various attacks by means of flaws and leaks of security protocols, illegally obtain the network resources and unauthorized information, and consequently endanger security and application of a network. Therefore, the security of security protocols has become one of the key problems of network security. To verify the security of security protocols is called security protocol analysis and a current research hot spot on network security. At present, most wildly used protocol verification method is various formal ones. By means of the formal mothods, we may make a model for security protocol using formal language or model and then verify its security according to assumptions and verification rules.How to ensure the security of security protocol is our starting point on network security in the paper. We research and analyze symmetric key cryptograph, public key cryptograph, elliptic curve cryptograph, and digital signature algorithms, etc. We further discuss some typical authentication protocols, key management and distribution methods, etc., and analyze informal methods and formal methods of security protocol, especially BAN logic. And then, we analyze a few authentication protocols with BAN logic.Some examples that have been analyzed with BAN, have shown that the BAN logic has the active effect in analyzing the authentication protocols, and finds some flaws and redundancy that were not discovered before. But through analyzing two authentication protocols, BAN logic defect in protocol analysis about man-in-the-middle attack and key guessing attack was pointed out, and the improved protocol against a man-in-the-middle attack and one against key guessing attack are given in the paper. Finally, we put forward three security schemes based on security protocal, the first for electronic official-documents interchange based on ECC, the second for message interchange based on ECC, and the last for message interchange signcrypting based on ECC. The elliptic curve cryptographic technique has been brought in message interchange schemes. The primary advantage that elliptic curve systems have over systems based on the multiplicative group of a finite field (and also over systems based on the intractability of integer factorization) is the absence of a subexponential-time algorithm that could find disaete logarithms in these groups. Consequently, we can use an elliptic curve group that is smaller in size while maintaining the same level of security. The result is smaller key sizes, bandwidth savings, and faster implementations. In other words, use of elliptic curve cryptographic techniques provide greater security using fewer bits, resulting in a protocol which requires low computational overhead, and thus, making it suitable for digital signature, key agreement and exchange and more secure and faster message interchange in network.更多还原