随着全球信息技术和智能化的飞速发展,第四次工业革命最显著的特点是将工业与互联网的连接变得越来越紧密。OPC UA协议是工厂设备之间进行交互时使用的协议,为独立于生产厂商和开发平台的系统或设备提供通信连接,需要实现工业互联网行业设备之间远距离的数据共享和传输、多平台互联等,OPC UA协议被广泛应用于该行业,这将难以避免地把协议自身存在的潜在威胁引入工控系统,在此过程中工控系统协议的安全性问题油然而生。近几年,持续上升的工控系统网络攻击事件也充分证实了这一点,表明工控系统安全问题早已不可忽视。目前针对工控协议的研究大多数集中在协议自身安全功能的实现层面以及在其他领域的应用方面,较为局限,缺乏采用形式化的方法对协议展开建模和评估。本文的研究对象是工厂设备之间进行交互时使用的OPC UA协议,采用着色Petri网作为理论基础,并以Dolev-Yao攻击者模型为指导,主要从如何正确的对该协议握手阶段的两个子协议进行形式化建模和基于改进的Dolev-Yao攻击者模型建立协议安全评估模型验证该协议的安全性和隐私性方面做了详细研究。论文具体研究工作如下:1、通过对该协议握手阶段的两个子协议进行详细分析,构建出子协议的消息流模型图。基于此再根据着色Petri网理论中的HCPN（Hierarchical Colored Petri Nets）分层建模方案,使用Petri网建模工具CPN Tools对OPC UA的两个子协议建立3层结构的初始模型。在HCPN建模中,顶层模型结构从较为宏观的角度描述子协议的交互过程,中层模型是在顶层模型基础上对协议的通信实体进一步细化,底层模型是在中层模型基础上对协议交互过程的详细描述。通过分析子协议初始模型状态空间中的各类属性来验证子协议初始模型的正确性及合理性。2、在协议形式化分析建模过程中,加入攻击者模型后控制模型的状态空间规模一直以来是重点关注的问题。考虑到建模过程灵活、图形化界面直观易懂以及自动生成状态空间报告的优势,选用CPN Tools对协议展开建模。为解决状态空间爆炸问题,对消息流中的信息进行拆解和参数化,提出了改进的DolevYao攻击者模型。基于子协议原始HCPN模型的基础上,在网络信道上添加攻击者模型,由此建立子协议的安全评估模型,并在安全评估模型中添加重放、篡改、欺骗三种中间人攻击。通过分析CPN Tools生成的状态空间报告的参数,同时结合工具中SML查询语言发现协议的潜在威胁以及总结安全问题产生的原因。3、针对OPC UA子协议中随机数的机密性和基于身份认证属性的欺骗问题,结合密码学、网络安全知识提出针对性的安全增强方案。新方案在子协议的消息流中添加接收者公钥,并对随机数加入密钥包装机制可以有效提高协议的安全性,抵御各类中间人攻击。并对子协议新方案展开安全性评估,此外,提出一种不可链接性的建模方法来验证子协议新方案的隐私性。