随着计算机网络的迅速发展,信息通信的安全问题变得越来越突出,越来越复杂,解决安全问题对许多网络应用来说具有重要意义。目前,网络通信安全问题的解决方案中,安全协议是最有效的手段之一。由于网络本身的开放性,使得网络中存在着各种安全威胁,攻击者可以采用多种方式对安全协议进行攻击,破坏其安全属性。分析安全协议中可能存在的缺陷很难完全由人工来识别,因此,需要借助形式化的分析方法和工具来完成。安全协议的形式化分析过程包含安全协议系统建模、安全属性验证、以及攻击序列生成等。本文通过分析安全协议模型中攻击者的“任意”性行为和协议的多次并发会话问题,提出了一种改进的攻击者模型和多并发会话划分分析方法。针对安全属性验证和攻击序列生成问题,采用安全属性违背事件对不安全状态进行分类描述,提出基于安全属性违背事件生成攻击序列的两种方法：状态空间搜索法和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)提出一种基于攻击策略的攻击序列选择生成方法利用攻击序列生成方法能够得到大量的攻击序列,为集中有限的资源对安全协议系统存在的攻击序列实施重点分析,需要进一步确定依据攻击策略的攻击事件,选择生成攻击序列,使生成的有限攻击序列充分覆盖攻击目的。