【作者】 陈铁明；

【导师】 蔡家楣；

【作者基本信息】 浙江工业大学 ， 计算机应用技术， 2004， 硕士

【摘要】 保障网络通信安全的一个极其重要的环节是安全协议，安全协议的形式化分析方法已成为近年来安全领域研究的热点之一。同时，PKI体系作为一个强有力的网络安全保障系统已被广泛地应用于各种商业网络环境，各种基于PKI应用的复杂安全协议也成为研究和发展热门，其中以SSL协议的应用最为成功。目前，试图用简单的推理构造逻辑方法分析诸如SSL的复杂安全协议其效果不尽人意，因此，本文的研究重点就在于提出一种新的形式化分析思路来分析和设计复杂的安全协议。 复杂安全协议本质上就是由简单的协议模型不断进化而得，因此本文采用基于代数规范的方法提出一个安全协议的进化模型框架，安全协议的主体均可采用该框架得以形式化描述，并通过进化模型的扩展达到安全协议进化的目的。本文采用著名的信念逻辑GNY逻辑系统及其相关的形式化工具SPEARⅡ，以SSL协议为分析实例，详细阐述了从初始协议模型到各个进化协议模型的分析过程，并将最终的进化模型与SSL协议作比较，给出SSL协议的安全分析，同时在分析过程中以协议模型为基础设计了两个实用的安全认证方案。因此，本文提出的进化协议思路不仅有助于对复杂协议的分析，还不失为一种复杂协议的设计方法。另外，本文在使用GNY逻辑的分析过程中，提出三条实用的GNY扩展规则，而在文章最后，对基于攻击逻辑的安全协议验证方法作了初步研究，提出了将该协议攻击验证技术融入协议自动分析工具的设计框架。更多还原

【Abstract】 Security protocol is a very important role in securing network communication, and the formal analysis method for security protocol becomes one of the hottest research topics in security field. Meantime, PKI has been applied in various commercial network environments as a perfect security guarantee, and so many complex security protocols based on PKI application are also on hot way, in which SSL protocol is a most typical one. However, using formal method based on reasoning logic to analyze complex security protocols such as SSL is not so efficient at present. So, the research topic in this paper is to present a new analysis way based on formal method to analyze and design complex security protocols.It’s essential that complex security protocols can be obtained through the continues evolution of simple protocols, therefore, the Evolution Model Framework for security protocol based on algebraic specification is presented in this paper, the body of a security protocol can be formalized using this framework and the goal of a security protocol’s evolution can be attained by expanding this framework. In this paper, the belief logic system GNY and it’s related implementation tool SPEARII are utilized, SSL protocol is a focused instance, then the detailed analysis procedure from initial protocol model to various evolution protocol models is given, later the final evolution protocol model and SSL protocol are contrasted and thus the security analysis conclusion is drawn for SSL. During the analysis procedure two practical security authentication solutions are designed based on evolution protocol models. So, the evolution protocol model is not only useful to analyze complex protocols but also to design protocols. Furthermore, three expanded GNY logic rules are given during above analysis based on GNY, and at the end of this paper, security protocol formal verification based on attack logics is discussed and presented, a development framework of integrating such verification model into automated analysis tools such as SPEARII is shown finally.更多还原