A formal approach to attack graphs

An attack graph is a concise portrayal of the various paths within an open system that enable an attacker to reach a prohibited state (such as gaining access to a restricted resource), despite the system’s preventive measures. The assessment of system vulnerability involves examining the presence of such paths. In this work, we analyze attack graphs using a game-theoretic approach. Specifically, we introduce a well-suited game model that represents the dynamics between the system and the attacker, and propose an automata-based solution to demonstrate the absence of vulnerability.