论文部分内容阅读
计算机网络中,安全协议为通信双方的信息交互提供安全保证,是计算机网络安全的基础.而当安全协议中存在安全漏洞时,会对信息安全产生重大威胁,造成数据泄露、身份被冒用等危害.因此,对于安全协议安全性的研究,历来都属于安全领域的重要研究方向.目前的安全性分析方法主要是通过协议形式化分析与验证来实现.形式化分析方法的理论体系大致可分为三类:模态逻辑技术、模型检测技术和定理证明技术.在不同类别的理论体系中,所使用的技术方法各有不同,对安全协议分析的侧重点也略有不同.对于每一种理论体系,研究者们也提出了不同的方法,以及针对经典方案的改进来提高形式化分析的准确性.对于复合协议,其主要问题是通过对多种现有可靠安全协议加以组合,构成新的协议并保持其安全性可靠.对于复合协议的安全性分析,也有异于普通的安全协议形式化分析.本文总结了各种类别中的主要分析方法,并比较了每种方法的优缺点,同时特别针对复合协议的安全性分析技术进行了概述.最后指出了形式化分析方法中需要解决的问题,以及下一步的研究方向.
In computer networks, security protocols provide security assurance for information exchange between two parties and are the basis of computer network security, while when security vulnerabilities exist in security protocols, they pose a serious threat to information security, causing data leakage and identity being fraudulent Therefore, the study of security protocols has always been an important research field in the field of security.At present, the security analysis methods are mainly realized through the formal analysis and verification of protocols.The theoretical system of formal analysis methods can be roughly divided There are three types of techniques: modal logic, model detection, and theorem proving techniques, which are different in the different types of theoretical systems and have a slightly different focus on security protocol analysis. Theoretical system, the researchers also put forward different methods and improve the accuracy of formal analysis in view of the improvement of the classical scheme.The main problem for the compound protocol is that by combining a variety of existing reliable security protocols to form a new Agreement and maintain its safety and reliability.For the security analysis of composite protocols, but also different from the normal security protocol Formal analysis.This paper summarizes the main analysis methods in each category and compares the advantages and disadvantages of each method.At the same time, it gives an overview of the security analysis techniques of composite protocols.Finally, it points out that the formal analysis methods need to be solved The problem, and the next research direction.