随着Internet技术持续突飞猛进地发展,网络上的信息安全问题日益突出。特别是电子商务、数字货币和网络银行等新业务的深入开展,信息的保密性、完整性和可用性等安全问题成了关键之所在。安全协议,又称密码协议,是以密码学为基础的协议,它在网络和分布式系统中提供各种各样的安全服务。安全协议的目标都与安全有关,例如,认证主体的身份;在主体之间分配会话密钥等。目前,安全协议已广泛应用于计算机网络与分布式系统中,当前关于安全问题的研究热点之一是安全协议的形式化描述与分析。目前安全协议常见的分析方法包括:逻辑方法、模型检测、定理证明等方法,它们都有各自的优点和缺点。本文主要研究以Petri网模型为基础融入其他方法,提出一种新的协议建模及分析检测方法,并使用该新方法对安全协议进行了分析检测,以验证其有效性。本文的主要创新点及研究成果如下:1.提出了一种新的安全协议建模方法,此方法根据通信主体的三态建立的协议模型具有意义明确、便于分析等特点。2.目前国内外很多学者使用petri网分析安全协议时,往往是通过验证协议的不安全状态是否可达,来判断协议的安全性。而本文所提出的方法是从协议的初始状态出发去检测可能存在的攻击。3.在协议分析检测过程中,本文创造性地融入了其他分析方法,构建了各个通信主体分析集。4.本文研究制定了主体分析集更新规则、攻击检测规则。5.本文使用了该新方法对多个经典协议进行分析检测,并找到了可能存在的攻击。