近年来随着智能制造、工业大数据、物联网的快速发展,传统的工业控制系统正在快速向互联互通的网络化控制系统转变,工业以太网协议也趋于开放化和标准化。作为工业网络控制系统的关键因素,工业以太网协议在带来便利的情况下显著地增加了工业控制系统遭受网络攻击的风险,影响着工业网络控制系统的可靠性和安全性。尽管当前已有大量的研究工作对工业以太网协议安全性进行改进,但这些改进方案均存在较大的局限性,往往专注于协议自身安全功能的实现,缺乏对协议安全性的形式化建模分析和评估。此外,大量安全改进方案需要添加额外的加解密设备来完成安全功能,对实时性和可靠性造成了一定影响,同时增加了企业的硬件成本。因此研究工业以太网协议的形式化建模并进行安全评估,挖掘协议存在的漏洞,对协议进行有效安全性改进具有重要的现实意义和科学价值。本文以工业以太网安全协议“DNP3-SA”为研究对象,以有色Petri网理论和DelovYao攻击方法为指导,基于CPN Tools模型检测工具,重点研究该协议的形式化建模和安全评估,挖掘协议漏洞,提出针对性的安全改进方案,并对所提方案应用CPN和SPAN两种模型检测工具进行安全性验证。具体的研究内容如下:1)对工业以太网协议安全进行深入研究,总结协议安全防护的研究现状。阐述工业控制系统和工业以太网协议的体系结构,分析5种主要协议的脆弱性。从外部主动防御技术、内部被动防御技术和协议安全改进三个方面,提出完善的工业以太网协议安全防护模型,并对主要防护技术进行介绍,指出未来工业以太网协议安全改进的发展方向和研究方法。2)研究基于有色Petri网理论的协议分层建模方法,在抽象出协议消息流模型的基础上,基于CPN模型检测工具,建立4层结构的DNP3-SA协议的HCPN模型,对协议工作模式(主动模式和请求应答模式)和关键消息传输过程进行细粒度的建模,精确模拟协议数据的变化过程,精确反应协议的运行细节。基于状态空间分析结果对协议HCPN模型的功能一致性进行验证。3)充分利用CPN在可视化、模型动态执行以及状态空间分析等方面的优势,针对安全协议形式化分析方法中攻击者的强大能力,研究基于Delov-Yao攻击者模型的改进方案,削减和避免攻击模型状态空间过大或爆炸的问题。在原始HCPN四层模型的基础上,引入重放、欺骗和篡改三种改进的攻击者模型建立协议的安全评估模型。并基于协议认证属性的形式化定义、CPN模型分析工具和状态空间查询方法评估全攻击状态下的协议的安全性,挖掘DNP3-SA协议存在的安全漏洞。4)根据协议的安全评估结果和协议漏洞,将可信平台引入到DNP3-SA协议中以解决工业控制网络设备的身份认证问题。针对性地提出协议的改进方案,包括对协议单播模式和广播模式的安全改进。对于协议单播模式的安全改进,主要基于在身份认证与密钥协商阶段引入可信平台,在密钥更新和通信阶段对消息序列号加密及引入新的随机数,确保通信实体不被劫持、协议序列不被扰乱和消息不被篡改。对于协议广播模式的安全改进,提出的方案通过现有的加密原语与仅由主站生成和分发的单向散列函数(哈希链)保证广播通信阶段的前向安全性。并对两种改进方案应用CPN和SPAN模型检测工具进行安全性评估和验证,给出改进方案的性能分析。