| Industrial Control Systems(ICS)is the economic lifeblood of a country and is widely used in various fields of the national economy.It is an important part of many key infrastructures in our country,and its safety is self-evident.With the proposal of "Made in China 2025",industrial control systems and network interconnection have become an inevitable trend.At present,due to the lack of cor e technology in the application of industrial control systems in China,foreign industrial control system protocols and industrial control equipment are commonly used In recent years,the industrial control security defence has just started,and the security analysis of the protocol is imminent.The formal analysis of the security protocol is the most convenient and effective model-based formal analysis method.The TLS protocol studied in this thesis is used to ensure the security of EtherNet/IP protocol da ta transmission in industrial network control systems.1.First of all,due to the hidden security risks of the EtherNet/IP protocol,the industrial control system based on this protocol has the threat of information theft and tampering.The security of information transmission depends on the security of the TLS protocol between the transport layer and the application layer.At present,the EtherNet/IP protocol still uses the TLS1.2 version.In order to improve security,it will inevitably choose to embed i n future development.TLS1.3 to improve the overall security of the EtherNet/IP protocol.This thesis uses CPN Tools formal analysis tools to model the TLS1.3 handshake protocol.The model implements the TLS1.3 handshake protocol random number generation,protocol version selection,pre-master key transmission and mutual identity authentication model.In order to prevent the problem of state space explosion,the range of random numbers is limited,and the asymmetric encryption and decryption process in the protocol is modelled.2.At present,there is certain blindness in the selection of protocol formal analysis methods and protocol analysis tools.This thesis analyzes the structure and security attributes of the EtherNet/IP protocol,and comprehensively an alyzes the performance of protocol formal analysis methods and protocol analysis tools.The analysis tools CPN Tools and Scyther tools analyze the security attributes of the TLS1.3 handshake protocol.It is verified that the security attributes of the TLS1.3 handshake protocol conform to the protocol specifications.Comparing the performance of the two analysis tools from the analysis process and results,CPN Tools has the advantages of refining the protocol content and analyzing the overall protocol in mor e detail in complex protocol analysis.3.The TLS protocol is an important standard protocol to ensure network transmission security and implements data encryption,data integrity,and identity verification.Due to the complexity of the TLS protocol and th e diversity of identity authentication,based on the elliptic curve key exchange method on the finite field,this thesis uses the modelling method of hierarchically coloured Petri net(HCPN)to model the TLS1.3 handshake protocol and adds The Delov-Yao attack model analyzes the state space report under the corresponding model.Experimental results show that the newly released TLS1.3 handshake protocol pre-master key has good confidentiality,and identity authentication meets the security attributes of the protocol specification.Using the Scyther tool to verify that the TLS1.3 handshake protocol did not find an attack shows the urgency of upgrading the TLS protocol in the future EtherNet/IP protocol. |
PDF Full Text Request