Formal Security Analysis of OPC UA Protocol in Industrial Control System

Tao Feng ； Zhuang-Yu Ma ； Jun-Li Fang

《International Journal of Network Security》 24卷3期 (2022/05) Pp. 573-585

https://doi.org/10.6633/IJNS.202205_24(3).20

摘要

The OPC UA is a protocol used in the interaction between factory equipment. It is also widely employed in the industrial Internet industry, where long-distance data sharing and transmission between devices, multi-device interconnection, etc., must be realized. Therefore, it is essential to study the security of industrial control system protocol. However, most previous research on industrial control protocols mainly focuses on realizing the security of the protocol itself, lacking formal modeling and security evaluation, leading to some research gaps. Based on the previous colored Petri net theory, combined with the Dolev-Yao attacker model, this paper tries to make targeted improvements to analyze the security of the OPC UA protocol. First, based on the colored Petri net theory and CPN Tools, the security mechanism of the protocol is verified for consistency. Then the Dolev-Yao attacker model is introduced to evaluate the security of the original model of the protocol. By analyzing the security mechanism of the protocol, some issues, including the security of random numbers in OPC UA protocol and the deceptive attack of identity authentication attributes, have been found. Besides, some corresponding improvement projects are given. Finally, we used CPN Tools to verify the security of the new project. We also found that adding the recipient's public key to the message and the key packaging mechanism can effectively prevent attacks against the protocol, improving the protocol's security.

關鍵字

Colored Petri Nets ； Formal Analysis ； Key Packaging ； OPC UA Protocol ； Security Evaluation