Make attack-defense trees formal objects

We consider a highly classic model used by security expert to reason about ways to attack a system and to defend it. Introduced by Schneier in 1999, attack-defense trees mean to graphically represent how non-atomic goals (either of the attacker or of the defender) decompose into a combination of subgoals, or how they are countered, in an informal manner though. Formal semantics for this informal model have been intensively studied the last decade, in order to enrich the set of formal method tools in risk analysis. We present this broad area of research, while focusing on our recent investigations to equip the model with a dynamic semantics that reflects the course of steps of an attack. In particular, we study natural decision problems, as well as the expressiveness of the model, that incidentally coincides with star-free languages.

Authors

• Sophie Pinchinat

Keywords

No keywords are indexed for this paper.