协议是指两个或者两个以上的参与者为完成某一项特定任务相互约定的执行步骤和执行规则.协议的定义包含三层含义：⑴协议至少有两个参与者；⑵协议在参与者之间表现为消息交换和消息处理交替进行的一些列步骤；⑶协议的执行是为了能够完成某项任务或达成某种共识。安全协议就是建立在密码体制基础上的一种通信协议,他运行在计算机网络或分布式系统中。借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重要。安全协议攻击者的破坏和安全协议无穷个会话的并发交叠运行使得安全协议运行时往往难以实现它的设计目标。形式化方法已被证明是分析和验证安全协议的有效手段。近几十年来,运用形式化方法对安全协议进行分析一直是信息安全领域研究的热点,并产生了一系列比较有效的验证方法和验证工具,如BAN类逻辑、串空间模型、Petri网模型等形式化方法和FDR、NRL等分析器。但是具体的形式化方法在分析安全协议时都有其不足之处,如形式化定义不规范、通用性差、分析效率低、缺乏自动工具等。所以如何取长补短,改进已有方法的缺陷或发现更有效的方法是当前安全协议形式化分析工作的趋势。　　 本文针对目前安全协议形式化分析中存在的问题进行研究,主要工作和研究成果如下：⑴通过对不可否认协议的语义进行分析,建立CPN(coloured petri net,有色petri网)中基本元素与安全协议中元素的对应关系,对CPN Tools提供的建模语言(CPN ML)在规范协议描述、简化协议建模、自动检测方面进行扩展,提出一种基于CPN的通用和规范的安全协议形式化分析语言,该语言可以像用面向对象编程语言编程一样对安全协议进行建模。⑵利用本文扩展的安全协议分析语言,提出一种新的不可否认协议分析方法,该方法利用CPN tools的状态空间查询功能和自建的查询函数库来对不可否认协议进行分析和验证,该方法具有通用性强、时效性强、交互性好等诸多优点,并通过实例说明这种方法的有效性。⑶利用本文扩展的安全协议分析语言和有色petri网建模工具CPN tools中的查询函数对安全协议的通用属性进行描述,把安全属性的验证问题就转化为模型状态空间的分析问题,使得模型的建立与分析一体化,并提供了通用的安全属性描述与验证方法,同时验证过程是自动进行的,并且可以自动查找攻击路径。