On Validating Attack Trees with Attack Effects: An Approach from Barwise-Seligman's Channel Theory

TL;DR

This paper enhances attack trees with attack effects using Barwise-Seligman's channel theory, enabling formal validation of attack decompositions and improving security analysis accuracy.

Contribution

It introduces a formal framework that incorporates attack effects into attack trees, allowing systematic evaluation and validation of attack decompositions.

Findings

Formal definition of attack decomposition consistency

Application to vehicular network security case study

Discussion on mitigation strategies based on attack effects

Abstract

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.