Résumé
An attack graph is a succinct representation of all the paths in an open system that allow an attacker to enter a forbidden state (e.g., a resource), besides any attempt of the system to prevent it. Checking system vulnerabil- ity amounts to verifying whether such paths exist. In this paper we reason about attack graphs by means of a game-theoretic approach. Precisely, we introduce a suitable game model to represent the interaction between the system and the attacker and an automata-based solution to show the absence of vulnerability.