A Formal Verification Approach to Handle Attack Graph

We propose a formalization of attack graphs through a multi-agent approach. Specifically, we focus on dynamic scenarios that capture the interaction between an attacker and defenders during a cyberattack. We introduce a formal definition of an attack graph using interpreted systems, demonstrating how this formalization enables us to express interesting security properties. Finally, we present a tool AG2IS, which we have developed as an implementation of our formal definitions, to perform the formal verification of attack graphs.