A Comprehensive Formal Security Analysis of OPC UA
summary
Formal model of OPC UA v1.04 and v1.05 uses ProVerif symbolic model to analyze RSA and new DH/ECC key exchange, covering secure-channel, session creation, reopening and switching, with a configurable lattice of 7,560 variants. The effort finds five attacks and three weaknesses (including a session-hijack via channel reopening when client keys are compromised), proves many configurations secure and verifies Perfect Forward Secrecy (PFS) for ECC channels, and proposes fixes that the OPC Foundation acknowledges and partially adopts.
AI-written summary · about
chapters (7)
- 0:00OPC UA introduction
- 4:04Security analysis goals
- 5:30Formal modeling with ProVerif
- 7:15ProVerif challenges
- 12:29Discovered vulnerabilities
- 13:34Session hijack example
- 16:23Findings and future work
related talks
40mExploiting OPC-UA in Every Possible Way: Practical Attacks Against Modern OPC-UA Architectures
36mWhen The Front Door Becomes a Backdoor: The Security Paradox of OSDP
19mDesign Space and Challenges in Design of Attested TLS Protocols
30mInsecurity protocols: an overview of modern authentication
19mIoT Security Exposed: From PLC Flaws to the Imperative of SBOM
15m"Don't roll your own crypto": Formal Methods for Security
45mWhen Machines Can't Talk
38mHow to read a PL-security paper