ATM: A Logic for Quantitative Security Properties on Attack Trees

Stefano M. Nicoletti*, Milan Lopuhaä-Zwakenberg, Ernst Moritz Hahn, Mariëlle Stoelinga

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Downloads (Pure)


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}$$ to the case study of a CubeSAT, presenting three different ways in which an attacker can compromise its availability. We showcase property specification on the corresponding attack tree and we present theory and algorithms—based on binary decision diagrams—to check properties and compute metrics of $$\textsf{ATM}$$ -formulae.

Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
Subtitle of host publication21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings
EditorsCarla Ferreira, Tim A.C. Willemse
Place of PublicationCham
Number of pages21
ISBN (Electronic)978-3-031-47115-5
ISBN (Print)978-3-031-47114-8
Publication statusPublished - 2023
Event21st International Conference on Software Engineering and Formal Methods, SEFM 2023 - Eindhoven University of Technology, Eindhoven, Netherlands
Duration: 6 Nov 202310 Nov 2023
Conference number: 21

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference21st International Conference on Software Engineering and Formal Methods, SEFM 2023
Abbreviated titleSEFM 2023
Internet address


  • 2023 OA procedure


Dive into the research topics of 'ATM: A Logic for Quantitative Security Properties on Attack Trees'. Together they form a unique fingerprint.

Cite this