Attack Defense Trees with Sequential Conjunction

摘要

Attack defense trees are used to show the interaction between potential attacks on a system and the system defenses. In this paper we present a formal semantic model for attack defense trees with sequential composition, allowing for the description of attacks that are performed as a sequence of steps. The main contributions of our work are a formal representation of attack defense trees with sequential conjunction, a demonstration that this representation is equivalent to a process-algebraic one, and an algorithm for identifying the existence of attacks. We illustrate with an attack on over the air updates.