Formal verification has become a key tool to rigorously assess the security of industrial cyber‑physical systems. At the same time, new decentralized PKI approaches are emerging to overcome single points of failure and transparency limitations of traditional CA hierarchies. In modular automation scenarios (e.g., module type package), concepts try to decouple the certificate management from a single operator PKI. This modularization promises flexibility and scalability, but it also introduces new attack surfaces and complex trust relationships that are not yet formally understood.  

This thesis offers a highly topical research opportunity at the intersection of industrial security, PKI design, and formal methods. You will gain hands‑on experience with state‑of‑the‑art verification tools, contribute to more secure modular automation architectures, and explore how future decentralized PKI concepts can be applied and validated in real industrial settings.

In particular, the outcome of the thesis might influence standardization of the security aspects of the module type package.

GOALS:

• Translate emerging concepts to formal models
• Specify and verify key properties using a tool like ProVerif or Tamarin
• Compare centralized vs. decentralized designs

HELPFUL PRIOR KNOWLEDGE:

• Basic Understanding of Industrial Automation
• Interest to get familiar with emerging security concepts