Attack graphs is an attack modelling formalism that allows to represent the different attack paths in a system based on known vulnerabilities. Once attack graphs are generated they can be used as a basis to perform different types of analysis: reachability analysis, generation of a patch policy…
In general these analysis consider a “static” scenario: given an attack graph, the defender designs some a priori security hardening policy. However few works address a more dynamic scenario corresponding to reactions during an on-going attack, and capturing interactions between an (or several) attacker(s) and a defender. Recently, classic formal verification approaches such as model checking have been extended to handle multi-agent systems. The goal of this project is to define a game model based on attack graphs and a verification procedure for this game.