  Attack trees are a popular way to represent and evaluate potential security
threats on systems or infrastructures. The goal of this work is to provide a
framework allowing to express and check whether an attack tree is consistent
with the analyzed system. We model real systems using transition systems and
introduce attack trees with formally specified node labels. We formulate the
correctness properties of an attack tree with respect to a system and study the
complexity of the corresponding decision problems. The proposed framework can
be used in practice to assist security experts in manual creation of attack
trees and enhance development of tools for automated generation of attack
trees.
