【作者】 石曙东；

【导师】 李芝棠；

【作者基本信息】 华中科技大学 ， 计算机系统结构， 2009， 博士

【摘要】 安全协议是建造网络安全环境的重要基石,是保证网络安全的核心技术。设计和证明安全协议自身的正确性和安全性,成为网络安全的基础。形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法,对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击,但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善,存在一定的局限性,不能分析和验证某些类型安全协议的安全性:有些只能分析安全协议的不安全性,不能给出协议安全性的精确证明。在总结安全协议现存各种缺陷的基础上,根据缺陷产生各种原因将缺陷分为:过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为:重放消息型攻击、猜测口令型攻击、分析密码型攻击、并行会话型攻击、格式缺陷型攻击和身份绑定型攻击等六类。Burrows,Abadi和Needham提出的BAN逻辑开创了用逻辑化方法分析安全协议安全性的新纪元。由于该方法是对现实协议分析方法的抽象,逻辑处理的符号集是对现实具体协议的抽象;其初始假设、断言集合等均是从现实世界中抽象出来的要素。因此,其狭窄的符号集合定义也就决定了该方法存在不能分析某些类型协议安全性的缺陷,如:不能发现由于时间同步问题而导致的协议缺陷。另外使用BAN逻辑对安全协议分析时,很多初始假设是不合理的,如消息不可伪造假设就非常不合理,这些假设的不合理,妨碍了该分析方法的正确应用。BAN逻辑还存在非严谨的理想化步骤缺陷;语义不清晰缺陷;非严密的环境模型缺陷和无法有效预测对协议存在的攻击等缺陷。1995年由Raiashekar Kailar提出的Kailar逻辑主要用于描述和分析电子商务协议,但是它只能分析电子商务协议的可追究性,无法分析电子商务协议的另一个重要特性——公平性。与BAN逻辑一样,使用Kailar逻辑分析协议之前同样需要引入一些初始假设,而初始假设的引入仍然是一个非形式化的过程,具有一定的人为性,其不准确会导致安全协议分析的失败。另外,用Kailar逻辑解释协议语义时,只能解释签名的明文消息,这样限制了其使用范围,对某些安全协议不能分析。针对BAN类逻辑和Kailar逻辑的弱点,设计了一种新的安全协议分析逻辑CPL(Cryptographic Protocols Logic),CPL不但可用于分析协议的安全性,还可用来设计安全协议,即CPL逻辑把分析和设计安全协议纳入同一个逻辑体系中,消除了用不同方法分别设计和分析安全协议,将导致结果不一致性的缺陷,同时也简化了分析和设计安全协议时对初始条件和安全协议最终目标分别进行形式化的过程和步骤,提高了分析和设计安全协议的效率。定义了CPL逻辑的基本符号、给出了CPL逻辑用于分析协议安全性的六类二十五条逻辑分析规则和用于设计安全协议的二十九条逻辑设计规则。分析规则和设计规则可分别用于安全协议的分析和安全协议的设计。给出了基于Kripke的CPL逻辑的语义,并利用逻辑语义对CPL系统自身的正确性进行了详细证明。运用新逻辑的分析规则和协议运行的初始条件以及安全协议的执行步骤分析安全协议的安全性。运用新逻辑的设计规则和协议运行的初始条件以及协议的最终目标设计出满足安全要求的安全协议。使用新逻辑分析了两个不同类型协议的安全性——密钥建立协议和身份认证协议。更多还原

【Abstract】 Working as a kind of kernel technology for the secure network communication, the security protocols are the foundation in building up a safe internet environment. Therefore, the correctness and security of protocols play a crucial role in network environment. However, it remains to be solved on the security and design of the protocols to better meet the demands of the safety. A formalized method, thereafter, has been proved to be effective in analyzing and testing verification of the protocols, which so far has become a focus in the field of formal study.Although the formal method has succeeded in finding flaws and attacks of many security protocols, it still suffers from lots of problems, such as the faultiness of the formal method itself, which can not suit the verification of some security protocols. On the other hand, some others can only presume the insecurity of cryptographic protocols rather than the credible verification of security objectives.In terms of the causes and attacking methods accordingly, there are 7 types of deficiencies, i.e. protocol deficiency, password/key deficiency, outdated information deficiency, internal protocol deficiency, parallel communication deficiency, code system deficiency and other deficiencies. In the meanwhile, 6 types of attacks in security protocols have been classified: information-reissuing attacking, presuming attacking, code-analyzing attacking, parallel communication attacking, type deficiency attacking and binding attacking.BAN logic, the foundation of the logic analysis, put forward by Burrow, Abadi and Needham, forms the landmark in analyzing security protocols. However, the narrow definition of symbol muster proves that there are some deficiencies which can not be analyzed, for the reasoning method of BAN logic is as a matter of fact abstracted from the real protocol analysis method and the symbol cluster of the logic process is abstracted from the real protocols. For example, it can not analyze the protocol deficiency by time synchronization, or it can not analyze the protocol with special password conversion method, etc. Besides, many illogic initial presumptions exist in BAN logic, which limits seriously the method into practice. Take the presumption that the news can not be forged as an example. Finally, some other deficiencies exist in BAN logic: non- standard idealized process deficiency, reasoning rule deficiency, lacking-in-clear- semantic deficiency, lacking-in-environment-model deficiency and lacking-in-effective-exploring -attacking deficiency, etcAs an important logic in studying and analyzing electronic business protocols, Kailar logic has flaws as follows: 1) Kailar logic can only study the pursuitability rather than the impartiality of the protocol; 2) As some presumptions will be introduced before the reasoning of Kailar logic, which is a non-standard process, improper introduction of presumption, therefore, will lead to the failure of protocol analysis; 3) The applicable range could be restricted when Kailar logic can only explain those signatory explicit information.To sum up, a new logic of security protocol analysis---CPL, that is, Cryptographic Protocols Logic---has been designed, which can not only analyze but also design the security protocols. Thus, the new logic integrates the analysis and design into one logic frame, avoiding the potential disagreement owing to the different methods in analyzing and designing, simplifying the steps of initialized conditions and objectives in the formalized process of analyzing and designing security protocol, improving the efficiency of the analyzing and designing. CPL gives the primary symbols, reasoning and composition rules, among of which, the two rules can be used in analyzing and designing respectively in security protocols. The analysis process of the security protocols can test the safety of the protocol by way of the reasoning rules and initialized conditions and executive steps in analyzing the security of the protocols. The design process can design the security protocols by way of the composition rules and initialized conditions and objectives in protocol operation. Two kinds of protocols, i.e. password protocols and identification protocols have been illustrated on the basis of the new logic.更多还原