安全协议也被称之为密码学协议,它的目标是通过应用密码学基件在不安全的网络环境中提供安全的通信服务。安全协议的海量、复杂、易错等特点,导致协议安全性自动化分析的需求与日俱增。CPN Tools（Colored Petri Net,CPN）是一种基于模型检测的协议自动化分析工具,作为模型检测的代表性方法之一,因具备并发分布式系统建模的能力且集成了大量强有力的自动化计算工具,在协议自动化分析领域具有很好的发展前景。但在安全协议分析领域,由于CPN Tools缺乏对敌手状态的有效建模,在利用CPN Tools进行安全协议分析时,针对不同安全协议需要手动构建敌手模型,这一过程会导致协议分析的自动化程度大幅下降,且极易引入安全风险。本文以CPN模型为基础、以协议安全性自动化分析为核心,构建了基于着色Petri网的安全协议自动化建模与分析系统,解决了已有方案需手动构建CPN敌手模型和协议模型的问题,极大提高了系统的自动化程度。该系统基于CPN建模规范自定义一套新的安全协议描述规范,并通过分析CPN模型的XML文件结构,设计了一种CPN基本对象的自动化生成工具,实现了在CPN Tools环境下安全协议分析模型的自动化生成模块和协议文本描述的自动化解析。在此基础上,系统提供一种基于ML语言的协议安全评估规则描述方法,该方法可以精确定位CPN模型状态空间衍生范围,并依据安全评估规则快速检索不安全状态节点,以提取安全协议攻击路径。综上,通过引入上述自动化工具,该系统精简了基于CPN模型的协议安全性分析流程,极大地降低了应用过程中的协议安全性分析门槛。最后,以经典的Andrew Secure RPC协议为实证应用,验证了本文设计的基于着色Petri网的安全协议自动化建模与分析系统的性能和可用性。首先,通过自定义协议描述规范对协议4条会话消息进行文本描述;然后,基于自动化建模工具生成协议安全性分析CPN模型,通过与手动建模在各项条目上的对比,验证了自动化建模工具的自动化性能;最后,通过分析协议需要满足的2项安全要求得出协议安全性分析的3项评估规则,以其中1项评估规则为例,得出依据该评估规则的协议安全性分析结果,通过与现有文献中的安全性分析结果相比,表明了本文所设计的系统具有较强的可行性和有效性。