The problem this article addresses is, given a formal specification of a system, how to produce an attack tree that correctly and clearly describes the ways the system can be attacked. Correctness means that the attacks displayed by the attack tree are indeed attacks in the system; clarity means that the tree is efficient in communicating the attack scenario. To pursue clarity, we introduce an attack-tree generation algorithm that minimises the tree size and the information length of its labels without sacrificing correctness. We achieve this by establishing a connection between the problem of factorising algebraic expressions and the problem of minimising the tree size. Notably, our generation algorithm can handle complex attacks that execute actions in parallel and sequentially. For completeness, we introduce a system model that integrates well with our generation approach, and validate the resulting framework via a running example.

翻译：本文针对的问题是如何根据系统的形式化规范，生成准确且清晰地描述系统可能被攻击路径的攻击树。准确性意味着攻击树呈现的攻击行为确实是系统中的真实攻击；清晰性则要求攻击树能够高效传达攻击场景。为追求清晰性，我们提出一种攻击树生成算法，该算法在不牺牲准确性的前提下最小化树规模及其标签信息长度。通过建立代数表达式因式分解问题与树规模最小化问题之间的联系，我们实现了上述目标。值得注意的是，我们的生成算法能够处理并行与串行执行攻击动作的复杂攻击场景。为完善理论框架，我们引入了一个与生成方法高度集成的系统模型，并通过实例验证了整体框架的有效性。