We provide the first formal foundation of
attack trees which are a popular extension of the well-known attack trees. The
attack tree formalism increases the expressivity of attack trees by introducing the sequential conjunctive operator
. This operator enables the modeling of ordered events.
We give a semantics to
attack trees by interpreting them as sets of series-parallel graphs and propose a complete axiomatization of this semantics. We define normal forms for
attack trees and a term rewriting system which allows identification of semantically equivalent trees. Finally, we formalize how to quantitatively analyze
attack trees using attributes.