Formal Modeling and Verification of Generic Credential Management Processes for Industrial Cyber–Physical Systems

Industrial cyber-physical systems (ICPS) face rising cyberattacks, requiring secure credential management also in resource-constrained embedded systems. Standards specifying field level communication of ICPS (e.g., PROFINET or OPC UA) define protocol-specific credential management processes, yet lack formal security verification. We propose a generic model capturing initial security onboarding and automated credential provisioning. Using ProVerif, an automatic symbolic protocol verifier, we formalize certificate-based authentication under a Dolev-Yao adversary, verifying private key secrecy, component authentication, and mutual authentication with the operator domain. Robustness checks confirm resilience against key leakage and highlight the vulnerabilities of the trust on first use concept proposed by the standards. Our model offers the first formal guarantees for secure credential management in ICPS.