<figure><img src="image_1.png" /></figure>

HAL
open science

# A Comprehensive Formal Security Analysis of OPC UA

Vincent Diemunsch, Lucca Hirschi, Steve Kremer

► To cite this version:

Vincent Diemunsch, Lucca Hirschi, Steve Kremer. A Comprehensive Formal Security Analysis of OPC UA. Usenix Security 2025, 2025, Seattle (USA), Washington, United States. hal-04989554

HAL Id: hal-04989554

https://inria.hal.science/hal-04989554v1

Submitted on 13 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Comprehensive Formal Security Analysis of OPC UA

Vincent Diemunsch

Lucca Hirschi

Steve Kremer

ANSSI & Université de Lorraine,
CNRS, Inria, LORIA, France

Université de Lorraine,
CNRS, Inria, LORIA, France

Université de Lorraine,
CNRS, Inria, 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.

## 1 Introduction

Industrial Control Systems (ICS) manage critical infrastructure facilities, such as power plants, and are part of Operational Technology (OT), i.e., covering devices that interact with the physical environment [28]. As opposed to classical Information Technology (IT) systems, OT historically prioritizes safety and reliability, above other security properties such as confidentiality. Moreover, the life cycle of OT systems is much longer, as updates require heavy and costly qualification processes. Severe security incidents, e.g., the Stuxnet [1] worm in 2010, led to adding a security layer (such as Internet Protocol Security (IPsec), or more often Transport Layer Security (TLS) [22]) to existing ICS protocols. However, these

additional security layers are tailored for the Internet and are poorly suited to OT, motivating secure ICS protocols.

Open Platform Communication Unified Architecture (OPC UA) is a general purpose ICS protocol between Supervisory Control and Data Acquisition (SCADA) systems – including operators’ workstations – and automation devices, that regulate an industrial process through sensors and actuators. It is developed by the OPC Foundation and standardized as IEC 62541 (currently in v1.04) [23]. OPC UA has undergone several security analyses by state agencies, such as the German BSI (two analyses in 2017 and 2022 [13, 31]), the French ANSSI (development of the open source implementation S2OPC [29]), as well as by OT security companies that analyzed implementations [8, 9, 30].

OPC UA follows a modular and layered design, where functionalities are activated through profiles. We focus on the OT profile "UA-TCP UA-SC UA-Binary", which is by far the most commonly used [31, § 6.3.4]. This so called OPC UA Binary profile mainly relies on the UA Secure Conversation (UASC) sub-protocol. The protocol is parameterized by a security policy: policies based on Elliptic Curve Cryptography (ECC) have been introduced in version 1.05 of the OPC UA specification. The use of ECC based Diffie-Hellman is supposed to provide stronger confidentiality guarantees, namely PFS, compared to RSA which was the only option previously. In addition, ECC allows for improved performance through shorter keys, which can be crucial for embedded systems. Once a secure channel has been opened, sessions can be created inside this channel. Users can then activate sessions using their credentials and send user requests. OPC UA also allows to re-open existing channels (for key rotation), and re-activate sessions (for transferring to another channel or user).

**Contributions.** In this paper, we perform the first comprehensive, formal security analysis of OPC UA. We leveraged the ProVerif protocol prover [6] to conduct this automated analysis. Our main contributions are as follows.

We provide a detailed description of the security sub-protocols of the OPC UA Binary specification version 1.05
(Sections 2.1 and 2.2), their expected security goals, and the considered threat model (Section 2.3). The relevant security aspects of the specification [23] span 5 documents (out of more than 20), totaling 528 pages. We have extracted what we believe to be a specification suitable for a protocol security analysis. This description is concise, yet comprehensive as it covers both ECC and RSA security profiles (also covering v1.04), sub-protocols for both channel and session establishment, and management, under different configurations (considering different channel modes, session security modes, and user authentication means).

In Section 3, we present our formal model of OPC UA in the applied pi calculus (the input language of ProVerif) which in particular encompasses the following features: (i) the reopening of secure channels, (ii) the reactivation of sessions using passwords as well as user certificates, (iii) the switching of sessions between secure channels, (iv) the authentication of user, client and server involved in a request and its response. This involves dealing with a complex state machine.

We formally specify the security properties (authentication and confidentiality) in Section 3.3. The properties are often tricky to formalize, and we need to condition them by the exact configurations in which a property is expected to hold, as the protocol also allows degraded configurations (that may be deployed simultaneously in other sessions). This also means that our model precisely describes in which configurations and threat models each property is actually expected to hold.

We analyze OPC UA using ProVerif. Given the size and the complexity of our model, and the large number of possible configurations, we provide tooling (Section 4.2) that allows to (i) generate ProVerif models for a particular set of configurations, and threat model; (ii) efficiently explore the lattice of configurations and threat models, and automatically find maximal configurations in which a property holds, as well as minimal configurations in which we find attacks (or reach the limits of ProVerif). Moreover, we used many advanced features of ProVerif [7] to fine tune the model and guide the proof search, to be able to conclude in complex configurations (Section 4.3). We believe that this is among the most complex analyses performed with ProVerif, both due to the size of the model as well as the complexity of the state machine, e.g., the model requires a lot of information to be stored in a global state. To the best of our knowledge, it is the largest ProVerif model in terms of LoC and initial clauses (the internal protocol representation on which ProVerif reasons) ever analyzed.

Our analysis allowed to discover 8 new vulnerabilities and other weaknesses in OPC UA v1.05 (Section 5), 6 of these also affect v1.04. Each of these have been responsibly disclosed to and acknowledged by the OPC UA Foundation. We proposed provably secure fixes and other mitigations, most of them are now included in the specification. Finally, we draw more general lessons for the future of OPC UA (Section 5.7).

**Artifacts.** All models, results, and instructions to reproduce them are provided in the companion artifact [15]. We some-

times cite the full version of this paper [14] where additional details are provided.

# 2 OPC UA Protocol

## 2.1 Overview

We start by presenting the OPC UA protocol version 1.05.03 with a high-level overview of the sub-protocols and their interactions. In this work, we cover the security sub-protocols, namely the secure channel and the session sub-protocols. They are specified in the OPC UA standard, mostly in [23, Parts 4,6,7]. They involve three kinds of agents: *clients* (e.g., user workstations), *servers* (e.g., SCADA), and *users* (e.g., humans operating user workstations). Each agent is assumed to be enrolled in a Public Key Infrastructure (PKI) and possesses a certificate that describes its identity and role (e.g., a client certificate $C_{cert}$) with the associated private key (e.g., $C_{sk}$); users store them on a smart card or may alternatively use a login password pair.

The main flow is depicted in Fig. 1: a client *opens a secure communication channel* with a server and *creates a session* inside this channel. A user on this client can then log in, i.e., *activate* a previously created session, and use this session to send/receive *requests* to/from the server. We now briefly present those sub-protocols.

**Secure communication channels.** Any communication between a client and a server in OPC UA starts by opening a secure channel. While there exists a specific configuration (OPC UA HTTPS) that leverages TLS for this, the more widely deployed profile (OPC UA Binary) has a dedicated channel sub-protocol called UASC. This sub-protocol is made of two parts: (i) a handshake layer, called *OpenChannel* (see Fig. 1), that establishes a new channel ID $id_c$ and a set of symmetric keys $sk$, shared between client and server; (ii) a record layer that protects all subsequent messages with these symmetric keys (depicted by $||.||^{id_c,sk}$). The symmetric keys can be renewed by re-running *OpenChannel* on an existing channel.

Channels can be configured in three Modes:

* Enc: provides integrity and confidentiality.

* Sign: provides integrity only. This can be required for the system to be monitorable by third parties.

* None: insecure channels, which are reserved for scanning the network and debugging.

Finally, a channel *SecurityPolicy* defines the asymmetric and symmetric cryptographic algorithms to use. The protocol supports two families: RSA and ECC. The ECC family offers an Elliptic Curve Diffie-Hellman (ECDH) key exchange that can additionally provide PFS.

**Session creation and activation.** OPC UA sessions provide a user context for requests and their responses.<fnref n="1" /> Sessions are

<footnote n="1">¹There are also sessionless requests, but we choose not to cover them in this work because they rely on issued tokens (see next footnote).</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 1: Overview of the OPC UA protocol: a client opening a secure channel (id<sub>c</sub> with keys sk), creating a session id<sub>s</sub>, and a user U activating it. Sub-protocols, which will be detailed later, are indicated in red, and protocol configurations in blue. ||·||<sup>id<sub>c</sub>,sk</sup> denotes channel protection, that depends on the channel configuration (Encryption&Signature | Signature | None).</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 2: Overview of the OPC UA state machine</figcaption></figure>

created by a client in a channel (see CreateSession in Fig. 1), and yield a session identifier *id*<sub>s</sub> and a session token *tok*<sub>s</sub> (explained in Section 2.2.2). The options (SSec | SNoAA) define the security level provided by the session and will be explained later in Section 2.2.2. Created sessions can be activated (see ActivateSession) directly by the client with the anonymous user (Ano), or by a regular user. Regular users rely for this on login password pair (Pwd) or a certificate (Cert), which may be stored on a smart card for better security (see NIST [28] § 6.2.1.4.3).<fnref n="2" />

**State machine.** There exist various ways for channels and sessions to evolve and the resulting state machine, depicted in Fig. 2, is rather complex and further complicated by the various configurations that can be arbitrarily combined: (RSA | ECC + Enc | Sign | None + SSec | SNoAA + Pwd | Cert | Ano). Once opened, a channel can be *Reopened*, by running *OpenChannel* on the existing channel, resulting in

a key renewal. Sessions can then be created and activated on any channel. By running ActivateSession on a previously activated session, users can:

*   **ReActivate**: hand over sessions to other users (e.g., at shift change), or

*   **Switch**: transfer them to a new secure channel (e.g., in case the previous channel was terminated).

Such complex operations are required for increased reliability, which is key in OT systems (see [14, B.1]).

## 2.2 Protocol Description

For the sake of clarity, we first present the different sub-protocols when SecurityPolicy is set to ECC and Mode to Enc, and then explain the main differences with other configurations. We refer the reader to [14, B] for their detailed description.

**Cryptographic Schemes.** We use the following notations for cryptographic operations. $[m]_{sk}$ denotes the signature of $m$ with the private key $sk$, $\{m\}_k$ the symmetric encryption of $m$ with the key $k$, and $[m]_{mk}$ the addition of a Keyed-Hash Message Authentication Code (HMAC) with key $mk$. The choice of the precise cryptographic suite implementing those depend on server configuration. E.g., for SecurityPolicy [ECC-B] ECC-nistP256 [24], they are respectively instantiated with ECDSA-SHA2-256, AES128-CBC and HMAC-SHA2-256. More importantly for this work, the combination of HMAC and symmetric encryption roughly follows the MAC-then-Encrypt construct with some data in plaintext. Formally:

$$[m, \{p\}_{ek}]_{mk} := m, \mathrm{AES}_{ek}(p, \mathrm{HMAC}_{mk}(m, p)).$$

The case of profiles with authenticated encryption schemes (a minority of profiles: 3 over 11) is a bit different (see [14, B.2]) and is left as future work.

### 2.2.1 UA Secure Conversation

We now present the UASC sub-protocol, including OpenChannel, see Fig. 3. The first two messages are for channel opening or reopening, and the last two are for requests and responses sent over the created channel. The requests that can be sent over the channels are described in Section 2.2.2.

**Channel (re)opening.** To open a secure channel, the client sends an *OpenSecureChannel* request. This request notably includes the client's certificate $C_{cert}$ and is signed with the associated private key $C_{sk}$. The channel ID $id_c^0$ is initially set to 0 to indicate that a new channel should be opened. There is also a counter $Rq$, incremented at each request. Finally, the request includes the Diffie-Hellman (DH) half-key $C_{hk} = g^c$, from which the shared secret will be derived.

The server checks the client certificate and the signature of the client request. Its response is similar, but includes its own certificate $S_{cert}$ and half-key $S_{hk} = g^s$. The server also chooses a new, fresh channel ID $id_c$ (a counter) and $tok_c$ (a nonce). The former identifies the channel, while the latter

<footnote n="2">²Another user authentication mode uses issued tokens (e.g., WS-SecurityTokens (Kerberos), JSON Web Token (JWT) or OAuth 2 tokens). They rely on authorization services, that are protocols in their own rights. However, issued tokens details are neither specified nor included in the security profiles of version 1.05. Hence, we do not cover them here, and rather focus on the two core OPC UA user authentication methods.</footnote>
identifies the shared secret sk that will be derived. sk is computed by a Key Derivation Function (KDF) of the shared DH secret $g^{c \cdot s}$. More precisely, two keys for encryption ($sk.C_{esk}$ and $sk.S_{esk}$) and HMAC ($sk.C_{msk}$ and $sk.S_{msk}$) are derived. The client checks the server certificate and the signature of the response and derives sk as well. ($id_c$ is included twice.)

An existing channel with ID $id_c^{old}$ can be reopened by a client by choosing $id_c^0 := id_c^{old}$ (instead of zero). The server will then choose a new security token $tok_c'$ but keep $id_c = id_c^{old}$. The client must reopen before the channel lifetime (depending on server configuration) expires.

**Message security.** Once a channel is open, client and server can send requests and responses, which are wrapped and cryptographically protected as shown in the last two messages of Fig. 3. In particular, reusing notation from Fig. 1, $||\text{request}||^{id_c,sk} := [\text{MSG}, id_c, tok_c, \{Rq', \langle request \rangle\}_{sk.C_{esk}}]_{sk.C_{msk}}$.

**Other configurations.** When SecurityPolicy = RSA, the client and server exchange nonces $C_{nonce}^c$ and $S_{nonce}^c$ instead of DH half-keys. Those nonces are asymmetrically encrypted with the receiver's public key and are sent along with the hash of the public key used for encryption. When Mode = Sign, the encrypted parts are in plaintext in MSG messages. When Mode = None, signatures, HMAC, encryption, certificates, and half-keys (or nonces) are omitted in all messages. See a detailed description of those configurations in [14, B.2].

### 2.2.2 Sessions

We now describe the CreateSession and ActivateSession sub-protocols (both depicted in Fig. 4). The first two messages allow the creation of a session, the third and fourth its activation, and the last two describe how user requests, at the application layer, are wrapped in a session. We stress that all those messages are sent over and protected by some channel, and act as $\langle request \rangle$ and $\langle response \rangle$ of that channel, cf. Fig. 3.

**Session creation.** The client sends a Create request with a fresh nonce $C_{nonce}$ and $C_{cert}$. The server checks that the client certificate is the same as the one associated to the channel through which this message is sent (this client certificate was sent in the OpenChannel request). The server response provides a new, fresh session ID $id_s$ (a counter) that will identify the session. It also includes a fresh Session Authentication Token $tok_s$ (a nonce) that serves the same purpose as $id_s$ but is supposed to be kept secret. A fresh server nonce $S_{nonce}$ is provided and acts as a challenge to the client for the next session activation. The server also proves possession of his certificate, by signing $C_{cert}$ and $C_{nonce}$ with $S_{sk}$. Finally, a signed fresh DH half-key $S_{ek} = [[g^s]]_{S_{sk}}$ is added in an additional field for later use, should the session be activated in configuration Pwd (described next). If all checks pass, clients and servers notably store the session information: $id_s, tok_s, id_c$ ($id_c$ refers to the channel on which the messages were sent).

**First activation.** Once created, a user can activate a session

<figure><img src="image_5.png" /><figcaption>Figure 3: (Re)Open Secure Channel (first two messages) and Channel Communications (last two) in (ECC + Enc). OPN is a header string. After the first two messages, client and server can derive a set of symmetric keys sk containing encryption keys $C_{esk}$, $S_{esk}$ and HMAC keys $C_{msk}$, $S_{msk}$. The last two messages describe the channel protection of subsequent requests/responses payloads $\langle request \rangle/\langle response \rangle$ (cf. Section 2.2.2).</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Figure 4: Session creation (first two messages) and activation (third and fourth) and user requests/responses (last two) in (ECC + Enc + SSec + Cert). The session activation involves the user to produce the signature with $U_{sk}$. Create and Activ are header strings. The last two messages describe how user requests $\langle Urequest \rangle$ and responses $\langle Uresponse \rangle$ payloads, from the application layer, are wrapped in a session.</figcaption></figure>

($id_s, tok_s, id_c$) by sending an Activ request. This request includes $tok_s$ and a signature of $S_{cert}$ and $S_{nonce}$, sent in the previous session creation response, to prove possession of $C_{sk}$. In mode (Cert) (as in Fig. 4), the request must also contain the user's signature (with $U_{sk}$ associated to $U_{cert}$) of $S_{cert}$ and $S_{nonce}$. In practice, the signature can be computed on the user's Smart Card. The server verifies the signatures and responds with fresh $S'_{nonce}$ and $S'_{ek}$ for future reactivations.

**User requests and responses.** User requests $\langle Urequest \rangle$, produced by the application layer, are wrapped in a session by appending the session token $tok_s$. The user response $\langle Uresponse \rangle$ can then be linked to that session as well, since the response will use the same $Rq$ at channel level. Indeed, recall that such session requests are additionally sent through, and cryptographically protected by, some secure channel.

**Reactivation and channel switching.** Session handover to another user is achieved by sending an activation request referring to a previously activated session, on the same client
and channel, but for a different user. Similarly, the switching of secure channel is an activation of the same session, on the same client by the same user, but carried out on a different secure channel, with the same security Mode and the same client and server certificates.

**Other activations.** In configuration Ano, $U_{cert}$ and the signature with $U_{sk}$ are omitted and the session is not bound to a user. In configuration Pwd, $U_{cert}$ is replaced by a login and the user's signature is replaced by the password encrypted with a symmetric key derived from the latest $S_{ek}$ and some fresh client DH half-key, both sent together with this ciphertext. When Mode = RSA, the only difference is that $S_{ek}$ is omitted and, when necessary, the password is instead asymmetrically encrypted with the server's public key. Note that in configuration Enc, the password may be sent without symmetric encryption (i.e., sent as plaintext at the session layer), as encryption is provided at the channel level.

**Session security.** We now explain the differences between SSec and SNoAA. By default, in SSec, server and client certificates are exchanged and trust checked against the PKI, at session creation and activation. However, the specification also defines a *No Application Authentication mode* [23, Part 7, § 5.3], where the server is configured to accept all certificates and only use them for message security. We call this mode SNoAA. We provide further details about SNoAA and the other aforementioned configurations in [14, B.3].

## 2.3 Security Goals

In this section, we describe the security goals of OPC UA, and the threat model under which these goals should hold as described in [23, Part 2 "Security Model"). In [14, B.4], we provide more evidence, with references to the specification, supporting our interpretations.

### 2.3.1 Threat Model

We first summarize the threat model in terms of attacker capabilities and compromise scenarios detailed in [23, Part 2, § 4.3 "Security threats to OPC UA systems"). OPC UA is claimed to resist the following threats: eavesdropping (§ 4.3.3), message spoofing (§ 4.3.4), message alteration (§ 4.3.5) and replay (§ 4.3.6), emitting malformed messages (§ 4.3.7). The attacker is also able to set up a rogue server (§ 4.3.10), and to act as a MiM (§ 4.3.9). Therefore, we shall consider an *active adversary on the network* who can eavesdrop, intercept, manipulate, and inject messages. Such an attacker is often referred to as a *Dolev-Yao attacker* [16].

Moreover, user credentials (passwords, or certificate private keys) may be compromised (§ 4.3.12). Client and server certificates and associated private keys are also considered as potentially compromised [23, Part 4, § 6.1.4]. In short, the attacker can compromise agents' long-term secrets. Channel symmetric keys $sk$ are more ambivalent: their lifetime depends

on a parameter (i.e., revisedLifetime) spanning from a few minutes to 40+ days and is not enforced by security profiles. We conservatively consider those keys as semi-long-term. We do not consider compromise of such keys by default, but will allow such compromise in specific cases (password confidentiality), when mentioned explicitly. However, full attacker control of a machine, allowing ephemeral secret leaks (e.g., DH client's secret $c$), remains out of scope [23, Part 2, § 4.4].

### 2.3.2 Security Properties

We now discuss the security properties that OPC UA is supposed to guarantee as per [23, Part 2, § 4.2 "Security objectives"] (with additional supporting evidence in [14, B.4]).

**Confidentiality.** Secure channels with Mode = Enc must provide confidentiality of data exchanged on the network: user requests and responses. Passwords must remain confidential for all channel modes. Moreover, channels configured with ECC additionally provide PFS, i.e., any message exchange prior to the compromise should remain secure. To sum up, OPC UA is expected to guarantee that: (i) *The attacker cannot learn the user requests and responses payloads when sent over channels in configuration Enc.* (ii) *PFS is guaranteed for the payloads sent over channels in configuration (ECC + Enc).* (iii) *The attacker cannot learn the user passwords.*

**Integrity and Authentication.** Integrity and authentication of user requests are key requirements for OPC UA [23, Part 2, § 4.2,5.1.1]. We express those more formally as *agreement properties* in Lowe's authentication taxonomy [21], where properties are expressed as relations between different agents' point of views of a protocol execution. Data and entity authentication can be expressed as a single, strong *agreement property*: *if a server S accepts a user request R supposedly from a user U on client C, then U has indeed initiated request R for server S on C.* Conversely, *if a user U receives on client C a user response R supposedly from server S, then S has indeed responded with R to client C for user U.* As the protocol is supposed to protect against replays, we moreover require that these agreements are *injective*, i.e., each received request corresponds to a distinct request emission.

## 3 OPC UA Formal Model

### 3.1 Proverif Background

In ProVerif, protocols are formally modeled in a dialect of the applied pi-calculus. Messages are abstracted by terms, to focus on their functionality e.g., a ciphertext perfectly hides its plaintext, unless the attacker knows the decryption key. Protocols are described by parallel processes, that model message exchanges and verification steps performed by agents. Finally, public communication channels are fully controlled by a Dolev-Yao attacker who can intercept, send, but also forge new messages. Given a security goal, ProVerif either returns
true if security is proved, or false and automatically produces an attack trace, or may return cannot-be-proved in some cases where an attack cannot be reconstructed (due to internal abstractions). Moreover, ProVerif may not terminate, since the underlying problem is undecidable. Below, we briefly recall the main concepts of ProVerif's syntax and semantics and refer the reader to [7] for a comprehensive description.

**Messages.** In symbolic models, messages are abstracted by formal terms in a term algebra. For example, a digital signature scheme is modeled by the function symbol `sign(·, ·)` and the term `sign(m, k)` represents the signature of message `m` using the secret key `k`. Similarly, signature verification is modeled by two additional function symbols: `checkSign(s, pk(k))` is the application of the verification algorithm, on the signature `s` and the public-key `pk(k)` associated to `k`. Finally, the expected functionality of a digital signature, i.e., the fact that the verification of a valid signature succeeds, is expressed by an equation: `checkSign(sign(m, k), pk(k)) = true`. We additionally provide the means to retrieve the signed message with a function symbol `readSign(·)` and equation `readSign(sign(m, k)) = m`. One can similarly model DH exponentiation, with function symbol `exp(·, ·)` and constant `g` representing the group generator. The equation `exp(exp(g, x), y) = exp(exp(g, y), x)` expresses that exponents commute.

**Protocol roles.** ProVerif relies on a process calculus to model the roles of a protocol. We illustrate the syntax on an example. Consider the Server role in the UASC sub-protocol, where the server receives an initial *OpenChannel* request from a client, and sends back a corresponding response message. A process modeling such a server running with *SecurityPolicy* *ECC* could be specified as follows (some parts are omitted with `[...]` for brevity):

1. `let Server(S_cert: cert, S_sk: skey) =`
2. `in (c, OPN_req: bs);`
3. `let (=OPN, =zero, =ECC, C_cert: cert, Rq: nonce, mode: chmode, C_hk: G) = readSign(OPN_req) in`
4. `if checkSign(OPN_req, get_pk(C_cert)) then`
5. `new s: ex; new tok_c: chtoken; new id_c: chid;`
6. `let S_hk = exp(g, s) in let seed = exp(C_hk, s) in`
7. `let C_enc_k = enc_key_ECC(seed) in [...]`
8. `let symkeys = (tok_c, C_enc_k, [...]) in`
9. `event NewSharedKey(C_cert, S_cert, mode, seed);`
10. `insert Schan(C_cert, S_cert, ECC, mode, id_c, symkeys);`
11. `let OPN_re = (OPN, id_c, ECC, S_cert, Rq, id_c, tok_c, S_hk) in`
12. `out(c, asign(OPNresp, S_sk)) [...]`

The *Server* process, parametrized with a certificate `S_cert` and an associated private key `S_sk` (line 1), initially waits for a message `OPN_req` from a client (line 2) on a public channel `c`; `cert`, `nonce`, `chmode`, and `G` are the expected types<fnref n="3" />. The server extracts the different fields from the message and checks that they contain the header string `OPN`, a channel ID set to `zero` and that `SecurityPolicy = ECC`; other fields are bound to the variables `C_cert`, `Rq`, `mode`, and `C_hk` (line 3). Next, it checks the signature (line 4). If all those checks succeed, the server generates new *names* that are fresh values, namely a

new ephemeral secret, channel identifier, and token (line 5), and computes the shared DH key and associated symmetric channel keys `C_enc_k`, etc. (lines 7, 8). The server then logs the fact that a new shared key has been computed with the event `NewSharedKey` (line 9). *Events* are used to model security properties (see next paragraph). The server also stores the channel information in a *table* `Schan` (line 10) and computes the *OpenChannel* response that is signed (line 11) and output to the client (line 12). *Tables* are used to store evolving states of the different agents. For instance, the table `Schan(C_cert, S_cert, ECC, mode, id_c, symkeys)` stores the channels, that have been opened by the server identified by the certificate `S_cert`. When the server receives the *CreateSession* request in the session sub-protocol, it will retrieve the channel information from this table, e.g., a server with certificate `S_cert` can retrieve `symkeys` and `C_cert` of a channel identified by `id_c` with: `get Schan(C_cert, =S_cert, sec_policy, mode, =id_c, symkeys)`.

**Security Properties.** Intuitively, events are merely annotations in execution traces that record some specific steps of the protocol. Security properties are then expressed as logical formulas over events. E.g., the following formula expresses the impossibility for an attacker to learn some shared secret *seed*, that has been computed for securing a channel in mode *Enc* by a server, and hence is logged in a *NewSharedKey* event: `event(NewSharedKey(S_pk, C_pk, Enc, seed))&& attacker(seed)==> false`.

Note that *attacker(seed)* is true whenever the adversary can compute the value of *seed*. The attacker is able to compute new terms by applying function symbols on previously observed outputs. This property thus models confidentiality of *Enc* channel shared secret keys, from the point of view of a server.

## 3.2 Modeling in the Applied Pi Calculus

We now discuss our formal model of OPC UA [15], and explain some of our modeling choices. As a general guideline, we strive to make attack conservative choices. For example, when the specification allows several options we allow all of them, or choose the least secure one.

**Overall architecture of processes.** Our model is based on three main processes, one for each kind of agents (users, clients and servers), running in parallel. We consider an unbounded number of agents, and each agent may engage into an unbounded number of protocol sessions. E.g., A client may start an arbitrary number of sessions with different servers.

Each of these main processes contains subprocesses for specific tasks. The client process allows to (re)open channels and create sessions. The user process allows to activate session (using user's credentials) and send/receive user requests/responses. The server process handles the different kinds of requests (channel (re)opening, session creation, (re)activation and channel switching, as well as user requests). As the scheduling is adversarial, the attacker decides which actions are triggered and which agents execute a given sub-protocol.

<footnote n="3">³Note that although the language is typed, the attacker is allowed to send ill-typed messages and ProVerif does capture type flaw attacks.</footnote>
**PKI, user passwords and compromise.** When an agent is created, it is enrolled in a PKI. The PKI issues a certificate modeled by a private function, i.e., a function that the attacker is not allowed to apply: *fun certify (kind,crypto,pkey): cert [private]*. A certificate specifies the *kind* of agent (Client, Server, or User), the *crypto* family RSA or ECC as well as the public key *pkey*. For each new user, a fresh password is also created.

At any time, we allow the attacker to compromise an agent. Compromise of agent A triggers the event *leak(A)* and results in the output of A's secret key, and password if A is a user.

**Local state and tables.** As illustrated in Fig. 2, the state machine is rather complex, and yet fully captured by our model. We use tables to store the local states of the protocol agents. In particular, we use tables for recording the list of channels that were opened and sessions that were created/activated by a client or server. Note that we distinguish these tables for clients and servers as their view may not coincide.<fnref n="4" /> We introduced 4 tables in total: channels and sessions for clients and servers. This way, were able to fully capture the OPC UA state machine, which will, however, make the reasoning and proof search extremely complex and will require a carefully designed proof methodology (see Section 4).

**Modes and configurations.** Our model is designed to be modular and allows to enable/disable the modes and features that are to be supported. We can set the *SecurityPolicy* (ECC or RSA), channel modes (None, Sign or Enc), the session security level (SSec or SNoAA), as well as the supported user creden- tial modes (Pwd, Cert or Ano). For example, the configuration (RSA | ECC + Enc | Sign | None + SSec | SNoAA + Cert) sup- ports all kind of crypto, channels, and session modes as well as user identification through certificates. However, anonymous and password-based login are excluded. Further parameters allow to enable or disable agent and channel keys compromise, reopening of channels, and channel switching. Regarding the two admissible behaviors for password encrypt- ion in Enc channels mentioned in Section 2.2.2 (double encryption or only channel encryption), we conservatively chose the least secure option (channel encryption only).

Being able to use such parameters has proven to be ex- tremely useful to establish our proof methodology (Section 4). We stress that we aim to obtain results with respect to a rich model with almost all modes enabled (although we sometimes consider some option values in isolation).

**Size of the model.** The complexity of our model is also re- flected by its size: while the ProVerif files were written in a modular way that amount to 2.4k LoC (including all decla- rations and property definitions), the unfolded process that ProVerif generates to reason corresponds to 8.6k LoC that are translated into 2.3k initial clauses (for the full configuration when verifying a confidentiality property). As a point of com- parison the most comprehensive model of TLS 1.3 [5] has an

unfolded process of 7.3k LoC translating to 1.4k clauses.

## 3.3 Formal Security Properties

In this section, we explain how we formally modeled in ProVerif, the security properties identified in Section 2.3.2.

**Conf<sub>C</sub> and Conf<sub>S</sub>: Confidentiality of user requests and responses.** When *Mode* = *Enc*, user requests and the corre- sponding responses are supposed to be confidential. In addi- tion, when *SecurityPolicy* = *ECC*, the protocol is expected to provide PFS. These requirements are formalized as follows, where *C_data* is an event triggered by clients whenever they send/receive a user request/response *R*:

```
event(C_data(C_pk, S_pk, SecPo, Enc, SE, R))@t && attacker(R)
==> event(leak(S_pk))@ts && (SecPo = RSA || ts < t)
```

For any user request *R* sent at time *t* in a session *SE* with *Mode* = *Enc*, such that *R* is known to the attacker, it must be that the peer has been compromised (*leak(S_pk*)). Moreover, if the *SecurityPolicy* (*SecPo*) is not *RSA*, and thus is *ECC*, then *PFS* requires that the leak must have occurred *before* the request (*ts* < *t*). A similar property models the confidentiality from servers' point of view, using an event *S_data* triggered whenever a request/response is received/sent. We respectively call those two properties *Conf<sub>C</sub>* and *Conf<sub>S</sub>*.

**Conf<sub>Pwd</sub>: Confidentiality of passwords.** A second confiden- tiality requirement is that passwords remain secret:

```
event(new_user(U, pwd, U_sk, U_pk, U_cert)) && attacker pwd
==> event(leak(U_pk)) ||
    ( event(C_Activ_req(C_pk, S_pk, mode, check, SE, U, pwd)) &&
      event(leak(S_pk)) )
```

The property states that for any declared user, if the attacker knows her password, then one of the following must have happened: (i) the user has been compromised, or (ii) the pass- word has been used by a client to activate a session (event *C_Activ_req*) with a compromised server *S_pk*. Indeed, in both cases the password is trivially leaked. Otherwise, we expect the password to remain confidential.

**Agr<sub>S</sub> and Agr<sub>C</sub>: Data and entity authentication of user requests and responses.** Finally, we model authentication of user requests. As discussed in Section 2.3.2, this property is an injective agreement property:

```
inj-event(S_Rcv_User_Req(C_pk, S_pk, SE, U, R))
==> inj-event(C_Snd_User_Req(C_pk, S_pk, SE, U, R))
|| ( event(leak(C_pk)) || mode = None) &&
    ( U = anon || event(leak(U)) ||
      event(C_Activ_req(C_pk, S_pk, mode, check, SE, U, pwd)) &&
      event(leak(S_pk)) )
```

The property states that, whenever the server *S_pk* receives a request *R* from a user *U_pk*, sent on a client *C_pk* in a session *SE*, then *U_pk* did indeed send *R* to *S_pk* in session *SE* or the attacker can impersonate the user and either (a) the client was compromised (*leak(C_pk*) or (b) the channel mode is *None*. To impersonate the user we have to consider three cases: (i) either the session is anonymous, *i.e.*, there is no user, or (ii) the user credentials have been leaked, or (iii) the user did use his password to authenticate to a corrupted server (on an arbitrary client). By declaring the agreement to be injective, we ensure

<footnote n="4">⁴However, user processes have access to client tables (users can access local clients' states they use and control).</footnote>
that any user request event on the server side corresponds to a distinct user request event on the client side. This is called Agr<sub>S</sub>. The opposite property, Agr<sub>C</sub>, is also modeled and starts with a C_Rcv_User_Resp, ends with a S_Snd_User_Resp event, and is simply conditioned by || event(leak(S_pk)).

**Sanity checks.** In addition, we deploy a number of sanity checks to ensure the validity of our model. We check that all expected protocol flows are indeed executable in each of the configurations (encoded as reachability of events). For each of the security properties we also verify that the property is indeed violated when not conditioned correctly, e.g., removing event(leak(U_pk)) in Conf<sub>wd</sub>. Finally for each correspondence property H ===> C we check that the hypothesis H can be satisfied as otherwise the property would trivially hold.

# 4 Proof Methodology

We now present our analysis methodology, and some of the more advanced proof techniques we developed to overcome the complexity of our model. Those were pivotal to produce any meaningful analysis, as ProVerif was initially unable to successfully conclude, even for simplified configurations.

## 4.1 Protocol Configurations and Modularity

In order to isolate the different model features that were challenging for ProVerif to analyze, we developed a modular protocol model that allows to choose: (i) a particular protocol configuration, (ii) the possibility for compromise of long-term keys (Ltk) and/or channel keys (Chk), or no key leakage at all (Nok), (iii) to turn on (T) / off (F) channel reopening and session switching. We summarize them in Table 1.

Note that a protocol configuration may enable multiple admissible values at once, e.g., a deployed server may be configured to accept either ECC, RSA, or both. The protocol simplifications obviously allow to simplify the automated analysis by disabling some features. They also allow to minimize attack traces and narrow down the exact protocol features that are required to trigger a vulnerability. We use a preprocessor, based on a Python Jinja template engine, to generate the model corresponding to the chosen configuration. As each of these model options are pairwise independent, we end up with 7 056 possible configurations and as many models.

## 4.2 Systematically Exploring Configurations

As we shall see, the set of model configurations (see Table 1) forms a lattice with a single maximal element. Formally, we first define an order relation over configuration options as the set inclusion for protocol configuration and key leakage options (e.g., Sign < Enc | Sign) and F < T for the other options. The order over configurations is then defined point-wise. Given a configuration c, we denote by c<sup>↑</sup>, respectively c<sup>↓</sup>, its upward, respectively downward, closed set.

<table><caption>Table 1: Model configurations are defined by setting (possibly multiple) admissible values to each configuration option. The first four lines correspond to protocol configurations, the fifth line allows to enable/disable key leakage, and the last two lines correspond to protocol simplifications.</caption><thead><tr><th>Configuration option</th><th>Admissible values</th><th># configurations</th></tr></thead><tbody><tr><td>SecurityPolicy</td><td>(ECC | RSA)</td><td>3</td></tr><tr><td>Mode</td><td>(Enc | Sign | None)</td><td>7</td></tr><tr><td>SessionSecurity</td><td>(SSec | SNoAA)</td><td>3</td></tr><tr><td>UserAuthentication</td><td>(Cert | Pwd | Ano)</td><td>7</td></tr><tr><td>Leak</td><td>(Ltk | Chk / Nok)</td><td>4</td></tr><tr><td>Reopen</td><td>(T | F)</td><td>2</td></tr><tr><td>Switch</td><td>(T | F)</td><td>2</td></tr></tbody></table>

We developed a Python script to efficiently explore the verification of all configurations for a given property, and extract maximal configurations for which the property holds, minimal configurations for which the property does not hold, i.e., an attack is found, as well as minimal configurations for which ProVerif does not terminate successfully, i.e., either returns cannot-be-proved or exhausts a given resource (time or memory) budget. Indeed, whenever a property holds on a configuration c, the property holds on any configuration in c<sup>↓</sup> (as all traces in these configurations are included in the traces of c). Conversely, when a property is falsified on c, it is falsified on c<sup>↑</sup> as well. As a heuristic, we assume that when ProVerif does not successfully conclude on c it will neither conclude on configurations in c<sup>↑</sup>.

As ProVerif may not terminate, we allocate a maximal time and memory budget. We start with a small resource budget (a few seconds and MO of RAM) that allows to quickly explore the lattice and often prune large parts on which ProVerif efficiently concludes. Our script then iteratively increases the budget and re-explores the configurations that exhausted the previous budget (more details in [14, D.1]). Moreover, our script allows to explore the lattice in parallel on multiple CPU cores. This lattice exploration script is reminiscent to previous work, e.g., [18, 19] that faced similar challenges, but we push these ideas further with variable resource allocation and exploration heuristics (iteratively increasing resources).

## 4.3 Advanced proof techniques

As mentioned above, due to the complexity of the model, ProVerif fails to successfully conclude on most properties and configurations except for the most basic ones, e.g., when only Mode = None is enabled as no secure channel can be opened in such a trivial case. To obtain meaningful results, we thus had to use a number of existing, advanced features that allow to fine-tune the generation of Horn clauses and the resolution underlying ProVerif's proof search. The authentication properties were particularly challenging and required what we
believe to be a novel proof methodology combining existing
features in order to successfully prove them.

4.3.1 Advanced features

In order to finitely represent the potentially unbounded number
of fresh values a *name* can have, ProVerif uses a sound ab-
straction: a *name* `new n` is internally represented as a function
of all previous (in the syntax tree) inputs, table accesses and
(internal) replication indices resulting in a term. It is possible
to fine-tune such contexts without impacting the model se-
mantics; i.e., ProVerif is sound independently of the contexts.
Larger contexts generally enlarge the verification complexity
but yield more precise results, that is ProVerif will less likely
return a *cannot-be-proved* result. Smaller contexts can drasti-
cally reduce the verification complexity, and even address non-
termination issues, but can result in more *cannot-be-proved*.
For our model, we have modified the context of 34 out of 39
new names, often to mitigate non-termination issues. In some
cases, different properties required different name contexts;
this is handled by our Python script generating the model for
a given configuration and property.

Similarly, internal abstractions on inputs may hamper
ProVerif's ability to conclude. Adding a [precise] statement on
selected inputs was often required for the attack reconstruc-
tion to succeed. Such statements instruct ProVerif to generate
clauses with additional information. However, the additional
precision significantly degrades performance and required
to fine-tune when to use it (depending on the property and
configuration being proved).

We also had to design *lemmas*. Lemmas use the same syn-
tax as security properties (queries) and are mainly invariants
on the protocol, whose validity is first checked by ProVerif.
Lemmas are then applied during the proof search when prov-
ing queries by providing additional information. The most
basic lemmas are of the form *not attacker(t)*, which specifies
that the attacker is unable to learn *t*. We have introduced such
lemmas notably to express the secrecy of the DH exponents
in the protocol which significantly speed up the verification.

4.3.2 A novel proof methodology

Despite the addition of proof helpers as described above, the
verification did not terminate for authentication properties on
most configurations. Introspection of the ProVerif’s proof
search procedure revealed that it was looping, due to the mod-
eling of sessions in tables and the actual loops in the protocol
state machine. For instance, to (re)activate a session, a table
entry of a previous session is necessary and a new entry of the
updated session is created. Hence, insertion of a table entry
requires the existence of a table entry. We therefore applied
the following principled methodology that is quite effective at
thwarting such loops, a recurring issue in complex protocol
verification. We exemplify the methodology in Appendix B.

A more detailed presentation, also recalling background on
ProVerif’s verification method, is given in [14, D.2].

**Step 1: Identify the loops.** When a proof seems to loop, the first step is to identify on which facts ProVerif's resolution procedure loops. In the output log (using verbose mode), we manually inspect if a fact is selected in most resolution steps, past the first few resolution steps that are not looping yet. This way, we extract one or a few candidates facts to break the loop.

**Step 2: Adding noselect statements to break the loops.** We now add a `noselect` statement for the identified fact. In our case study, we added such statements on `table(S_sessions(...))` and `table(C_sessions(...))` facts. We then re-run ProVerif and check if the proof terminates. If it does not, we repeat steps 1 and 2 until the proof terminates. If it does, it is very likely that ProVerif now returns a `cannot-be-proved`. We explain in the next steps how to deal with this.

**Step 3: Collecting false assumptions.** Since facts with `noselect` statement are not selected anymore, ProVerif has "no clue" about the terms in those facts. For example, for table facts, ProVerif will not be able to infer which table entries are actually possible by the protocol. More generally, without the ability to trace back from where a fact (under `noselect`) originates, it conservatively assumes those facts could initially contain arbitrary terms, leading to "false attacks".

Fortunately, ProVerif explicitly describes the assumptions
about these facts in the *goal reachable* and the *derivation*
provided in the case of *cannot-be-proved*. Those show the
clause that falsifies the property and the derivation yielding
this clause. In the hypotheses of this clause, one should manu-
ally inspect the terms in the `noselect` facts. A manual inspection
reveals what are the "false assumptions", namely the assump-
tions that (i) ProVerif took because of the `noselect` statements,
but (ii) are impossible to obtain in normal executions of the
protocol. For example, we observed distinct session tables
with the same client signing key, but that differ on the remain-
ing channel keys. This is however impossible since all channel
keys are derived from the same seed in the protocol.

**Step 4: Design invariants contradicting the false assumptions.** Once a false assumption is identified, we write an invariant that states that these assumptions are actually false. Such invariants can be stated in ProVerif as an *axiom* that will be applied on the clauses during the resolution. Writing the invariant boils down to express the contradiction of the false assumption. For example, we can state the invariant that if two session table entries coincide on the client signing key then remaining channel keys must also be equal. Identifying the false assumptions and stating the invariants is generally an iterative process. To ensure soundness, we use ProVerif to prove that these invariants indeed hold, see next step.

**Step 5: Proving the invariants.** Once enough invariants
are added and allow ProVerif to conclude the proof of the
main property (without cannot-be-proved), we need to prove the invariants themselves. Indeed, since axioms are assumed to hold by ProVerif, adding an invariant that does not hold could lead to wrong results. Hence, we let ProVerif prove each invariant. This is done by removing the `noselect` statements added in Step 1 and declaring the axioms as queries. (These modifications to the files are handled by our script that declares the invariants as axioms when proving the main property and declares them as queries when checking their validity.)

**Optional: Chaining invariants.** Note that for proving some invariants, ProVerif may require other invariants. In this case, we follow the same methodology where the main query becomes the invariant whose proof loops. Once this is completed, we can declare the new invariant as an axiom and prove the main property. We repeat this process until all invariants are proven and the main property is proven assuming those invariants. Resulting from this is a *dependency graph*. To ensure soundness we make sure this dependency graph is indeed acyclic, i.e., it is a *Directed Acyclic Graph (DAG)*.

**Soundness.** We emphasize that our methodology is sound and results in a fully checked proof. Soundness relies on the fact that all axioms are first proved as queries before being assumed, and that ProVerif guarantees soundness independently of name contexts and other proof options (see [14, D.2]).

# 5 Analysis Results

We have leveraged ProVerif to analyze the properties stated in Section 3.3. Our analysis uncovered several vulnerabilities affecting OPC UA version 1.05.03, some of them also affecting version 1.04. Each of these vulnerabilities, and the fixes we have designed to address them, have been responsibly disclosed to the OPC Foundation. Then, during the embargo period, we discussed with the Foundation (through their ticketing system, emails, and attending their working group meetings) the different fixes and their impact on existing implementations. The Foundation decided to keep most of them, which are now part of the updated specification v1.05.04 RC (Release Candidate). As we shall explain in detail, some of the vulnerabilities have not been entirely fixed (mostly for backward compatibility reason) and some residual risks remain. Therefore, we had to weaken the properties *Agr<sub>S</sub>* and *Agr<sub>C</sub>* we could prove on the updated specification, to reflect these residual risks. Excluding those residual risks, we show that our fixes do indeed avoid these attacks in the configurations for which we initially found them.

We detail the found attacks, their impact, root causes and remediation in Table 3. We summarize our formal findings in Table 2 and detail below the scope of our formal proofs. For each of the vulnerabilities, we add links to tickets that describe follow-up actions and modifications to the standard resulting from our disclosure and the discussions with the OPC Foundation. Since the vulnerabilities and weaknesses we

<table><caption>Table 2: Summary of our automated security analysis with respect to the properties from Section 3.3. X: an or several attack(s) are automatically found by ProVerif, with references to the corresponding subsections. ✓: ProVerif proved the property. X/✓: ProVerif shows that some residual risks remain in some configurations (attacks against *Agr*<sub>*</sub>) and proves instead a weaker property that does not consider the residual risks (*Agr*<sub>*</sub>). When we claim a proof: not all configurations have necessarily been proven, but all configuration options are covered (see "Scope of the proofs" in Section 5).</caption><thead><tr><th>Properties</th><th>OPC UA v1.05.03</th><th>v1.05.04 RC</th></tr></thead><tbody><tr><td><i>Conf<sub>C</sub></i></td><td><b>X</b> 5.6</td><td>✓</td></tr><tr><td><i>Conf<sub>S</sub></i></td><td>✓</td><td>✓</td></tr><tr><td><i>Conf<sub>Pwd</sub></i></td><td><b>X</b> 5.6</td><td>✓</td></tr><tr><td><i>Agr<sub>S</sub></i></td><td><b>X</b> 5.1, 5.2, 5.3, 5.4, 5.5</td><td><b>X</b>✓<sup>-</sup></td></tr><tr><td><i>Agr<sub>C</sub></i></td><td><b>X</b> 5.1, 5.2, 5.6</td><td><b>X</b>✓<sup>-</sup></td></tr></tbody></table>

describe target a specification, rather than an implementation, we did not request CVEs.

**Scope of the proofs.** Our detailed results can be found in [15] and are summarized next. Proofs for *Conf*<sub>C</sub> and *Conf*<sub>S</sub> (obtained in maximum 10 hours) are with respect to almost maximal configurations. Namely, we achieve the maximal configuration for RSA. Proofs are more challenging in ECC because they require PFS. We can nevertheless prove the maximal configuration (excluding None and SNoAA): (i) without Leak, as well as (ii) with Leak and either without Reopen, or without Switch. We proved *Conf*<sub>Pwd</sub> for the maximal configuration without Leak. With Leak, proofs were harder to obtain as we must choose between Reopen and Switch. We otherwise capture all configurations when considering in isolation SecurityPolicy and Mode.

The weakened agreement properties, $Agr_S^-$ and $Agr_C^-$ (formally defined in Appendix A), are even more complex to prove, due to the conditioning of all residual risks. We were thus not able to prove them for the maximal configurations, and we instead explored some configuration options separately. Regarding $Agr_S^-$, we were able to obtain proofs without Leak for Reopen + Switch. With Leak, additional residual attacks remain in presence of Reopen (5.4, 5.5) or Switch (5.4). We nevertheless obtained proofs without Reopen nor Switch. Regarding $Agr_C^-$, we additionally prove it for RSA + Leak + Reopen + Switch (without Enc).

We report all of our results in [15]. Finally, except for the signature oracle attack (5.6), all vulnerabilities we report were automatically discovered using ProVerif on our model.

## 5.1 Race Condition for User Contexts

We discovered a *race condition* after the handover of a session to a new user, that breaks the authentication of user requests.
<table><caption>Table 3: Summary of the attacks found that affect OPC UA v1.05.03. Additionally, all attacks except those that require ECC also affect OPC UA v1.04. Att(d) denotes the attacker should know or compromise *d*. We indicate with Agr<sub>CS</sub> when both Agr<sub>C</sub> and Agr<sub>C</sub> are violated (similarly for the weakened variants). For agreement properties, we indicate in square bracket the piece of data on which the disagreement occurs. For instance, Agr<sub>CS</sub>[U] indicates that clients and servers both end up in disagreement on the user U who sent/received a request. Finally, Agr<sup>-0</sup><sub>S</sub> denotes the first weakening of Agr<sub>S</sub> (see Appendix A). We indicate in bold font the remediations chosen by the OPC UA Foundation to be included in the specification and in parentheses the tickets that can be found at https://mantis.opcfoundation.org/view.php?id=<ticket>.</caption><thead><tr><th>Name (Section)</th><th>Violated Properties</th><th>Violation</th><th>Threat</th><th>Configuration</th><th>Practical Impact</th><th>Root Causes</th><th>Remediations: Fix, Mitigation (Mit), Enhancement (Enh) and their Tickets</th></tr></thead><tbody><tr><td>Race Condition for User Contexts (5.1)</td><td>Agr<sub>S</sub>[U]</td><td>Server S receives a user request allegedly from C, U but U<sub>2</sub> sent it</td><td>Ø</td><td>Assumptions</td><td></td><td>Abuse of user rights, wrong logging (user)</td><td>• RC1: missing binding btw user and activated session (SAtoken tok<sub>s</sub>)</td></tr><tr><td>Client Impersonation in ECC (5.2)</td><td>Agr<sub>CS</sub>[C]</td><td>Server S receives a user request allegedly from C<sup>a</sup>, U but it comes from C, U</td><td>Att(C<sub>sk</sub>)</td><td>ECC + SNoAA</td><td>Confusion (client, user) at server, potential confusion test vs prod. client, wrong client logging</td><td>• RC2: lack of receiver identity</td><td>• Fix2: enforce receiver identity in ECC (9349)<br>• Enh2: clarify stronger checks in SNoAA (9350, 9427)</td></tr><tr><td>KCI: User Impersonation (5.3)</td><td>Agr<sup>-0</sup><sub>S</sub>[U]</td><td>Server S receives a user request allegedly from C<sup>a</sup>, U but user U is on client C and did not send it</td><td>Att(C<sub>sk</sub>), Att(S<sub>sk</sub>)</td><td>Cert</td><td></td><td>User impersonation</td><td>• RC3: lack of binding of user's authentication (user's signature) to full context (client identity)</td></tr><tr><td>Downgrade of Password Security (5.6)</td><td>Conf<sub>Pwd</sub></td><td>Compromission of user password</td><td>Att(ch<sub>sk</sub>)</td><td>Enc + Pwd</td><td>Stealing of user password, full user impersonation</td><td>• RC4: relaxed security configuration to avoid what may appear to be redundant encryption but is not</td><td>• Fix3: add client's identity (public key or certificate) in user's authentication signature<br>• Enh3: plan to release some enhanced security versions of the user tokens (9809, 9810)</td></tr><tr><td>Risk of Signature Oracle (5.6)</td><td>Conf<sub>C</sub>, Conf<sub>Pwd</sub>, Agr<sub>C</sub></td><td>Server impersonation towards honest clients and users in ECC, a less severe UKS attack for RSA</td><td>Ø</td><td>ECC + SNoAA</td><td>Stealing of user password, full server impersonation</td><td>• RC5: lack of context in signatures</td><td>• Fix5: add context and tags to the signature<br>• Enh5: checked well-formedness of certificates (9594, 9596, 9597 and 9598) and nonce length (9595, 9599)</td></tr><tr><td>Session Hijack— Reopen (5.4)</td><td>Agr<sup>-</sup><sub>S</sub>[U]</td><td>Server S receives a user request allegedly from C<sup>a</sup>, U but user U is on client C and did not send it</td><td>Att(C<sub>sk</sub>)</td><td>Sign (+ Reopen)</td><td>User impersonation</td><td>• RC6: lack of binding btw channel symmetric keys before and after renewal (Reopen)<br>• RC7: no session ownership proof (tok<sub>s</sub> not secret)</td><td>• Fix6: forbid reopen takeover by linking channel secret keys through renewal (10056)<br>• Fix7: keep tok<sub>s</sub> secret even is Sign mode, and use it as a MAC computed on each request<br>• Mit2: disable Sign mode by default (9875)</td></tr><tr><td>Session Hijack— Switch (5.4)</td><td>Agr<sup>-</sup><sub>S</sub>[U]</td><td>Server S receives a user request allegedly from C<sup>a</sup>, U but user U is on client C and did not send it</td><td>Att(C<sub>sk</sub>)</td><td>Sign (+ Switch)</td><td>User impersonation</td><td>• RC7: no session ownership proof (tok<sub>s</sub> is not secret)</td><td>• Fix7: keep tok<sub>s</sub> secret even is Sign mode, and use it as a MAC computed on each request<br>• Mit2: disable Sign mode by default (9875)</td></tr><tr><td>KCI: Session and User Con- fusion (5.5)</td><td>Agr<sup>-</sup><sub>S</sub>[U]</td><td>Server S receives a user request allegedly from C, U but U<sup>d</sup> sent it and U<sup>d</sup> can be a dummy user without any valid credential</td><td>Att(S<sub>sk</sub>)</td><td>(Reopen)</td><td>User impersonation</td><td>• RC6: lack of binding btw channel symmetric keys before and after renewal (Reopen)<br>• RC7: no session ownership proof (tok<sub>s</sub> not secret)</td><td>• Fix6: forbid reopen takeover by linking channel secret keys through renewal (10056)<br>• Fix7: keep tok<sub>s</sub> secret even is Sign mode, and use it as a MAC computed on each request</td></tr></tbody></table>
<figure><img src="image_7.png" /><figcaption>Figure 5: Client impersonation attack when SecurityPolicy = ECC and SessionSecurity = SNoAA. Lack of agreement on the client during user Authentication is made possible by the same weakness that allows the KCI attack, i.e., the lack of link to the client.</figcaption></figure>

This violation occurs on all versions of OPC UA and does not
require any key compromise.

**Description.** Suppose that an honest client creates a session, that is activated by user $U^1$ who sends a user request $R$. Before the request is received (either intercepted by an attacker, or delayed) the session is transferred to user $U^2$ by a new activation request. After the session transfer, the request $R$ is received by the server and interpreted as a request from $U^2$, hence violating *Agr$_S$*. The detailed message exchange is given in [14, C.1]. A similar attack can be mounted against *Agr$_C$*. The attack relies on the fact that a user handover neither modifies the session identifier nor the session token, none of them being bound to the user identity.

**Impact.** Since a user $U^2$ may have higher security clearance or privileges than $U^1$, this attack may lead to an abuse of access rights and privilege escalation. It also leads to wrong security logs and user requests attributions.

**Mitigations and fix.** The confusion of user context could be avoided by using a fresh *Session Authentication Token* *tok$_S$* for each new user, i.e., in each session activation response ([23, Part 4, § 5.6.3.2 table 17]). This would avoid the above attack, but would not be backward compatible.

The OPC Foundation has acknowledged the problem, and plans to include the following mitigations in v.1.05.04 RC (#9351): (i) clients should "create a new session for the new credentials, do the higher privilege operation and close the sessions"; (ii) "do not process new requests until activate session completes; any existing requests finish with the current credentials". As a result, the privilege escalation exploit discussed above is no longer possible. However, *Agr$_S$* and *Agr$_C$* are still formally violated due to the lack of agreement on the user's identity (and not only his rights). Therefore, in order to further analyze *Agr$_S$* and *Agr$_C$*, we had to weaken the properties to allow the user to differ, if there has been a previous activation with another user. The weakened properties are formally defined in Appendix A.

## 5.2 Client Impersonation in ECC

Our analysis uncovered that the supposedly more secure ECC policy suffers from a client impersonation attack when *SessionSecurity* = *SNoAA* that violates *Agr*<sub>S</sub> and *Agr*<sub>C</sub>. The attacker can deceive a server into believing that the user issuing the request is on a different client.

**Description.** We illustrate the attack against *Agr*<sub>S</sub> in Fig. 5 (detailed flow in [14, C.2]) and suppose an honest client *C*, a compromised client *A* (presented as the attacker) and an honest server *S*.

*C* sends an *OpenSecureChannel* request to *S*. The attacker intercepts this request and modifies the client's identity and resigns the request as coming from *A*. The server sends its response that the attacker forwards to *C*, who accepts and opens the channel. Indeed, when *SecurityPolicy* = *ECC*, the server's response does *not* include the client's identity. According to [23, Part 6, § 6.7.2.3 table 51] the *ReceiverCertificateThumbprint*, that indicates what public key was used to encrypt the remaining of the message, *shall be null if the message is not encrypted*, which is the case in *ECC* (but not in *RSA*, for which the attack is impossible). Therefore, client *C* is unable to detect that the server's response was intended for *A*.

At this stage, this already violates authentication of the *OpenSecureChannel* request, which one could state as an intermediate property, as there is disagreement on the client identity between *C* and *S*. The attack is also reminiscent of Lowe's attack on the NSPK protocol [20].

We now show the attacker can continue and violate *Agr*<sub>S</sub>. Once the channel is established, the client *C* will use it to create a session. A user on client *C* will activate this session and send a user request. These requests will be accepted when *SessionSecurity* = *SNoAA* as the server does *not* check that the client certificate corresponds to the one of the channel.

Hence, the server believes that the request received stems from user *U* on client *A* while it actually originates from user *U* on client *C*. As illustrated by the events at the end of the client and server's execution in Fig. 5, this disagreement
<figure><img src="image_8.png" /><figcaption>Figure 6: KCI user impersonation attack when SessionSecurity = SSec (illustrated here when SecurityPolicy = ECC and Mode = Enc). Values in a session between the attacker and the server (respectively client) are annotated with $^{as}$ (respectively $^{ca}$). We write OpenChannel($id_c^{as}$, $sk^{as}$) for the channel open request and response messages with $id_c^{as}$ identifier and keys $sk^{as}$.</figcaption></figure>

violates $Agr_S$ (note that user $U$ is neither compromised nor using passwords). The same attack and disagreement on the client identity does actually also violate $Agr_C$.

Interestingly, this attack affects the newly introduced ECC but not the "old" and supposedly less secure RSA security policy since the ReceiverCertificateThumbprint is not null. It witnesses the fact that cryptographic suites cannot be simply replaced without a thorough security analysis.

**Impact.** Such an attack could for instance be exploited to create wrong security logs or circumvent user authorization based on the client machine (e.g., Role Based Access Control). Indeed, the server will associate the wrong client-user pair to a user request. A more dramatic example of a potential exploit scenario of the lack of agreement allows an attacker to redirect legitimate (say highly privileged) user $U$'s requests at a training client $C$ intended to a training server, to an in-production SCADA server $S$, who will accept and log them as coming from a control room client $A$, that we assume compromised (say decommissioned). This kind of confusion is made possible by the lack of agreement on the pair user-client and a "Non-Transparent Redundancy" server mode. We further explain this and report an additional, less serious Denial-of-service attack (DOS) attack in our full vulnerability report [15].

**Mitigation and fix.** We proposed to fix this vulnerability by including ReceiverCertificateThumbprint (i.e., hash of the receiver's public key) in ECC as well. This fix was accepted by the OPC Foundation and changes in the specification are documented in tickets #9349, #9350 and #9427 including the fix and several clarifications (notably the Conformance Unit 3781). In particular, they updated [23, Part 6]

v1.05.04 RC to "require the ReceiverCertificateThumbprint to be set for all ECC policies". Since the issue is corrected in the specification, we included the fix in our model to show its effectiveness. In particular, while ProVerif finds an attack against $Agr_C^{-}$ on v1.05.03 for configuration (ECC + Enc + SNoAA + Cert + Leak), it proves v1.05.04 RC secure for the same property and configuration.

## 5.3 KCI: User Impersonation

While key compromise allows to trivially impersonate the compromised party, a Key Compromise Impersonation (KCI) attack allows to impersonate an uncompromised party to the compromised party. Modern protocols are designed to resist such attacks. For instance, the TLS 1.3 specification explicitly lists resistance to KCI attacks as one of its goals [26, App. E] for certificate-based authentication. Yet, we have discovered a KCI attack that allows to impersonate an honest user on an honest client to a server whose keys have been leaked.

We note that password-based authentication is broken in OPC UA as soon as a user connects to a server whose keys have been compromised since clients send user's passwords to the server. Certificate based authentication is supposed to resist this since it involves a signature by the user's private key (e.g., computed on a smart card) of a nonce generated by the server. The attack we found shows the contrary: a user can be impersonated even when using a certificate to authenticate.

**Description.** The attack involves an uncompromised client $C$, an uncompromised user $U$, and a compromised server $S$. We also suppose that the keys of another client $C^A$ have been compromised. We explain the attack when SecurityPolicy =
<figure><img src="image_9.png" /><figcaption>Figure 7: Session hijacking by reopening a channel when Mode = Sign, illustrated here with SecurityPolicy = ECC and SessionSecurity = SSec.</figcaption></figure>

ECC and Mode = Enc. The detailed message flow is provided in Fig. 6.

1. The attacker opens a channel between $C^A$ and $S$ and creates a session $se_1$ between $C^A$ and the honest server $S$, in which $S$ generates the nonce $S_{nonce}$ (see Fig. 4).

2. $C$ sends an Open Channel Request to $S$ that is intercepted by the attacker. Knowing $S$'s long-term keys, the attacker forges and sends back to $C$ a valid response. Hence, the attacker also knows the channel keys.

3. $C$ sends a Create Session Request to $S$. The attacker intercepts it. Knowing $S$'s long-term keys and the channel keys, the attacker can impersonate the server and forges a valid Response. Moreover, the attacker uses the same server nonce $S_{nonce}$ as in sessions $se_1$. $C$ records this session $se_2$ in its local state.

4. User $U$ on client $C$ sends an activation request for $se_2$ to $S$. The attacker intercepts it and extracts the signature $[S_{cert} | S_{nonce}]_{U_{sk}}$ created by $U$ to authenticate, where $U_{sk}$ is the private key associated to $U_{cert}$.

5. The attacker activates session $se_1$ using $U$'s signature $[S_{cert} | S_{nonce}]_{U_{sk}}$. As the server $S$ has created $S_{nonce}$ for session $se_1$, this session creation is accepted by $S$.

6. The attacker can now send arbitrary user requests in $se_1$ from client $C^A$ without any further intervention from $U$. Note that the user $U$ had no interaction with client $C^A$.

This attack violates $Agr_S$ as a server accepts a user $U$'s request without the user having sent any request.

**Impact.** Assuming long-term keys $S_{sk}$ of server $S$ were compromised, an attacker can send arbitrary user requests to the legitimate server $S$ on behalf of a user $U$, even if $U$ authenticates with an uncompromised certificate on an uncompromised client (e.g., using state-of-the-art authentication on a smart card), and even if $U$ did not send any user request. We stress that we solely assume that $S_{sk}$ are compromised (e.g., through a flawed certificate management/renewal or flawed certificate storage/generation) but do not assume that the server is fully compromised. In particular, the server

$S$ could be protected with additional layers of security and can have access to high-privileged data and actions that the attacker does not have access to.

**Mitigation and fix.** We proposed to fix this vulnerability by adding the client's identity to the user's signature, i.e., $[C_{pk} | S_{cert} | S_{nonce}]_{U_{sk}}$, where $C_{pk}$ is the public key of the client's certificate. Such a fix would however break backwards compatibility of systems in production. The OPC Foundation acknowledged the attack, but considered the compromise of server long-term keys to be a very strong threat model that should be accepted for now, given the cost of a non-backward compatible fix. In the mid-term, they want to consider to "release some enhanced security versions of the user tokens", notably using ideas from RFC 8705 (e.g., CertificateBound JWTs); see the associated tickets #9809 and #9810.

To further analyze OPC UA, we had to weaken $Agr_S^-$ to accept this residual risk, and to not deem as attacks the executions where a client is compromised and an honest user activates a session towards a compromised server (see Appendix A).

## 5.4 Session Hijack by Reopening or Switching

Even though the weakened property $Agr_S^-$ purposely avoids the previous attacks, we were able to uncover yet another attack when channels only provide integrity, i.e., Mode = Sign.

**Description.** The attack involves a compromised client $C$, an uncompromised user $U$ and an uncompromised server $S$. The detailed message flow is provided in Fig. 7.

1. Client $C$ (whose key $C_{sk}$ has been compromised) opens a channel in Mode = Sign and creates a session with $S$. The attacker learns the session token $tok_s$ as only integrity is provided. (Note that although the attacker knows $C_{sk}$, it does not know the channel keys $sk$.)

2. Honest user $U$ on client $C$ activates the session using its user credentials (which are not leaked to the attacker).
<figure><img src="image_10.png" /><figcaption>Figure 8: Session confusion illustrated here with Mode = Enc, SecurityPolicy = ECC and SessionSecurity = SSec.</figcaption></figure>

3. Using $C_{sk}$ the attacker re-opens the channel with $S$ and learns the updated channel keys $sk'$.

4. Knowing $sk'$ and $tok_s$, the attacker can send arbitrary user requests impersonating $U$.

**Session Hijack by Switching variant.** Note that a variant of this attack relies on switching the channel of a session, rather than reopening the channel. In the above attack, a channel reopening request was issued by the attacker to gain access to the channel underlying the session. Alternatively, an attacker can intercept a session re-activation, open a new channel, and replay the re-activation attack on the new (attacker controlled) channel (see [14, C.3] for details).

**Impact.** Assuming that a client's long-term is compromised, an attacker can completely hijack the session of a user who activated a session on that client. The attacker can therefore send arbitrary requests on behalf of $U$.

**Mitigation.** This attack has also been acknowledged by the OPC Foundation. As a counter-measure the foundation considers deactivating the mode Mode = Sign by default (tickets #9874, #9875). For a future version, the foundation also considers chaining channel keys through reopening (ticket #10056), which requires knowledge of previous channel keys to initiate a Reopen.

## 5.5 KCI: Session and User Confusion

As a response to our Session Hijack attacks, the OPC Foundation decided to disable Mode = Sign by default. However, even

when Mode = Enc, we found another KCI attack that violates the weakened property $\text{Agr}_S^-$, which excluded the previous KCI attack (Section 5.3). We shall also assume a compromise of a server's long-term key. Recall that an impersonation of this server is obviously possible. What we additionally show is an impersonation of honest users towards that honest server.

**Description.** The attack involves an honest client $C$ and user $U$, a compromised server $S$. We additionally assume the adversary has normal access to $C$ but is not necessarily registered in the user database. The detailed message flow is provided in Fig. 8.

1. User $U$ on client $C$ opens a channel, creates and activate a session $s_1$ with server $S$.

2. When $C$ renews the channel keys (Reopen), the attacker impersonates $S$ and learns the new channel keys $sk_2$. He will then learn $tok_s^1$ for session $s_1$.

3. The adversary initiates a new session $s_2$ creation and activation on $C$ with a dummy user $U^d$ ($U^d$ does not have to be a valid, registered user). The adversary continues impersonating $S$: it proceeds and accepts those requests and uses the exact same $tok_s^1$ from $s_1$. $C$ has now registered two sessions $s_1$ (with $U$) and $s_2$ (with $U^d$), both with the same $tok_s^1$. Note that $S$ is neither aware of session $s_2$ nor of user $U^d$.

4. $C$ will eventually reopen the channel with the honest server $S$: the attacker can pretend to lose the connection, or can wait for the channel to be reopened or switched.

5. From now on, when $C$ sends requests from $U^d$ to $S$ in session $s_2$, it uses $tok_s^1$, which causes $S$ to believe this
request is coming from the honest user *U* in session *s*₁.

**Impact.** The impact is similar to the previous KCI attack (Section 5.3). Assuming long-term keys of server *S* were compromised, an attacker having unprivileged access to an honest client *C* can send arbitrary user requests to the legitimate server *S* on behalf of an honest, possibly high-privileged, user *U*, who previously activated a session on that client. Without assuming having access to *C*, a variant of this attack where *U*<sup>*d*</sup> is a valid, honest user is still possible and has a similar impact as the Race Condition attack (Section 5.1): confusion of user context for user requests. Note that the attack is also possible when *Mode* = *Sign*.

**Mitigation.** This attack has also been acknowledged by the OPC Foundation. As a counter-measure the foundation considers chaining channel keys through reopening (ticket #10056).

## 5.6 Other Findings

We report on additional attacks and weaknesses in [14, C.4] that we briefly summarize here.

**Downgrade of Password Secrecy.** Our analysis uncovered that, when channel keys are leaked, counter-intuitively, *Mode* = *Enc* is less secure than *Mode* = *Sign* since it leaks user passwords. This is due to a relaxed security requirement in the specification that allows to send passwords in plaintext when *Mode* = *Enc* since they are under channel encryption anyway. Channel keys can be considered less secure than long-term keys in some scenarios (e.g., when stored in memory while long-terms keys are stored in Hardware Security Module (HSM)s).

The OPC Foundation acknowledged this issue and decided to add a warning and a recommendation to always encrypt passwords (see ticket #9432).

**Risk of Signature Oracle.** A server configured to allow *SNoAA* may not verify the certificate sent by a client application at session creation, but simply append the client nonce and sign the resulting bitstring, to prove possession of its private key. This induces a "signature oracle" to produce valid server signatures on adversarially-chosen data. In particular, this signature oracle can be exploited to forge valid *Open-Channel* response and *CreateSession* responses, allowing to fully impersonate an honest server towards an honest client in *ECC*. Hence, all security goals are violated and the attacker can learn users' passwords. For *RSA*, the attack is less severe as the attacker does not learn the channel keys and can only perform an Unknown Key Share (UKS) attack.

The OPC Foundation acknowledged the weakness, and to mitigate the vulnerability, (i) adds explicit requirements for v.1.05.04 RC, and conformance tests to ensure that certificates are validated before being used to produce a signature (tickets #9594, #9596, #9597 and #9598); (ii) states that all Nonces shall have a length specified by the *SecurityPolicy* (tickets

#9595, #9599). We reflect those fixes in our model and prove that they thwart the attack we found on the same configuration.

## 5.7 Lessons Learned

First, our results confirm that, without key compromise, OPC UA satisfies all security goals except $Agr_S, Agr_C$ due to the Race Condition attack (5.1) ($Agr_S^-, Agr_C^-$ hold nevertheless). This mostly aligns with prior analyses by the BSI [13,31]. Our work extends beyond this baseline by considering strong attacker models including key leakage that are also in scope of the specification's threat model (Section 2.3).

Within that scope, our analysis revealed several attacks and design weaknesses. Our analysis highlights that many attacks exploit (i) the multi-layer nature of the protocol: channels, created and activated sessions, requests, (ii) the agility of the protocol due to OT constraints: switch/reopen channels, re-activate sessions, etc., (iii) the complexity of the protocol: combination of multiple options and configurations. We believe that this protocol complexity is not inherently insecure, but requires a careful analysis. Several protocol design flaws are the root causes of our attacks and are often related to missing bindings between critical components, such as (see Table 3 for a detailed list): activated sessions are not bound to their user (5.1), signed requests are not bound to the recipient (5.2), signed user tokens are not bound to the client (5.3), new channel keys obtained by reopening are not bound to previous keys (5.4, [14, C.3], 5.5), and the absence of a context binding in signatures ([14, C.4.2]). This should be remembered when designing future protocol evolutions.

Our analysis also highlights the pitfalls of adding new features on top of an existing protocol. For instance, the addition of *ECC* by simply replacing a cryptographic primitive suite by another one has led to a quite subtle attack (5.2).

Finally, our interaction with the OPC Foundation demonstrates the importance of proactive reporting and collaboration between researchers and standardization bodies to enhance the resilience of critical infrastructures. We were able to adapt our models and analyses to the proposed fixes that were validated by the OPC Foundation.

## 6 Related Work

Formal symbolic verification, using tools such as ProVerif and Tamarin, has been used on many deployed and standardized protocols, including TLS [4, 5, 11], EMV [3], 5G [2, 10], Bluetooth [32], LAKE-EDHOC [19] or WiFi [27]. We continue this line of work, and exploit several of the latest features of ProVerif [7] to enable what we believe to be among the most complex formal analyses. While several of these works also generate different protocol configurations, there are key differences. For instance, Wu et al. [32] use a modular encoding that allows to easily select a given subprotocol of each kind out of many: this results in a large number of rather small
models (200 LoC for the largest unfolded process and 100 initial clauses vs 8.6 kLoC and 2.3 k clauses in our model); moreover, as these models do not consider key compromise (as those of Shen et al. [27]), their verification was fully automatic, and did not face the challenges we needed to address (such as providing lemmas, or fine-tuning of the selection function; see Section 4.3).

Puys et al. [25] previously used ProVerif to analyze OPC UA v1.03, that does not include ECC. Moreover, their models are minimalistic and only consider channel opening and user sessions without analyzing their interaction, omitting many details and configurations studied here. This is reflected by <100 LoC and <100 initial clauses for each of the (separate) models of channel and session protocols.

A quite exhaustive security analysis of OPC UA v1.04 was performed by the German BSI [31]. It includes a risk analysis, a dynamic security analysis through fuzzing and static code analysis of the open62541 implementation. Deployed OPC UA products have also been studied through large-scale Internet measurements [12] and an analysis of products and libraries for OPC UA [17]: these works demonstrate a large number of misconfigured OPC UA artifacts (e.g., certificate checks disabled for testing purpose) enabling attacks that OPC UA was designed to resist (e.g., rogue server); often these misconfigurations were due to unclear instructions or implementations that rely on incomplete libraries. In contrast, our attacks affect even a perfectly well-configured OPC UA protocol deployment. Being performed on version 1.04, these analyses do not include the ECC policy. Moreover, these analyses do not include any security proofs, and we consider them as complementary to our formal verification effort.

Finally, note that six, out of the height vulnerabilities we found, already affected versions 1.03 and 1.04, and yet had not been discovered by these previous efforts.

# 7 Conclusion

We proposed a verification framework for OPC UA based on a comprehensive protocol description, a ProVerif model using a number of advanced ProVerif features and a new proof methodology, and some tooling to mitigate the complexity of the proof effort. Our framework automatically discovered several vulnerabilities that have all been acknowledged by the OPC Foundation. In response, the specification has been updated with fixes and mitigations that we had analyzed.

We believe that our framework can serve as a starting point for other researchers and practitioners working with OPC UA (notably Section 5.7). Our proof methodology may also serve for other ambitious case studies whose automated verification do not work "out-of-the-box". As discussed, the protocol residual risks induced additional analysis challenges, especially for proving the agreement properties. Should those risks be accepted by the Foundation in the longer term, we plan to further improve our proof methodology and develop

dedicated invariants to obtain complete proofs for maximal configurations.

# 8 Ethics Considerations and Compliance with the Open Science Policy

## 8.1 Ethics Considerations

Our paper describes vulnerabilities and weaknesses in a deployed security protocol, OPC UA. Some findings only apply to the latest version of this protocol, that is not yet deployed (version 1.05). As discussed in the paper, all findings have been *responsively disclosed* to the OPC Foundation. To do so, we used the Foundation's reporting tool: https://mantis.opcfoundation.org. For each vulnerability, a private ticket has been issued, and the vulnerabilities have been discussed during the embargo period. We also attended several meetings of the working group for further discussion. The resulting changes to the specification have been documented in public tickets that are cited in the paper.

The vulnerability report that we transmitted to the OPC Foundation for *responsible disclosure* is in the file *vulnerabilities.pdf* [15]. It provides details on the attacks that we present in Section 5. Moreover, Table 3 gives further details on root causes and potential fixes.

No other ethics considerations have been identified.

## 8.2 Open Science

As mentioned in the paper, our models are available in a companion artifact [15], that includes the vulnerability report, all ProVerif models, the dependency graph between properties, and the necessary scripts to reproduce the results from Section 5.

The `README.md` file provides detailed instructions on how to (i) install ProVerif, (ii) configure the Python environment for the scripts, (iii) compute attack traces as PDF files, (iv) prove the security properties in maximal configurations, (v) launch lattice exploration campaigns.

The Python script `opcua.py` (configured by `config.py`) takes `Jinja2` template files `opcua-jinja.pv` and `config-jinja.pvl` to (i) produce the `tmp_opcua.pv` and `tmp_config.pvl` ProVerif input files according to the selected query and configuration, and (ii) launch ProVerif on these files.

The former template file `opcua-jinja.pv` contains the complete ProVerif model of the protocol, all queries corresponding to the security properties and the invariants. Advanced features described in Section 4.3 such as *Name contexts*, *noselect statements* and *invariants* may vary depending on the selected query. The latter template file `config-jinja.pvl` is used for configuring the model, as explained in Section 3.2, Section 4.1 and Table 1. It may also
modify the behavior of ProVerif to prevent attack reconstruction or make the output more verbose.

As an example of attack reconstruction, the attack 5.4 session hijack by reopening, that breaks Agr, is found with the command: `python3 opcua.py -q "3.1.reopen" -c "ECC, Sign, reopen, SSec, cert, no_switch, lt_leaks" -html and the detailed trace can be observed in the file output/trace1.pdf.

As an example of a security property proof, the confidentiality of user requests Conf is proved for SecurityPolicy = ECC without Leak by: `python3 opcua.py -q "Conf[C]" -c "ECC, None|Sign|Encrypt, reopen, SNoAA|SSec, anon|pwd|cert, switch, no_leaks"`.

**The novel proof methodology** presented in Section 4.3.2 requires, for the proof of a formal property to be sound, all its dependencies to be also proven. The dependency graph of our formal model is provided in the file `dependencies.txt`.

As an example of an advanced proof, the weakened authentication of user responses (property Agr, stated as query "3.2", relies on invariants "3.2.axioms", "3.2.A", "3.1.A" and "3.1.C". Each of these needs to be proven separately for the same configuration: `python3 opcua.py -q "3.2" -c "ECC, Encrypt, no_reopen, SSec, cert, no_switch, lt_leaks"` and then `python3 opcua.py -q "3.2.axioms" -c "ECC, Encrypt, no_reopen, SSec, cert, no_switch, lt_leaks"` etc. The script `prove.sh` (see below) allows to prove such a conjunction of properties.

**The systematic exploration of configurations** mentioned in Section 4.2, requires the script `prove.py` (that imports `configurations.py`). It provides the following lists: (i) the maximal true configurations, for which the property holds, (ii) the minimal false configurations, (iii) the minimal configurations for which ProVerif did not finished.

The bash script `prove.sh` starts a new campaign that iteratively increases the time budget for computations. A complete exploration of Conf is launched (preferably on a server for which long runs can be launched) by: `./prove.sh "Conf[C]" "RSA, None|Sign|Encrypt, reopen, SNoAA|SSec, anon|pwd|cert, switch, lt_leaks"`. A restart from a previous campaign ([14, D.1]), for example from the log file `query_Conf[C]_2560.txt` (2560 is the timeout in seconds used at the last step) is launched with a doubled timeout by: `./prove.sh "Conf[C]" "RSA, None|Sign|Encrypt, reopen, SNoAA|SSec, anon|pwd|cert, switch, lt_leaks" 5120 "query_Conf[C]_2560.txt"`. Timeouts for future steps will then be automatically doubled, and handled by the `prove.sh` script. Note that for agreement properties, it is possible to explore proving the conjunction of Agr and all its axioms (as queries) with the query argument "3.1.all" (and "3.2.all" for Agr).

The file `results.md` presents the maximal true configurations for each security property.

## Acknowledgments

This work benefited from funding managed by the French National Research Agency under the France 2030 program (ANR-22-PECY-0006) and the ANR chair in AI ASAP (ANR-20-CHIA-0024) with support from the region Grand Est. We thank Alexandre Debant and Vincent Cheval, for in-depth discussions about ProVerif proofs. We also thank Randy Armstrong and the OPC UA Foundation for the discussions about potential fixes.

## References

[1] M. Baezner and P. Robin. Stuxnet. http://hdl.handle.net/20.500.11850/200661, 2017.

[2] D. A. Basin, J. Dreier, L. Hirschi, S. Radomirovic, R. Sasse, and V. Stettler. A formal analysis of 5G authentication. In *Conference on Computer and Communications Security (CCS)*. ACM, 2018.

[3] D. A. Basin, R. Sasse, and J. Toro-Pozo. The EMV standard: Break, fix, verify. In *Symposium on Security and Privacy (S&P)*. IEEE, 2021.

[4] K. Bhargavan, B. Blanchet, and N. Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. In *Symposium on Security and Privacy (S&P)*. IEEE, 2017.

[5] K. Bhargavan, V. Cheval, and C. A. Wood. A symbolic analysis of privacy for TLS 1.3 with encrypted client hello. In *Conference on Computer and Communications Security (CCS)*. ACM, 2022.

[6] B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In *Computer Security Foundations Workshop (CSFW)*. IEEE, 2001.

[7] B. Blanchet, V. Cheval, and V. Cortier. ProVerif with lemmas, induction, fast subsumption, and much more. In *Symposium on Security and Privacy (S&P)*. IEEE, 2022.

[8] S. Brizinov and N. Moshe. Exploiting OPC-UA in Every Possible Way: Practical Attacks Against Modern OPC-UA Architectures. https://www.blackhat.com/us-23/briefings/schedule/exploiting-opc-ua-in-every-possible-way-practical-attacks-against-modern-opc-ua-architectures-31535, 2023.

[9] P. Cheremushkin and S. Temnikov. OPC UA security analysis. https://ics-cert.kaspersky.com/publications/reports/2018/05/10/opc-ua-security-analysis/, 2018.
[10] C. Cremers and M. Dehnel-Wild. Component-based formal analysis of 5g-aka: Channel assumptions and session confusion. In *Network and Distributed System Security Symposium (NDSS)*, 2019.

[11] C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe. A comprehensive symbolic analysis of TLS 1.3. In *Conference on Computer and Communications Security (CCS)*. ACM, 2017.

[12] M. Dahlmanns, J. Lohmöller, I. B. Fink, J. Pennekamp, K. Wehrle, and M. Henze. Easing the conscience with OPC UA: an internet-wide study on insecure deployments. In *Internet Measurement Conference (IMC)*. ACM, 2020.

[13] Damm, Gappmeier, Zugfil, Plöb, Fiat, and Störtkuhl. OPC-UA security analysis. Technical report, Bundesamt für Sicherheit in der Informationstechnik (BSI), 2017.

[14] V. Diemunsch, L. Hirschi, and S. Kremer. Full version of this paper on IACR eprint. https://eprint.iacr.org/2025/148, 2025.

[15] V. Diemunsch, L. Hirschi, and S. Kremer. Submission artifacts. https://archive.softwareheritage.org/swh:1:rev:1528b4a1dbd05e4e509dabdfd8d7f4a0cd3a6dac;origin= https://github.com/vdh-anssi/opc-ua_security, 2025.

[16] D. Dolev and A. Yao. On the security of public key protocols. *IEEE transactions on information theory*, IT-29(2), 1983.

[17] A. Erba, A. Müller, and N. O. Tippenhauer. Security analysis of vendor implementations of the OPC UA protocol for industrial control systems. In *Workshop on CPS & IoT Security and Privacy (CPSIOTSEC@CCS)*. ACM, 2022.

[18] G. Girol, L. Hirschi, R. Sasse, D. Jackson, C. Cremers, and D. Basin. A spectral analysis of noise: A comprehensive, automated, formal analysis of Diffie-Hellman protocols. In *USENIX Security Symposium*, 2020.

[19] C. Jacomme, E. Klein, S. Kremer, and M. Racouchot. A comprehensive, formal and automated analysis of the EDHOC protocol. In *USENIX Security Symposium*, 2023.

[20] G. Lowe. Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR. In *Tools and Algorithms for the Construction and Analysis of Systems*. Springer, 1996.

[21] G. Lowe. A hierarchy of authentication specifications. In *Computer Security Foundations Workshop (CSFW)*. IEEE Comput. Soc. Press, 1997.

[22] S. Obermeier, R. Schlegel, and J. Schneider. A security evaluation of IEC 62351. In *Journal of Information Security and Applications*, 2016.

[23] OPC Foundation. OPC Unified Architecture Specification. https://reference.opcfoundation.org/, 2023. Release 1.05.03.

[24] OPC Foundation. OPC Unified Architecture Specification. https://profiles.opcfoundation.org/profile/, 2024. Release 1.05.

[25] M. Puys, M.-L. Potet, and P. Lafourcade. Formal Analysis of Security Properties on the OPC-UA SCADA Protocol. In *Computer Safety, Reliability, and Security (SAFECOMP)*, volume 9922 of LNCS. Springer, 2016.

[26] E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446, Aug. 2018.

[27] Z. Shen, I. Karim, and E. Bertino. Segment-based formal verification of wifi fragmentation and power save mode. In *Asia Conference on Computer and Communications Security*, (ASIA CCS). ACM, 2024.

[28] K. Stouffer, M. Pease, C. Tang, T. Zimmmerman, V. Pilitteri, S. Lightman, A. Hahn, S. Saravia, A. Sherule, and M. Thompson. Guide to Operational Technology (OT) Security. https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-82r3.pdf, 2023.

[29] Systerel. A safe and secure OPC UA implementation. https://www.s2opc.com/, 2023. Version 1.3.1.

[30] Team82 Research. OPC UA Deep Dive: A Complete Guide to the OPC UA Attack Surface. https://claroty.com/team82/research/opc-ua-deep-dive-a-complete-guide-to-the-opc-ua-attack-surface, 2023.

[31] J. vom Dorp, S. Merschjohann, D. Meier, F. Patzer, M. Karch, and C. Haas. OPC-UA security analysis. Technical report, Bundesamt für Sicherheit in der Informationstechnik (BSI), 2022.

[32] J. Wu, R. Wu, D. Xu, D. J. Tian, and A. Bianchi. Formal model-driven discovery of bluetooth protocol design vulnerabilities. In *Symposium on Security and Privacy (S&P)*. IEEE, 2022.

## A Weakened Properties

**Weakening to avoid race condition.** As a result of the changes in the specification detailed in Section 5.1, the privilege escalation due to the race condition is mitigated, but the agreement properties *Agr<sub>S</sub>* and *Agr<sub>C</sub>* are still violated. We therefore weaken *Agr<sub>S</sub>* as follows:
```
inj-event(S_Rcv_User_Req(C_pk, S_pk, SE, U, R))
==> ( inj-event(C_Snd_User_Req(C_pk, S_pk, SE, U', R))
    && event(S_Activation(C_pk, S_pk, SE', U')) )
|| ( event(leak(C_pk)) || mode = None ) &&
    ( U = anon || event(leak(U)) ||
        event(C_Activ_req(C_pk,S_pk,mode,check,SE',U,pwd))
    && event(leak(S_pk)) )
```

where SE' is the same as SE, except for the secure channel. Hence, we explicitly tolerate a mismatch on the user if this user has sent an activation request to the server (as in the race condition). Allowing the channel to differ in the sessions is needed as channels may be reopened. $Agr_C$ can be weakened in an analogous way (see [15]).

**Weakening to avoid the user impersonation KCI attack.**
As the first KCI attack (Section 5.3) has currently not been fixed, we weaken $Agr_S$ to exclude this attack and further analyze the protocol. Namely, we add a disjunct that excludes the combination of server's and client's long-term keys compromise. We additionally need to take into account other possible exploits of the KCI attacks that open up new ways to compromise user's authentication tokens. As a result, the condition

```
|| ( event(leak(C_pk)) || mode = None ) &&
    ( U = anon || event(leak(U)) ||
        event(C_Activ_req(C_pk,S_pk,mode,check,SE',U,pwd))
    && event(leak(S_pk)) )
```

is replaced by

```
|| ( event(leak(C_pk)) || mode = None ) &&
    ( U = anon || event(leak(U)) ||
        event(leaked_server(rogue_server)) ||
        event(C_Activ_req(C_pk,S_pk,mode3,check,SE',U,u_pk))
    && ( mode3 = None || mode3 = Sign )
)
```

Indeed, if the client is compromised and there is a rogue server (i.e., a compromised server), the attacker could use it to inject a $S_nonce$, honestly generated by an honest server, to obtain and steal an authentication token from an uncompromised user. Note that this now replaces the previous condition for the case $u_pk=pwd$. Similarly, if a user authenticates using a client in a channel in mode Sign or None, an attacker may act as a MiM and eavesdrops on the signed user's authentication token.

We define $Agr_S^-$ to be the property obtained by weakening $Agr_S$ to both avoid the race condition and the first KCI attack. Similarly, $Agr_C^-$ corresponds to the weakening of $Agr_C$ to avoid the race condition. (The KCI attacks do not violate $Agr_C$).

We do not claim $Agr_S^-$ is "optimal", in the sense that it would perfectly capture the residual risks; it could be an over-approximation since the residual risks are hard to define. However, $Agr_S^-$ nonetheless remains a sound approximation of a model that would consider that "all is lost" as soon as there is a rogue server. Supporting this is the fact that we later found another KCI attack (i.e., KCI: Session and User Confusion, see Section 5.5) that violates $Agr_S^-$ despite being a KCI attack too. The crux of this new attack is that it does not assume any client compromise, but only a server compromise.

## B Proof Methodology: An Example

We initially faced the following problem: the proof for $Agr_S^-$ in configuration (RSA + Sign + Reopen + SSec + Cert + Switch) does not terminate in reasonable time and shows an explosion of the number of generated clauses (clauses in the Queue).

The ProVerif output log with the option `verboseRules` shows that one quarter of the generated clauses have the fact `table(S_sessions(y))` as conclusion fact. We identify this fact as a candidate for breaking the loop.

We add

```
noselect x1,x2:pkey, x3:seid, x4:stoken, x5:smode, x6:channel_
    x7:login, x8:utoken, x9:exponent, x10:nonce;
table(S_sessions( *x1,*x2,*x3,*x4,*x5,*x6,*x7,*x8,*x9,*x10))
    /9000.
```

We re-run the proof and still observe that the proof search seems to loop. Inspection of the output log reveals that many clauses are generated with the fact `table(C_sessions(y))` so we add a noselect statement for `C_sessions` as well. We re-run ProVerif: the proof now concludes in 4 seconds with a cannot-be-proved.

Inspecting the derivation produced by ProVerif for the cannot-be-proved, we observe two hypotheses over the facts under the noselect statements:

```
event insert_S_sessions(pk(sk_2),pk(sk_3),id_132,SAtk,SSec,
    chan(certifyTIMES client,RSA,pk(sk_2)),certifyTIMES server,RSA,pk(sk_3)
    ),Sign,ch_n_1,
    keys(Token_1, enc_key_RSA(C_Nonce_1,S_Nonce_1),
        sign_key_RSA(C_Nonce_1,S_Nonce_1), enc_key_RSA(
            S_Nonce_1,C_Nonce_1), sign_key_RSA(S_Nonce_1,C_Nonce_1
        ))
    ),usr_7,U_tk_8,S_er_2,S_nonce_22))
```

and similarly for `insert_C_sessions`, where client signing key `sign_key_RSA(C_Nonce_1,S_Nonce_1)` and SAtk match between `S_session` and `C_session`. However, the rest of the channel keys (e.g., `S_enc_k_68`, `S_sign_k_68`) are not assumed to match.

We know this is impossible since all channel keys are derived from the same seed in the protocol. Therefore, if `sign_key_RSA(C_Nonce_1,S_Nonce_1)` matches between a client's session entry and a server's session entry, then all channel keys must match between those entries. Moreover, both entries should agree on client and server identities. We shall see how to add such an invariant in the next step.

We had observed that client server session table entries agreed on the session token and the client signing key. We therefore add an axiom that states that if client signing keys and SAtk are equal then all channel keys are equal as well and the client and server's identities match or both of the client's and server's long-term keys leaked.

Rerunning ProVerif on the main property we obtain again cannot-be-proved. However, inspecting the derivation we observe that the session entries between client and server now coincide on channel keys and identities. However, they still differ on sessions ids and users. We identify additional false assumptions and add invariants to remove them, we list them all in [15].

The above invariants can actually easily be proved by ProVerif in about 1 second as a query. See [14, D.2] for more details.