Formal Security Evaluation and Improvement of Industrial Ethernet EtherCAT Protocol

The EtherCAT protocol is widely used due to its high real-time performance and strong performance. However, with the rapid development and openness of the Industrial Ethernet protocol, industrial control systems are subject to huge network attack risks. There are many studies on the security and improvement of industrial Ethernet protocols, but these studies lack formal modeling and security evaluation of the protocol, and only focus on the realization of the security function of the protocol itself, which has certain limitations. In order to solve the current situation of industrial Ethernet being attacked, we take EtherCAT protocol which is widely used at present as the research object, and propose a model checking method based on colored Petri net theory and Dolev-Yao attack method, and evaluate and improve the security of the protocol. First, we verify the security mechanism of the protocol FSoE based on Petri net theory and CPN Tools model tools; then introduce the Dolev-Yao attack model to evaluate the security of the original model of the protocol. It is found that there are 3 types of man-in-the-middle attack vulnerabilities in the protocol, including tampering, replay, and deception. Finally, a new solution is proposed for the vulnerabilities in the protocol. A key distribution center and a Hash function are added to the original protocol. The security verification of the new scheme is carried out again using the CPN model detection tool. Through verification, it can be found that the new scheme can effectively prevent 3 types of man-in-the-middle attacks and improve the security of the protocol.