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}\) , a logic to express quantitative security properties on ATs. \(\textsf {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}\) 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}\) by presenting \(\textsf {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}\) -formulae.
