【作者】 白云莉；

【导师】 叶新铭；

【作者基本信息】 内蒙古大学 ， 计算机应用技术， 2013， 博士

【摘要】 随着计算机网络的迅速发展,信息通信的安全问题变得越来越突出,越来越复杂,解决安全问题对许多网络应用来说具有重要意义。目前,网络通信安全问题的解决方案中,安全协议是最有效的手段之一。由于网络本身的开放性,使得网络中存在着各种安全威胁,攻击者可以采用多种方式对安全协议进行攻击,破坏其安全属性。分析安全协议中可能存在的缺陷很难完全由人工来识别,因此,需要借助形式化的分析方法和工具来完成。安全协议的形式化分析过程包含安全协议系统建模、安全属性验证、以及攻击序列生成等。本文通过分析安全协议模型中攻击者的“任意”性行为和协议的多次并发会话问题,提出了一种改进的攻击者模型和多并发会话划分分析方法。针对安全属性验证和攻击序列生成问题,采用安全属性违背事件对不安全状态进行分类描述,提出基于安全属性违背事件生成攻击序列的两种方法：状态空间搜索法和on-the-fly生成方法。基于安全属性违背事件生成攻击序列的方法能够有效地控制搜索范围,提高搜索效率。最后通过分析安全协议中的数据特征,提取能够构成攻击的攻击策略,并依据攻击策略确定攻击目的,构建基于攻击目的的模型,选择生成攻击序列,有效地削减安全协议模型检测的状态空间。本文的贡献和创新性工作如下：(1)提出安全协议模型的多并发会话划分分析方法针对带有攻击者模型的安全协议形式化模型的复杂运行特点,提出一种改进的攻击者模型。通过对Dolev-Yao攻击者模型进行分析,将攻击者的功能划分为分解和合成两个前后阶段。同时,分析带有攻击者的安全协议形式化模型时,往往需要考虑多次并发会话的情况下攻击是否成功的情况。文本针对这一特点,通过会话配置和会话顺序的设定,提出多并发会话划分分析方法,一次分析一种并发情况,能够有效地划分并削减模型验证的状态空间。(2)提出基于安全属性违背事件的安全协议攻击序列生成方法针对攻击序列生成需求,定义面向安全协议攻击序列生成的CP-nets模型(Attack Trace Generation Oriented CP-nets,ATG-CPN)。依据安全协议规范和模型的特点,给出安全属性的形式化定义,并将攻击状态采用安全属性违背事件进行分类描述。提出基于ATG-CPN模型的状态空间搜索方法,生成到达攻击状态的攻击序列,减少了状态空间中搜索的状态数,避免生成虚假攻击。同时提出基于ATGx-CPN模型的on-the-fly攻击序列生成方法,该方法不需要对整个状态空间进行广度或深度搜索,基于部分状态空间生成有效的攻击序列。(3)提出一种基于攻击策略的攻击序列选择生成方法利用攻击序列生成方法能够得到大量的攻击序列,为集中有限的资源对安全协议系统存在的攻击序列实施重点分析,需要进一步确定依据攻击策略的攻击事件,选择生成攻击序列,使生成的有限攻击序列充分覆盖攻击目的。更多还原

【Abstract】 With the rapid development of the Internet, and increasing attention to the security of communication system, security protocols are widely deployed in the Internet. As the increasingly attacking capabilities and complexity of the applications, the design and analysis of security protocols are difficult to achieve. Model checking and attack trace generation method are major technologies to validate the correctness of security protocol.The Security protocol analysis and validation include security protocol modeling, attack trace generation and selection. Major causes of complexity of security protocol execution are resulted by the Dolev-Yao based attacker model and protocol multi concurrent sessions. A new improved attacker model is introduced. A new session configuration based dividing analysis method is effectively controlled the number of concurrent session. Attack states are characterized by security properties voilation events in the non secure states. Two attack sequence generation approach based on security properties voilation events are proposed:state exploration method and on-the-fly generation method. The security properties voilation events based attack sequence generation approach can effectively control the exploration scope and improve efficiency. Finally, by analyzing the data features of the security protocols, extract the attack tactics capable of form a successful attack. Based on attak tactics, modeling attack purpose and generating attack traces generally can reduce the workload of searching the state space.The main contributions of this dissertation are as follows:(1) A new multi concurrent session partition analysis method for security protocol model is presented.We proposed a new improved attacker model without reduce the capability of the Dolev-Yao attacker. Attacker’s function is divided into the decomposition and synthesis of two front and rear stages. Formal analysis of security protocol with an attacker needs to consider whether the attack was successful in the case of multiple concurrent sessions. By setting session configuration and session sequence, we proposed a multiple concurrent sessions partition analysis method, which is effectively reduce the state space of the model checking.(2) New attack sequence generation methods based on the security property voilation events are proposed.Attack Trace Generation Oriented CP-nets (ATG-CPN) is formally defined to model the security protocol with an attacker. Formal definition of security properties, including confidentiality property and authencation property, are given according to the security specification and formal model. Attack states are characterized by security property voilation events. Based on ATG-CPN models and security property voilation events, an attack sequence generation method is proposed. This novel CP-nets model based attack sequence generation approach improves the error coverage and avoids generating false attacks. A new CP-nets model based On-the-fly attack sequence generation method is also proposed, which does not need to explore the entire state space, so can effectively generate attack sequences.(3) A method of attack tactics based attack sequence selection method is presented.Using attack sequence generation method may generate a lot of attack sequences, to fit the model checking demand, a new attack tactics based attack sequence selection method is given. The limited attack sequences obtained after selection process meet coverage of attack trace generation purposes.更多还原