A Comprehensive Formal Security Analysis of OPC UA

Vincent Diemunsch; Lucca Hirschi; Steve Kremer

Paper 2025/148

A Comprehensive Formal Security Analysis of OPC UA

Vincent Diemunsch, ANSSI, France, Université de Lorraine, France, French National Centre for Scientific Research, French Institute for Research in Computer Science and Automation, LORIA, France

Lucca Hirschi

, Université de Lorraine, France, French National Centre for Scientific Research, French Institute for Research in Computer Science and Automation, LORIA, France

Steve Kremer

, Université de Lorraine, France, French National Centre for Scientific Research, French Institute for Research in Computer Science and Automation, LORIA, France

Abstract

OPC UA is a standardized Industrial Control System (ICS) protocol, deployed in critical infrastructures, that aims to ensure security. The forthcoming version 1.05 includes major changes in the underlying cryptographic design, including a Diffie-Hellmann based key exchange, as opposed to the previous RSA based version. Version 1.05 is supposed to offer stronger security, including Perfect Forward Secrecy (PFS). We perform a formal security analysis of the security protocols specified in OPC UA v1.05 and v1.04, for the RSA-based and the new DH-based mode, using the state-of-the-art symbolic protocol verifier ProVerif. Compared to previous studies, our model is much more comprehensive, including the new protocol version, combination of the different sub-protocols for establishing secure channels, sessions and their management, covering a large range of possible configurations. This results in one of the largest models ever studied in ProVerif raising many challenges related to its verification mainly due to the complexity of the state machine. We discuss how we mitigated this complexity to obtain meaningful analysis results. Our analysis uncovered several new vulnerabilities, that have been reported to and acknowledged by the OPC Foundation. We designed and proposed provably secure fixes, most of which are included in the upcoming version of the standard.

Note: Accepted for publication at USENIX Security 2025. Artifacts were evaluated and are available at: https://archive.softwareheritage.org/swh:1:dir:cddbdee0ddd129e0eb8dd8479e11c4b131bc3c86;origin=https://github.com/vdh-anssi/opc-ua_security

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. Major revision. USENIX Security 2025
Keywords: formal methods security analysis proverif OPC UA ICS
Contact author(s): vincent diemunsch @ inria fr
lucca hirschi @ inria fr
steve kremer @ inria fr
History: 2025-01-31: last of 5 revisions; 2025-01-30: received; See all versions
Short URL: https://ia.cr/2025/148
License: CC BY-SA

BibTeX

@misc{cryptoeprint:2025/148,
      author = {Vincent Diemunsch and Lucca Hirschi and Steve Kremer},
      title = {A Comprehensive Formal Security Analysis of {OPC} {UA}},
      howpublished = {Cryptology {ePrint} Archive, Paper 2025/148},
      year = {2025},
      url = {https://eprint.iacr.org/2025/148}
}