【作者】 董玲；

【导师】 陈克非；

【作者基本信息】 上海交通大学 ， 计算机系统结构， 2008， 博士

【摘要】 密码协议的安全性研究是网络安全研究的主要热点。本论文主要研究了如何应用系统工程思想和形式化方法来分析和设计密码协议,取得的主要研究结果如下:1.将系统工程思想引入密码协议设计,结合前人的研究成果,提出了10条密码协议工程原则:5条安全需求分析原则,4条详细设计原则以及1条安全性证明原则。将密码协议设计看作密码协议工程,从协议设计的不同阶段给出原则,是帮助研究人员按系统工程思想进行密码协议设计的有益尝试。实例分析表明,这些原则不仅较为完备,而且可操作性强,能帮助研究人员明确协议设计背后的隐含假设,发现和避免协议设计中的漏洞,简化协议设计。2.首次提出基于信任的新鲜性标识符分析密码协议的安全性,给出了新鲜性原则:对每个通信参与主体而言,密码协议的安全性取决于发送或者接收的、包含自身已相信新鲜的新鲜性标识符的单向变换。该原则找到了一条快捷、有效的密码协议安全性分析方法,论文示例了20多个经典密码协议的分析结果,分析出的针对协议的攻击或者安全隐患有12个是以往没有指出过的。新鲜性原则的特点是:①能有效区分消息是否新鲜,安全性的分析独立于并发运行环境的具体形式化描述,也独立于攻击者能力的具体形式化描述;②基于该原则得到的分析结果能够证明正确协议的安全性,也能够分析出不安全协议存在的安全属性缺失,以及由该缺失直接构造攻击的结构。3.基于新鲜性原则,提出了基于逻辑推理的信任多集形式化分析方法。以Needham-Schroeder公钥认证协议为例,说明了该分析方法的有效性、严谨性和自动化实现的可能。另外,针对无线网络的开放性和数据包易失的特点,扩展了信任多集方法,能有效用于无线密码协议分析。4.证明了保证认证协议安全的充分必要条件,这些条件在计算模型下分别满足基于匹配对话和不可区分性的4个可证安全定义。5.提出了信任多集自动分析工具的总体框架,通过在2种不同开发环境下信任多集自动分析工具初步实现的比较,给出了信任多集自动分析工具的详细设计。正在开发的信任多集自动分析工具已成功实现了对若干密码协议的安全性分析。6.基于新鲜性原则和因果一致性的分布式逻辑时间,建立了信任多集形式化设计方法。构造了一个公钥认证协议,并证明了该协议达到了消息数和轮数的下限。更多还原

【Abstract】 The security research of cryptographic protocols is becoming one of the hottest reasearch spots in network security field. This dissertation mainly discusses how to analyze and design cryptographic protocols based on the idea of system engineering and formal methods. The main results that the author obtainted are as follows:1. Based on the idea of system engineering and the previous presented principles, we present and illustrate 10 cryptographic protocol engineering principles in three groups: 5 cryptographic protocol security requirement analysis principles, 4 detailed protocol design principles and 1 provable security principle. Cryptographic protocol engineering is a new notion introduced in this thesis for cryptographic protocol design, which is derived from software engineering idea. The idea is useful in that it can indicate implicit assumptions behind cryptographic protocol design, and present operational principles on uncovering these subtleties.2. A novel freshness principle based on trusted freshness component is presented: for each participant of a cryptographic protocol, the security of the protocol depends only on the sent or received one-way transformation of a message, which includes certain trusted freshness component. The freshness principle indicates an efficient and easy method to analyze the security of cryptographic protocols and the analysis results of 20 classical cryptographic protocols are illustrated while 12 possible attacks or flaws are new. The freshness principle has following characteristic: it could efficiently distinguish the freshness of the messages to avoid replay attacks and interleaving attacks etc., and the analysis procedure is independent of the concrete formalization of the protocol concurrent runs and the adversarys’ possible behaviors. The security analysis results based on the freshness principle can either establish the correctness of the protocol when it is in fact correct, or identify the absence of the security properties and the structure to construct attacks based on the absence.3. Based on the freshness principle, a belief multisets formalism is presented. We have shown the efficiency, rigorousness, automation possibility of the belief multisets formalism by illustrating it via the Needham-Schroeder public key protocol. With the open medium transmission and packet loss considerations in mind, we present an extensible belief multisets formalism including DOS-tolerant property and consistency property analysis that is suitable for wireless protocol analysis.4. Security goals are presented accurately, which are proved not only necessary but also substantial to guarantee the security adequacy of the cryptographic protocols to 4 security definitions under the computational model. These 4 definiitons are presented based on matching conversation definition and indistinguishability security definition.5. A general model for automation of the belief multisets fomalism is presented. Via the comparison of our two partial implementations of the automation of the belief multisets fomalism under the different development environments, a detail implementation approach is determined. The developing automation of the belief multisets fomalism has successfully analyzed several cryptographic protocols.6. Based on the freshness principle and the treatment of the distributed logic time causal consistency, a model for designing cryptographic protocols is also proposed. We exemplify the usability of the model via redesigning the Needham-Schroeder public-key protocol, and prove that the reconstructed challenge-response key exchange protocol achieves the lower bounds of three messages and three rounds.更多还原