  In security analysis, attack trees are a major tool for showing the
structural decomposition of attacks and for supporting the evaluation of the
quantitative properties (called attributes) of the attacks. However, the
validities of decompositions are not established by attack trees themselves,
and fallacious decisions about security may be made when the attack trees are
inaccurate. This paper enriches attack trees with effects of attacks, with a
formal system focusing on refinement scenarios. Relationships among effects
indicate relationships among attacks and it allows for a systematic evaluation
of attack decompositions. To describe effects this paper applies
Barwise-Seligman's channel theory. Infomorphisms, in particular, play a
significant role to connect effects with distinct granularities. As a result,
the consistency of a decomposition is formally defined and a condition for it
is stated. This framework is applied to a case study of a vehicular network
system. As an application of the idea of consistency, possible degrees of
mitigation for attacks in attack trees are discussed.
