【作者】 谢鸿波；

【导师】 周明天；

【作者基本信息】 电子科技大学 ， 计算机应用技术， 2011， 博士

【摘要】 计算机网络正以惊人的速度向各个领域渗透,其中的安全问题也变得越来越突出和复杂,解决安全问题对许多网络应用来说已是头等大事。从目前解决安全问题的方式来看,安全协议是解决网络安全问题最有效的手段之一。如何保证安全协议的安全性是安全协议研究领域的一个关键问题。为了保证和验证安全协议的安全性,研究人员提出了形式化的方法。经过二十多年的发展,安全协议的形式化方法得到了快速的发展和广泛的应用,已经成为公认的,在安全协议验证和设计领域最为合理、有效的方法。形式化方法通过建立科学的理论模型,对安全协议进行严格的数学和逻辑推导,以此来证明安全协议的安全性或指出安全协议中存在的安全缺陷;同时,形式化方法还可用来指导安全协议的设计。虽然形式化方法已经成功地发现了许多安全协议的漏洞和攻击,但是,这些方法仍然存在很多问题。通过综合分析这些方法,我们发现,现有分析方法中有两个固有缺陷:一是没有明确的形式化的方法来统一描述多种安全属性;二是缺乏一般化的形式语言模型作为分析安全协议的统一框架。针对上述两个固有缺陷,我们从三个层面逐步深入地进行了研究:首先,我们深入研究了三类典型且重要的形式化分析方法:类BAN逻辑、串空间、SPI演算,分析了他们的固有缺陷,有效地改进了他们的部分缺陷。其次,我们提出了一种用有向图来描述协议运行的分析方法,该方法部分解决了目前协议分析方法共性问题中的第二个固有缺陷。最后,我们提出了一个安全协议的统一分析框架,在更高的抽象层次上对安全协议运行和安全属性及其验证方法进行形式化建模,并在这个框架指导下,基于符号迹的方法设计了一种新的协议分析方法,实例分析表明该方法是有效的。我们提出的安全协议统一分析框架是解决目前安全协议分析方法两个固有缺陷的一次有意义的尝试,取得了一定的科研成果。本文的主要创新点如下:(1)改进类BAN逻辑在“理想化协议”步骤和单调性信任关系方面的缺陷,提出了基于消息唯一起源的动态逻辑方法。通过消息唯一起源的概念,解决了“相信事情的发生”和“相信事情的真实性”两种不同信任的区别,在此基础上建立了动态逻辑方法。(2)定义了新的类BAN逻辑语义模型,分析了类BAN逻辑的本质缺陷。该模型定义了“可能世界”及“可达关系”的概念。在这种模态逻辑框架下,我们给出了类BAN逻辑的真值赋值函数。从理论上证明了类BAN逻辑的逻辑语义缺陷是不可逾越的。(3)提出了安全属性的统一形式化描述方法,尝试用匹配关系来描述安全属性。在研究过程中,我们对此做了进一步的改进,安全属性被最终定义为:实体的时序消息与属性消息之间的推导关系。该定义脱离具体协议,是对安全属性的抽象建模,因此,更具有普适性。(4)将进程演算与实体消息推理结合起来,采用匹配关系来描述安全属性,提出了组合分析方法。该方法一方面弥补了进程演算缺乏数据结构来表示实体知识的缺陷,另一方面明确指出了在符号迹的分析过程中,如何及何时进行带符号的消息推理。由于采用了与协议无关的安全属性形式化描述方法,该方法扩展性很强。(5)提出了安全协议有向图分析法,部分解决了当前分析方法在协议运行的形式化建模方面的缺陷。该方法将协议规范中的每个协议步骤分解为有序动作序列,给出协议的有向图生成规则以及能够准确地跟踪协议消息的多种构造途径的消息构造逆向搜索算法。(6)提出“安全属性建模+协议运行建模”模式的统一分析框架。在统一框架的基础上,采用时序消息的推导关系来描述安全属性,为符号迹方法增加时间概念和基于时间的消息推理规则,从而有效地构造了基于符号迹的安全协议分析方法。这种统一分析框架对于安全协议的设计和分析方法的设计具有十分重要的意义。更多还原

【Abstract】 The computer network is penetrating into all kinds of realm, this makes the security problem becomes more and more outstanding and complicated. Addressing security problems for many network applications is already the major event. Judging from the current solution to security problems, the security protocol is one of the most effective means to resolve the network security problems. How to analyze the security protocols to ensure their safety and validity is one of the key problems should be solved by formal methods for security protocols. After developing for more than twenty years, the formal method of security protocols has been rapid development and wide application, and accepted as the most effective and reasonable method in the field of security protocol verification. The formal method builds up the scientific theory model to carry out the strict mathematics and logic on security protocols to verify their security or point out their security flaws. Meanwhile, the formal method can be used to guide the design of security protocols.Although the formal methods have been succeeded in finding flaws and attacks of many security protocols, they still suffer from lots of problems. By comprehensive analysis of these methods, we have found two inherence drawbacks: do not unite the description of the security property with a clear formal method; lack of a more generalized formal language used as the unified framework to analyze security protocols.Aiming at the above-mentioned two inherent drawbacks, we gradually carry out the study from three levels: first of all, we in-depth study three kinds of typical and important formal methods: BAN-like logic, strand space, SPI calculus, analyze their inherent drawbacks, and effectively improve their partial drawbacks. Secondly, we present a method based on directed graph. This method partially solved the second inherent drawback. Finally, we put forward a unified framework to analyze the security protocol. This method models the protocol run, the security property and its verification at a high-level logic abstraction. Guided by this framework, we also design a new analysis method based on symbolic trace method. Examples show that this method is effective.The unified framework we presented in this dissertation is a significative attempt to solve the two inherent drawbacks of current security protocols. The main innovations are as follows:1. In order to overcome the flows of BAN-like logics in their“idealization protocol”step and monotony trust relationship, we present a dynamic logic based on the concept of MUO (Message Unique Origin). The concept of MUO resolves the difference between“believe the occurrence of the event”and“believe the truth of the event”, based on this, a dynamic logic is built up.2. Proposing a new semantic model to analyze the syntax flow of BAN-like logics. This model defines the possible worlds and their relationships of BAN-like logic, and under this modal logic frame, evaluation function is presented. We theoretically prove that the logic semantic flow of BAN-like logic is insurmountable.3. Proposing the unified formal method to description the security property, we attempt to use match relationship to depict the security property. But in the research process, we have made the improvement regarding this, and then the security property is finally defined as the deduction relationship between the messages based on time and the property messages. This definition is separated from the concrete protocol, therefore, has the universality.4. Proposing a combined analysis model which uses the matching relationship to depict security properties. This model combines the process calculus and the message deduction relationship. On the one hand, the method makes up the lack of the data structure in process calculus; on the other hand, the method makes it clear that how and when to carry out the symbolic message deduction.5. Proposing a directed-graph-based method to analyze security protocols, this preliminarily solves the flows in formally modeling the security protocol. This method decomposes each protocol step into the sequence of actions, and then defines the rules to generate the directed graph, as well as the converse-searching algorithm which can accurately tracks the ways to construct the protocol messages.6. Proposing a unified framework based on the pattern of“security property modeling + protocol run modeling”. We use time-based message deduction relationship to depict the security properties, and add time concept and time-based message reasoning rules to symbolic trace method, thus we effectively construct the symbolic-trace-based method to analyze security protocols. The unified framework is of great significance for the design of security protocols, as well as the design of the analysis method.更多还原