ATM: a Logic for Quantitative Security Properties on Attack Trees
Stefano Maria Nicoletti, Milan Lopuhaä-Zwakenberg, Ernst Moritz Hahn, Mariëlle I. A. Stoelinga · Software & Systems Modeling · 2025
Abstract Critical infrastructure systems — for which high reliability and availability are paramount — must operate securely. Attack trees (ATs) are hierarchical diagrams that offer a flexible modelling language used to assess how systems can be attacked. ATs are widely employed both in industry and academia but — in spite of their popularity — little work has been done to give practitioners instruments to formulate queries on ATs in an understandable yet powerful way. In this paper we fill this gap by presenting $$\textsf {ATM}$$ ATM , a logic to express quantitative security properties on ATs. $$\textsf {ATM}$$ ATM allows for the specification of properties involved with security metrics that include “cost”, “probability” and “skill” and permits the formulation of insightful what-if scenarios. To showcase its potential, we apply $$\textsf {ATM}$$ ATM both to the case study of a CubeSAT and to a larger model, constructed from the real-life cyberespionage campaign Operation Dream Job , as recorded by the MITRE ATT&CK Database. We showcase property specification on the corresponding attack trees and propel usability of $$\textsf {ATM}$$ ATM by presenting $$\textsf {LangATM}$$ LangATM – a domain specific language for our logic. Finally, we present theory and algorithms — based on binary decision diagrams — to check properties and compute metrics of $$\textsf {ATM}$$ ATM -formulae.