OPC UA是一种旨在确保安全的关键基础架构中的标准化工业控制系统(ICS)协议。即将发布的1.05版包括基础加密设计的重大更改,包括基于Diffie-Hellmann的密钥交换,而不是以前的基于RSA的版本。版本1.05应该提供更强大的安全性,包括完美的前锋保密(PFS)。我们使用最先进的符号协议验证程序proverif对OPC UA V1.05和V1.04中指定的安全协议进行正式安全分析。与以前的研究相比,我们的模型更加全面,包括新协议版本,包括建立安全渠道,会话及其管理的不同子协议的组合,涵盖了大量可能的配置。这导致了有史以来最大的模型之一,这是由于状态机器的复杂性而引起的许多挑战,主要是由于状态机的复杂性。我们讨论了如何缓解这种复杂性以获得有意义的分析结果。我们的分析发现了OPC基金会已报告并承认的几个新漏洞。我们设计并提出了证明是安全的修复程序,其中大多数包含在该标准的即将版本中。
主要关键词