传统的工业控制系统随着工业大数据[1]和物联网[2]的迅猛发展，变得更加互联互通，大量的以太网协议被应用到工业控制系统中，工业以太网协议在其中扮演着重要角色[3].但是由于工业控制系统在设计之初是封闭隔离的，所以大多协议未采用加密认证等信息安全手段[4]，使得攻击者能够很容易对数据进行监听、篡改和窃取等，从而达到破坏系统的目的[5-6].随着控制系统的网络化发展以及工业协议的开放化，协议暴露出许多安全隐患，因此需要重点对协议的安全性进行研究.
本文的主要贡献包括3个方面:
1) 提出了一种基于有色Petri网理论和Dolev-Yao攻击方法的模型检测方法;
2) 对EtherCAT协议的安全机制进行了详细分析，利用建模工具对协议进行了建模，并且验证了模型一致性.引入Dolev-Yao攻击者模型对协议进行了安全评估，发现协议存在的漏洞;
3) 对协议存在的漏洞提出了相应的新方案，并对新方案进行了安全性验证.
1 相关工作
对协议进行安全评估一般使用的是形式化分析方法，包括模型检测方法、定理证明方法、类型检测方法以及模态逻辑方法等.文献[7]分析的模态逻辑方法虽然能够对安全协议进行建模和验证，但是该方法抽象度过高，无法对协议交互的细节进行描述，无法展现协议运行的整体过程.文献[8]中分析了定理证明方法能够不限制协议的运行次数，但是不能够实现自动化.文献[9]中指出类型检测方法能够得出安全协议的结论，但是不能表现出攻击序列.基于模型检测的安全评估方法，能够对协议的行为进行安全建模，但是面临状态爆炸问题.针对于EtherCAT协议的安全研究，文献[10]通过基于机器学习的异常检测方法对EtherCAT进行了分析，发现该方法不仅能够进行异常检测，还可以标记攻击类型，但是未给出相应的改进方案；文献[11]中通过建立面向数据流的模型对EtherCAT进行分析，发现该方法能够对协议进行直观、准确的图形表示，并且能够验证协议的正确性，但是建模效率较低，一旦出错就得重新建模.
综上所述，目前已有的对工业以太网协议安全研究的工作大多集中在协议自身安全功能的实现，对协议的安全评估还处于起步阶段，针对工业以太网协议安全评估模型的建立，以及攻击者模型的建立，存在一定的问题.本文针对EtherCAT协议中的安全机制FSoE进行重点研究，以文献[12]中的有色Petri网理论和Dolev-Yao攻击方法为指导，利用建模工具CPN Tools对协议进行安全评估，挖掘协议漏洞，提出新的改进方案，并且对新方案进行安全性验证.
相比已有的研究工作，本文提出了基于有色Petri网理论和Dolev-Yao攻击方法的模型检测方法对协议进行安全分析；对协议的模型进行一致性验证，并且引入攻击者模型对协议进行安全评估；对协议安全评估的结果，提出针对性的新方案，并对新方案进行安全性验证.
2 相关理论
2.1 EtherCAT及其运行原理
EtherCAT协议是由EtherCAT技术集团(ETG)支持[13]的一种流行的实时工业以太网，该协议使用了以太网标准IEEE802.3的物理层和链路层，并且由Beckhoff定义.它是一种开放的实时以太网通信技术协议，具有高速低延时、适用性强、符合以太网标准、刷新周期短、同步性能好等特点，支持多种网络连接拓扑结构.
EtherCAT协议的工作原理如图1所示,Ether-CAT主从站之间的交互行为是由主站主动发起的，主站通过标准的以太网数据帧的形式将EtherCAT数据帧发送给从站，报文在经过每个从站时，从站对报文中与自己相关的数据信息进行相应处理，在报文的指定位置进行数据的读写，并且对计数器信息WKC(working counter)进行加1操作来表示从站对报文进行了处理，然后将数据帧传输到下一个从站节点，经过最后一个从站节点的处理后进行返回，最终通过第1个节点返回到主站[14-16].
Fig. 1 The operation principle of EtherCAT protocol
图1 EtherCAT协议的运行原理
2.2 安全机制FSoE简介
现代通信系统不仅要实现控制数据的确定传输，还要在相同的介质中进行安全关键控制数据的传输.
EtherCAT使用FSoE(fail safe over EtherCAT)机制来实现该目的.EtherCAT安全技术是基于IEC 61508开发的，由TÜV认证，并符合IEC 61784-3标准.该协议可支持功能安全等级SIL 3的安全应用场合.安全数据帧可被看作一个“安全容器”，其中包含了安全关键过程数据以及一些用于保证数据安全性的额外信息[17].
安全数据帧如图2所示，其至少可以传输1B的安全数据(Safedata)，也可以传输1 B或2 B倍数的Safedata，每2 B的Safedata被2 B的CRC校验.Safedata的长度在FSoE从属安全设备描述中定义，其最大数量不受协议的限制；CRC校验结果包括4种因素，分别为最后接收到的FSoE帧的CRC、传输数据(ConnlD,CMD,Data)、CRC的索引以及会话ID；其中的连接ID指示FSoE主节点和FSoE从节点之间的连接，它应该是系统中唯一的连接ID，必须在配置中进行检查.
Fig. 2 Data frame structure of FSoE
图2 FSoE的数据帧结构
2.3 CPN及建模工具
Petri网的概念是由德国科学家Carl Adam Petri最早提出的，后来出现了许多扩展的概念，例如时间Petri网、随机Petri网、CPN等[18-20].形式化建模工具CPN Tools具有编辑、模拟、状态空间分析和性能分析等特性，而且能够通过回馈机制对产生的错误进行精准定位.CPN建模能够进行增量语法检查及代码生成，在一定程度上保证了模型的正确性.该工具是由丹麦奥胡斯大学基于Design/CPN开发的，使用良好的人机界面技术对用户图形界面(GUI)进行了设计，不仅能够对有色Petri网进行编辑、模拟和分析，而且支持时间CPN和分层CPN，借助CPN工具，用户不仅可以轻松建模，还可以仿真和分析并行系统[21-22].
3 EtherCAT协议建模
在创建大型的、比较复杂的Petri网时，用传统的CPN模型是比较麻烦的，我们基于模块编程化思想，利用CPN建模工具内的替代变迁的概念可以将CPN网络结构拆分成多个小块.具有替代变迁的网络是多层次的网络，我们可以先从广义上建立一个简化的网络模型，然后再利用高层次中的替代变迁关联到更为详细的子页面中去，这样可以逐步细化自己的模型.
工业以太网的协议模型一般由3个部分组成，分别为发送端、接收端和中间的通信网络，但是一般用于工业上的协议通信都比较复杂，建立传统的模型可重用性较低，而且不能很好地表现其功能，利用分层建模的方法可以降低复杂度，本文将协议建模划分为顶层、中层和底层3个层次.
3.1 EtherCAT协议消息流模型
EtherCAT主从站之间存在2种通信模式，分别为过程数据通信和邮箱数据通信.EtherCAT使用安全机制FSoE来保证协议的安全性，该安全机制使用了过程数据通信模式，如图3所示为其信息的传输过程.
1) 主站发起会话连接请求，请求信息包括主站地址、从站地址以及会话连接ID.
2) 从站处理接收到的信息，如果连接成功，则回复连接成功消息和连接ID，如果失败，则进行重置操作.
3) 主从站成功建立连接后，进行安全数据传输，主站将安全数据进行分段处理，拆分为多个字节，然后对拆分后的安全数据分别进行本地CRC校验，最后将安全数据、CRC校验数据、命令信息、连接ID和计数器信息一并发给从站.
4) 从站接收到数据后，会将安全数据在本地进行CRC校验，然后与接收到的校验数据进行对比，如果相同则进行相应的命令操作，然后将计数器信息加1后，回复主站计数信息；如果不同，则进行重置操作.
Fig. 3 Message flow model of EtherCAT protocol
图3 EtherCAT协议的消息流模型
3.2 EtherCAT协议的CPN模型建立
本文将Ethernet协议的安全机制FSoE的主从站交互过程进行具体建模，该安全机制使用的是过程数据通信模式.
EtherCAT协议的顶层CPN模型如图4所示，顶层模型从整体上模拟了协议的会话过程，包括协议的通信双方、通信网络以及传输信息.图4中双线矩形代表替代变迁，椭圆代表消息库所，通信的主站用替代变迁Master表示，通信从站用替代变迁Slave表示，通信网络用替代变迁NET表示.
协议的中层模型由5个替代变迁和9个库所组成，如图5所示.主站向从站发起建立连接信息的过程由替代变迁Connection表示；从站对主站的连接信息进行处理和回复的过程由替代变迁Connection′表示；主站向从站发送安全数据的过程由替代变迁Safedata表示；从站对安全数据处理和回复的过程由Safedata′表示.
Fig. 4 Top level model of EtherCAT protocol
图4 EtherCAT协议的顶层模型
Fig. 5 Middle level model of EtherCAT protocol
图5 EtherCAT协议的中层模型
Fig. 6 Internal model of alternative transition Connection
图6 替代变迁Connection的内部模型
EtherCAT协议的底层模型包括5个部分，我们按照协议主从站整体的交互顺序，依次对会话连接过程和安全数据传输过程做详细介绍.图6对替代变迁Connection的内部模型进行了详细描述.变迁Conn_MAC将主站地址信息Mac_M和从站地址信息Mac_S合并成地址信息，变迁Combination将地址信息和连接ID合并为连接请求信息，通过库所Send_conn发送到从站；从站回复的确认信息由库所Rec_ConnID进行接收，确认信息通过变迁R_ConnID进行处理，然后将连接ID通过库所ConnID发送给安全数据.
图7对替代变迁NET的内部模型进行了详细描述.变迁Transmit_conn和Transmit ConnID分别模拟了在建立连接过程中，主站向从站发起连接请求信息的传输路径以及从站向主站回复信息的传输路径；同样在安全数据传输过程中，主站向从站发送安全数据的传输路径和从站向主站回复计数信息的传输路径由变迁Transmit Safedata和Transmit WKC表示.
图8对替代变迁Connection′的内部模型进行了详细描述.库所Rec_conn用来接收主站发送的连接信息，变迁R_conn message对接收到的信息进行处理，然后将接收到的消息存储到库所ReceiveMAC中，变迁Reply将连接ID信息和确认信息进行整合，通过库所Send_ConnID发送给主站，如果连接失败则从站会进行重置操作.
Fig. 7 Internal model of alternative transition NET
图7 替代变迁NET的内部模型
Fig. 8 Internal model of alternative transition Connection′
图8 替代变迁Connection′的内部模型
Fig. 9 Internal model of alternative transition Safedata
图9 替代变迁Safedata的内部模型
Fig. 10 Internal model of alternative transition Safedata′
图10 替代变迁Safedata′的内部模型
图9对替代变迁Safedata的内部模型进行了详细描述.变迁CRCdata首先对安全数据进行本地的CRC校验，然后将安全数据和CRC检验数据进行合并；变迁Combination′将接收到的确认连接ID信息、CMD命令信息和计数信息WKC进行合并；最后这些数据由库所Safeoutput一并发送给从站；计数器WKC的更新信息由库所Rec_WKC进行接收.
图10对替代变迁Safedata′的内部模型进行了详细描述.库所Safeinput用来接收主站发送的安全数据信息，变迁Safe_Message将接收的安全数据信息进行分解，从站对安全数据进行本地的CRC校验，然后与接收到的CRC校验数据进行对比，如果相同则按照接收到的命令信息进行操作，并将接收到的计数信息加1，由库所Send_WKC返回给主站.如果本地生成的CRC检验值与接收到的校验数据不同，则进行重置操作.
3.3 EtherCAT模型一致性验证
我们将对建议的原始EtherCAT协议的CPN模型进行一致性验证，使用了状态空间[23]分析工具.首先我们对所建立的模型给出了预期结果，模型会成功进行会话连接和安全数据传输，整个交互过程中不会产生重置操作.通过对表1的状态空间结果分析，可以发现状态空间节点、有向弧与强连通节点、强连通弧的数目相同，说明我们建立的原始模型不存在导致状态无限循环和迭代行为，所有状态节点都是可达的；主状态节点和活变迁为0，说明原始模型没有始终处于激活状态的活变迁，同时也不存在任意可达的状态；死节点为1，表示全部请求都被从站执行；存在2个死变迁Reset和Reset1，变迁Reset是用来表示连接失败后的重置操作，变迁Reset1是表示数据传输过程中CRC校验失败后的重置操作，这2个变迁均为死变迁说明模型不存在连接失败和数据传输失败的情况，与预期结果一致.
Table 1 State Space Analysis of the Original Model of EtherCAT Protocol
表1 EtherCAT协议原始模型状态空间分析
TypeNumberNameState Space Node31764State Space Arc102734SCC Graph Node31764SCC Graph Arc102734MainState Space Node0Live Transition0Dead Marking1Dead Transition2Reset∕Reset1
4 基于攻击者安全评估模型
Dolev和Yao发表了一篇重要论文，其对协议安全研究发展产生了深刻的影响[24].该论文的主要观点就是在假设密码系统是“完美”的基础上只讨论协议本身的安全属性，这样能够不去讨论密码算法的安全性而是专心研究协议的内在安全性质;而且Dolev和Yao提出了攻击者模型，攻击者具体强大的计算能力，不仅能够对协议运行过程中真实实体间交换的信息进行窃听、截获、篡改、重放操作，还可以对这些信息进行加密、解密、拆分和组合[25-26].
由于EtherCAT协议具有高度的实时性，数据帧经过每个从站的时间极小，在从站中数据帧的接收与解码、数据的提取与插入、数据帧的转发都是由硬件来实现的，因此本文将尝试对主从站之间的网络通道引入攻击模型.
4.1 引入攻击者模型
根据Dolev-Yao攻击者模型中，攻击者所具备的对网络信道发起各类中间人攻击的强大能力，对原始模型的网络传输层引入重放、欺骗和篡改的中间人攻击.
如图11所示，我们对原始模型的网络传输层面引入中间人攻击包括重放、欺骗和篡改攻击，图11中蓝色部分标注的库所和变迁模拟了重放攻击，变迁TA截获协议第一次传输时的信息，库所distri能够存储分解和待分解的信息，库所P2和P3存储原子信息.变迁TC采用攻击者的分解规则后将形成的原子消息保存到库所P3中，变迁TH采用攻击者的过度规则将无法解密的信息采用过度规则保存到库所P4中.变迁TD将采用攻击者的合成规则将原子消息合成后保存到库所P5中.使用并发控制库所SP对合成规则对应的变迁TD加以限制，初始状态可使能之外，每当有分解的信息产生后再进行点火合成.变迁TF将攻击者的信息合成发送到信道端口库所.图11中的红色标注的弧上的表达式和变迁库模拟了篡改攻击，表达式中引入的攻击者attack，通过变迁ATTACK发起攻击.图11中的紫色部分模拟了欺骗攻击，包括了原始网络传输过程中的全部变迁Transmit conn,Transmit ConnID,Transmit,SafeData,Transmit WKC.
Fig. 11 Attacker model
图11 攻击者模型
4.2 EtherCAT模型安全性评估
由表2所示的攻击者模型的状态空间报告可知状态空间节点、有向弧与强连通节点、强连通弧的数目相同，说明该协议的攻击者模型所有状态节点都是可达的，引入攻击者模型后，其状态空间节点和弧的数量相对于原始模型来说增加不是太多，说明引入攻击者模型后不会出现状态空间过大或者爆炸的情况，降低了状态空间节点规模，减少了不被接受者认可的消息，在保证攻击能力的基础上提高了攻击模型效率.说明我们引入的攻击者模型是有效的.
Table 2 State Space Comparison of Models
表2 模型状态空间对比
TypeOriginal ModelAttack ModelState Space Node3176437987State Space Arc102734123328SCC Graph Node3176437987SCC Graph Arc102734123328Dead Marking16Dead Transition28
将原始模型和加入攻击模型后的状态空间进行对比，我们发现死节点变成6个，死变迁变成8个.通过对死节点进一步的查询分析，发现有2个死节点是由于引入重放攻击和篡改攻击导致从站进行了重置操作而产生的，剩下的4个死变迁是因为引入欺骗攻击致使协议产生不可预期的终态而导致的；通过对死变迁进行分析，发现有2个死变迁是由于引入重放攻击使得会话连接在从站无法使能，另外2个死变迁是由于引入欺骗攻击导致从站没有接收到从站的返回信息，其余4个死变迁则是因为引入篡改攻击导致在安全数据传输过程中CRC校验错误而未使能.通过状态空间的对比分析，可以发现攻击者模型对原始模型的会话连接和安全数据传输过程发起了有效攻击，侧面反映出原始协议存在中间人进行重放、欺骗和篡改的漏洞.
5 EtherCAT协议新方案
5.1 新方案加固方法
通过引入攻击者模型对协议进行安全评估，发现协议存在中间人进行重放、欺骗和篡改的漏洞，针对安全评估结果，我们在协议的会话连接过程中引入秘钥分发中心进行认证加固，为了确保安全数据的安全传输，我们在安全数据传输过程中加入Hash值.
如图12所示为改进后的消息流图，改进后的消息传输过程为：
1) 主站向秘钥中心发生请求，包括主站地址、从站地址和连接ID.
2) 秘钥分发中心对接收到的数据进行处理，将地址信息和公钥Ks用从站的私钥Kb进行加密，与公钥Ks和接收到的其他信息，一起用主站的私钥Ka进行加密，然后回复给主站.
3) 主站用自己的私钥对从站回复的消息进行解密，得到公钥Ks后，将其余需要发送给从站的消息发送给从站.
4) 从站用自己的私钥Kb将收到的消息进行解密，获得公钥Ks，利用公钥将新产生的会话连接ID进行加密，然后回复给主站.
5) 主站用公钥将从站回复的消息进行解密，获得会话ID后，在本地对会话ID进行函数运行，最后用公钥加密函数运算的结果，发送给从站进行认证.
6) 从站用公钥进行解密接收到的消息，并且对解密后的会话ID 进行认证.
7) 建立会话连接之后，主站发起安全数据传输，首先将安全数据进行本地Hash，然后将安全数据、Hash值、命令信息、计数信息和连接ID一并发送给从站.
8) 从站首先对接收到的信息进行拆分，然后对安全数据进行本地Hash,用本地生成的Hash值与接收到的Hash值进行比对，如果相同则进行相应的命令操作，并且将技术信息加1，回复给主站.
Fig. 12 Message flow model of the new scheme
图12 新方案的消息流模型
Fig. 13 Middle level model of new scheme model
图13 新方案模型的中层模型
5.2 EtherCAT协议新方案模型
我们将原始协议进行加固，并且进行CPN建模.改进后的中层模型加入了秘钥分发中心，由6个替代变迁和13个库所组成，如图13所示.其中，秘钥分发过程由替代变迁Key Distribution表示，主从站连接建立以及认证的过程由替代变迁Connection和Connection′来表示，安全数据的传输过程由替代变迁Safedata和Safedata′表示.改进后的中层模型整体上描述了秘钥分发、连接认证和安全数据传输的过程.
图14对新方案替代变迁Connection的内部模型进行了详细描述.主从站的地址信息和连接ID由变迁Combination进行合并，然后通过库所SendMAC发送到秘钥分发中心；秘钥分发中心返回的消息由库所RecKs进行接收；主站利用自己的私钥Ka对收到的消息进行解密，同时对收到的消息进行确认；将解密后需要发送给从站的消息通过库所SendKb发送给从站；利用解密后的公钥Ks对库所RecSid′接收到的从站返回信息进行解密，对解密后获得的连接ID通过变迁Function进行函数运算；利用公钥Ks对函数运算的结果通过变迁变迁EncFID进行加密，最后由通过库所SendfSid发送给从站.
Fig. 14 Internal model of alternative transition Connection of new scheme model
图14 新方案模型的替代变迁Connection内部模型
图15对新方案替代变迁Key Distribution的内部模型进行了详细描述.秘钥分发中心将主站的请求信息和要分发的公钥Ks通过变迁Ks-Msg1进行整合；将收到的地址信息和公钥Ks通过变迁Kb-Msg进行整合；将要回复主站的消息通过变迁ComMsg进行打包；利用主站私钥Ka对打包消息通过变迁KComMsg进行加密，最后由库所RecKs发送给主站.
图16对新方案替代变迁Combination′的内部模型进行了详细描述，从站利用自身私钥Kb对接收到的消息通过变迁DecMsg进行解密；利用解密后获得的公钥Ks对新产生的连接ID通过变迁EncID进行加密，加密后的消息由库所RecSid发送给主站；利用公钥对主站发送的认证消息通过变迁DecFID进行解密，通过解密后获得的连接ID进行连接认证.
Fig. 15 Internal model of alternative transition Key Distribution of new scheme model
图15 新方案模型的替代变迁Key Distribution内部模型
Fig. 16 Internal model of alternative transition Connection′ of new scheme model
图16 新方案模型的替代变迁Connection′内部模型
图17对新方案替代变迁Safedata的内部模型进行了详细描述，新方案主要改进在于，通过变迁HashSafedata对安全数据进行本地Hash处理，最后将Hash值与安全数据一并发送给从站.
图18对新方案替代变迁Safedata′的内部模型进行了详细描述，新方案的主要改进在于，将接收到的安全数据通过变迁HashSafedata进行本地Hash处理，通过变迁Comparison对新产生的Hash值Hdata′和接收到的Hash值Hdata进行对比处理，相同则证明数据没有被篡改，然后进行相关命令的操作，并且将计数器加1返回给主站.如果不同则进行重置操作.
Fig. 17 Internal model of alternative transition Safedata of new scheme model
图17 新方案模型的替代变迁Safedata内部模型
Fig. 18 Internal model of alternative transition Safedata′ of new scheme model
图18 新方案模型的替代变迁Safedata′ 部模型
5.3 新方案安全评估模型
我们利用相同的方式，引入Dolev-Yao攻击模型，对新方案模型的网络层面进行中间人攻击，包括篡改、欺骗和重放攻击.如图19所示，蓝色部分模拟重放攻击，红色部分模拟篡改攻击，紫色部分模拟欺骗攻击.
Fig.19 Security evaluation model of new scheme
图19 新方案安全评估模型
5.4 新方案模型安全性验证
我们将新方案模型安全评估的状态空间与改进前进行对比，如表3所示.我们可以发现由于引入了秘钥分发中心进行认证以及对数据加入了Hash值，增加了许多库所和变迁，使得新方案的的状态空间节点和弧数目有所增加.利用改进前协议存在的3类中间人攻击对新方案进行安全性验证.由表3 的状态空间对比结果可以发现，新方案模型的状态空间死节点减少成一个，通过进一步查询得知，这个死节点表示协议运行后的终态，而改进前的多个死节点是由于攻击状态而造成的，说明新方案未遭受攻击.新方案的死变迁相较于改进前的死变迁数目有所变化，进一步分析发现这些死变迁均发生在网络层面，是由于攻击者无法发起有效攻击而造成的.攻击者无法获取协议连接过程的会话秘钥，而无法对获取的信息进行解密分解，从而无法发起重放攻击；在数据传输层面，新方案对协议的传输消息进行了Hash处理，由于Hash值的不可逆性，所以攻击者无法对消息发起篡改攻击；由于新方案对协议加入了认证，所以攻击者无法对协议进行欺骗攻击.
Table 3 Comparison of the State Space of the Safety Assessment Model
表3 安全评估模型状态空间对比
TypeBefore ImprovementNew SchemeState Space Node3798739128State Space Arc123328158885SCC Graph Node3798739128SCC Graph Arc123328158885Dead Marking61Dead Transition87
通过分析表明，由于攻击者无法获得消息的会话秘钥、认证秘钥以及无法篡改数据的Hash值，使得攻击者无法发起攻击，从而证明了新方案能够防御之前的3种中间人攻击，满足协议安全机制需求.
5.5 新方案性能分析和分析方法对比
本节我们对新方案进行性能分析，新方案通过引入秘钥分发中心对协议主从站建立连接的过程进行认证加固，秘钥靠秘钥分发中心分发，不需要主从站生成，因此对协议通信的整体时间消耗较小.新方案在安全数据传输中加入了Hash值，不需要对安全数据进行过多的加密操作，因此不需要对平台进行过大的升级，只是对整个通信来说，增加了计算、通信和存储数据的开销.所以改进方案对协议运行的开销不大，仅仅增加了计算和存储成本.本文在对协议进行引入秘钥分发中心和Hash函数改进时，增加了协议消息交互的步骤，在增强协议安全性的同时会对协议的实时性有所影响.
我们将本文用到的形式化分析方案与其他分析方法做比较，文献[10]中通过基于机器学习的异常检测方法对EtherCAT进行了分析，发现该方法不仅能够进行异常检测，还可以标记攻击类型；文献[11]中通过建立面向数据流的模型对EtherCAT进行分析，发现该方法能够对协议进行直观、准确的图形表示，并且能够验证协议的正确性.通过表4的对比分析，我们可以看出本文的基于有色Petri网理论和Dolev-Yao攻击方法为指导模型检测方法不仅能够进行直观、准确的图形化描述和验证协议功能的正确性，还可以发现协议的攻击类型，对协议通过引入攻击者进行异常检测.同时方案对引入的攻击模型进行了改进，解决了传统模型检测方法的状态空间爆炸的问题，可以用该分析方案对其他工业以太网协议进行安全分析与研究.
Table 4 Comparison of Protocol Formal Analysis Methods
表4 协议形式化分析方法对比
SchemeAnomalyDetectionAttackTypeIntuitiveGraphicVerifyFunctionalCorrectnessStateSpaceRef [10]√√Ref [11]√√Our Scheme√√√√√
6 总结与展望
本文将研究的重点放在工业以太网应用热门的EtherCAT协议的安全机制FSoE上，首先通过对协议安全机制消息流的分析，利用建模工具CPN Tools对协议进行HCPN建模；然后在原始模型的基础上加入攻击者模型，并且通过对原始模型和攻击模型状态空间表进行对比，对模型进行安全性评估发现协议存在重放、窃听和篡改3类中间人攻击；最后针对协议所存在的3类攻击提出了新的方案，并且对新方案进行再次建模，引入攻击者模型进行再次攻击，通过分析改进前和新方案的状态空间表，得出新方案可以有效防御重放、窃听和篡改3类中间人攻击.但是本文研究目的是为了改进协议的安全性，对协议的实时性考虑不足，而且只对协议进行了中间人攻击，并未考虑协议是否存在其他形式的攻击.下一步将考虑协议在保证安全的情况下是否满足实时性要求，还有在其他攻击形式下是否还存在安全的不足.
[1]ur Rehman M H, Ahmed E, Yaqoob I, et al. Big data analytics in industrial IoT using a concentric computing model[J]. IEEE Communications Magazine, 2018, 56(2): 37-43
[2]Sisinni E, Saifullah A, Han S, et al. Industrial Internet of things: Challenges, opportunities, and directions[J]. IEEE Transactions on Industrial Informatics, 2018, 14(11): 4724-4734
[3]Li Qiang, Feng Xuan, Wang Haining, et al. Understanding the usage of industrial control system devices on the Internet[J]. IEEE Internet of Things Journal, 2018, 5(3): 2178-2189
[4]Xu Yikai, Yang Yi, Li Tianren, et al. Review on cyber vulnerabilities of communication protocols in industrial control systems[C] //Proc of IEEE Conf on Energy Internet and Energy System Integration (EI2). Piscataway, NJ: IEEE, 2017: 1-6
[5]McLaughlin S, Konstantinou C, Wang Xueyang, et al. The cybersecurity landscape in industrial control systems[J]. Proceedings of the IEEE, 2016, 104(5): 1039-1057
[6]Li Xuan, Zhou Chunjie, Tian Yu-Chu, et al. Asset-based dynamic impact assessment of cyberattacks for risk analysis in industrial control systems[J]. IEEE Transactions on Industrial Informatics, 2017, 14(2): 608-618
[7]Konigsberg Z R. Modeling and verification analysis of a flexible manufacturing system: A modal logic approach[J]. Neural, Parallel & Scientific Computations, 2018, 26(1): 65-74
[8]Rashid A, Siddique U, Tahar S. Formal verification of cyber-physical systems using theorem proving[C] //Proc of Int Workshop on Formal Techniques for Safety-Critical Systems. Berlin: Springer, 2019: 3-18
[9]Cremers C, Dehnel-Wild M, Milner K. Secure authentication in the grid: A formal analysis of DNP3 SAv5[J]. Journal of Computer Security, 2019, 27(2): 203-232
[10]Akpinar K O,Ozcelik I. Analysis of machine learning methods in EtherCAT-based anomaly detection[J]. IEEE Access, 2019, 7: 184365-184374
[11]Wang Shun, Li Xiaojuan, Guan Yong, et al. Executable micro-architecture modeling and automatic verification of EtherCAT[C] //Proc of 2018 IEEE Smart World, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation. Piscataway, NJ: IEEE, 2018: 308-315
[12]Lu Ye. Formal security assessment and improvement of DNP3-SA Protocol based on HCPN model detection[D]. Lanzhou: Lanzhou University of Technology, 2018 (in Chinese)(鲁晔. 基于HCPN模型检测方法的DNP3-SA协议形式化安全评估与改进[D]. 兰州: 兰州理工大学, 2018)
[13]Langlois K, Tom V D H, Rodriguez C D, et al. EtherCAT tutorial: An introduction for real-time hardware communication on windows[J]. IEEE Robotics & Automation Magazine, 2018, 25(1): 22-122
[14]Park S M, Kim H, Kim H W, et al. Synchronization improvement of distributed clocks in EtherCAT networks[J]. IEEE Communications Letters, 2017, 21(6): 1277-1280
[15]Delgado R, Shin W C, Hong C H, et al. Development and control of an omnidirectional mobile robot on an EtherCAT network[J]. International Journal of Applied Engineering Research, 2016, 11(21): 10586-10592
[16]Li Liying, Cong Peijin, Cao Kun, et al. Game theoretic feedback control for reliability enhancement of EtherCAT-based networked systems[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits andSystems, 2018, 38(9): 1599-1610
[17]Morato A, Vitturi S, Cenedese A, et al. The fail safe over EtherCAT (FSoE) protocol implemented on the IEEE 802.11 WLAN[C] //Proc of the 24th IEEE Int Conf on Emerging Technologies and Factory Automation (ETFA). Piscataway, NJ: IEEE, 2019: 1163-1170
[18]Simon M, Moldt D, Schmitz D, et al. Tools for curry-coloured Petri nets[C] //Proc of Int Conf on Applications and Theory of Petri Nets and Concurrency. Berlin: Springer, 2019: 101-110
[19]Li Liang, Basile F, Li Zhiwu. An approach to improve permissiveness of supervisors for GMECs in time Petri net systems[J]. IEEE Transactions on Automatic Control, 2019, 65(1): 237-251
[20]Abbaszadeh M, Saeedvand S. Weak consistency model in distributed systems using hierarchical colored Petri net[J]. Journal of Computers, 2018, 13(2): 236-243
[21]Arena D, Criscione F, Trapani N. Risk assessment in a chemical plant with a CPN-HAZOP Tool[J]. IFAC-Papers OnLine, 2018, 51(11): 939-944
[22]Artamonov I V, Sukhodolov A P. CPN tools-based software solution for reliability analysis of processes in microservice environments[J]. International Journal of Simulation: Systems, Science and Technology, 2018, 19(6): 56.1-56.8
[23]Gu Ya, Liu Jicheng, Li Xiangli, et al. State space model identification of multirate processes with time-delay using the expectation maximization[J]. Journal of the Franklin Institute, 2019, 356(3): 1623-1639
[24]Dolev D, Yao A. On the security of public key protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208
[25]Baskar A, Ramanujam R, Suresh S P. Dolev-Yao theory with associative blindpair operators[C] //Proc of Int Conf on Implementation and Application of Automata. Berlin: Springer, 2019: 58-69
[26]Rocchetto M, Tippenhauer N O. CPDY: Extending the Dolev-Yao attacker with physical-layer interactions[C] //Proc of Int Conf on Formal Engineering Methods. Berlin: Springer, 2016: 175-192
