Formal models for threat analysis in next-generation networks

Modern computing and networking infrastructures are becoming increasingly complex, heterogeneous, and dynamic, integrating paradigms such as cloud computing, cyber-physical systems, and next-generation mobile networks. At the same time, cyber attacks are evolving in sophistication, often unfolding across multiple stages and spanning cyber, physical, and human domains. Threat modeling and analysis are fundamental proactive cybersecurity activities aimed at identifying such attacks. However, current approaches often struggle to model complex attack scenarios and frequently overlook the human and physical dimensions of attacks. This PhD research aims to design a novel threat modeling and analysis methodology combining high modeling expressivity, formal rigor and automation. The approach relies on a threat modeling taxonomy to formally represent system components, vulnerabilities, threats, and relationships, enabling the construction of a structured knowledge base. An automated analysis engine applies formal derivation rules to infer security properties and reconstruct multi-step attack scenarios. An interactive analysis phase further supports explainability and decision-making. The expected outcome is a formally grounded methodology for analyzing complex threats across heterogeneous, multi-domain infrastructures.