A Comprehensive Formal Security Analysis of OPC UA
Vincent Diemunsch
34th USENIX Security Symposium (USENIX Security '25) · Day 3 · Network Security 4: Internet and Beyond
This talk presents a rigorous formal security analysis of **OPC Unified Architecture (OPC UA)**, a critical industrial control system (ICS) protocol. Delivered by Vincent Diemunsch from the French Cyber Security Agency, in collaboration with Lukayashi and Steve Kramer from INRIA, the research delves into the protocol's built-in security mechanisms. OPC UA is widely deployed in safety-critical infrastructures such as nuclear power plants, power grids, air traffic control, and oil and gas installations, making its security paramount.
AI review
Legitimate formal methods research on a widely-deployed ICS protocol that actually matters — OPC UA runs in nuclear plants and power grids, and these folks found five new attacks and three weaknesses the prior piecemeal analyses missed. The session hijack via channel renewal is a clean, concrete result, not a theoretical curiosity, and getting the OPC Foundation to patch from academic disclosure is a real outcome. The methodology contribution — breaking ProVerif resolution loops with 100+ lemmas across 756 configurations — is genuinely novel and transferable to other complex protocol…