Quantitative Attack Tree Analysis via Priced Timed Automata

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 13 Citations

Abstract

The success of a security attack crucially depends on the resources available to an attacker: time, budget, skill level, and risk appetite. Insight in these dependencies and the most vulnerable system parts is key to providing effective counter measures. This paper considers attack trees, one of the most prominent security formalisms for threat analysis. We provide an effective way to compute the resources needed for a successful attack, as well as the associated attack paths. These paths provide the optimal ways, from the perspective of the attacker, to attack the system, and provide a ranking of the most vulnerable system parts. By exploiting the priced timed automaton model checker Uppaal CORA, we realize important advantages over earlier attack tree analysis methods: we can handle more complex gates, temporal dependencies between attack steps, shared subtrees, and realistic, multi-parametric cost structures. Furthermore, due to its compositionality, our approach is flexible and easy to extend. We illustrate our approach with several standard case studies from the literature, showing that our method agrees with existing analyses of these cases, and can incorporate additional data, leading to more informative results.
LanguageUndefined
Title of host publicationProceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015)
EditorsSriram Sankaranarayanan, Enrico Vicario
Place of PublicationZurich
PublisherSpringer International Publishing
Pages156-171
Number of pages16
ISBN (Print)978-3-319-22974-4
DOIs
StatePublished - Sep 2015
Event13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015 - Universidad Complutense de Madrid, Madrid, Spain
Duration: 2 Sep 20154 Sep 2015
Conference number: 13
http://formats2015.unifi.it/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9268
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015
Abbreviated titleFORMATS
CountrySpain
CityMadrid
Period2/09/154/09/15
Internet address

Keywords

  • EC Grant Agreement nr.: FP7/318003
  • EWI-25869
  • FMT-MC: MODEL CHECKING
  • EC Grant Agreement nr.: FP7/2007-2013
  • Model Checking
  • IR-97025
  • Socio-technical security
  • Case Studies
  • Attack Tree
  • Attacker Profile
  • METIS-312524
  • Uppaal Cora

Cite this

Kumar, R., Ruijters, E. J. J., & Stoelinga, M. I. A. (2015). Quantitative Attack Tree Analysis via Priced Timed Automata. In S. Sankaranarayanan, & E. Vicario (Eds.), Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015) (pp. 156-171). (Lecture Notes in Computer Science; Vol. 9268). Zurich: Springer International Publishing. DOI: 10.1007/978-3-319-22975-1_11
Kumar, Rajesh ; Ruijters, Enno Jozef Johannes ; Stoelinga, Mariëlle Ida Antoinette. / Quantitative Attack Tree Analysis via Priced Timed Automata. Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015). editor / Sriram Sankaranarayanan ; Enrico Vicario. Zurich : Springer International Publishing, 2015. pp. 156-171 (Lecture Notes in Computer Science).
@inproceedings{cc5c54fe273a4270a7ed5dae02088af0,
title = "Quantitative Attack Tree Analysis via Priced Timed Automata",
abstract = "The success of a security attack crucially depends on the resources available to an attacker: time, budget, skill level, and risk appetite. Insight in these dependencies and the most vulnerable system parts is key to providing effective counter measures. This paper considers attack trees, one of the most prominent security formalisms for threat analysis. We provide an effective way to compute the resources needed for a successful attack, as well as the associated attack paths. These paths provide the optimal ways, from the perspective of the attacker, to attack the system, and provide a ranking of the most vulnerable system parts. By exploiting the priced timed automaton model checker Uppaal CORA, we realize important advantages over earlier attack tree analysis methods: we can handle more complex gates, temporal dependencies between attack steps, shared subtrees, and realistic, multi-parametric cost structures. Furthermore, due to its compositionality, our approach is flexible and easy to extend. We illustrate our approach with several standard case studies from the literature, showing that our method agrees with existing analyses of these cases, and can incorporate additional data, leading to more informative results.",
keywords = "EC Grant Agreement nr.: FP7/318003, EWI-25869, FMT-MC: MODEL CHECKING, EC Grant Agreement nr.: FP7/2007-2013, Model Checking, IR-97025, Socio-technical security, Case Studies, Attack Tree, Attacker Profile, METIS-312524, Uppaal Cora",
author = "Rajesh Kumar and Ruijters, {Enno Jozef Johannes} and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
note = "Foreground = 80{\%}; Type of activity = Conference; Main leader = UT; Type of audience = scientific community, industry; Size of audience = 50; Countries addressed = International;",
year = "2015",
month = "9",
doi = "10.1007/978-3-319-22975-1_11",
language = "Undefined",
isbn = "978-3-319-22974-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "156--171",
editor = "Sriram Sankaranarayanan and Enrico Vicario",
booktitle = "Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015)",

}

Kumar, R, Ruijters, EJJ & Stoelinga, MIA 2015, Quantitative Attack Tree Analysis via Priced Timed Automata. in S Sankaranarayanan & E Vicario (eds), Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015). Lecture Notes in Computer Science, vol. 9268, Springer International Publishing, Zurich, pp. 156-171, 13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015, Madrid, Spain, 2/09/15. DOI: 10.1007/978-3-319-22975-1_11

Quantitative Attack Tree Analysis via Priced Timed Automata. / Kumar, Rajesh; Ruijters, Enno Jozef Johannes; Stoelinga, Mariëlle Ida Antoinette.

Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015). ed. / Sriram Sankaranarayanan; Enrico Vicario. Zurich : Springer International Publishing, 2015. p. 156-171 (Lecture Notes in Computer Science; Vol. 9268).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Quantitative Attack Tree Analysis via Priced Timed Automata

AU - Kumar,Rajesh

AU - Ruijters,Enno Jozef Johannes

AU - Stoelinga,Mariëlle Ida Antoinette

N1 - Foreground = 80%; Type of activity = Conference; Main leader = UT; Type of audience = scientific community, industry; Size of audience = 50; Countries addressed = International;

PY - 2015/9

Y1 - 2015/9

N2 - The success of a security attack crucially depends on the resources available to an attacker: time, budget, skill level, and risk appetite. Insight in these dependencies and the most vulnerable system parts is key to providing effective counter measures. This paper considers attack trees, one of the most prominent security formalisms for threat analysis. We provide an effective way to compute the resources needed for a successful attack, as well as the associated attack paths. These paths provide the optimal ways, from the perspective of the attacker, to attack the system, and provide a ranking of the most vulnerable system parts. By exploiting the priced timed automaton model checker Uppaal CORA, we realize important advantages over earlier attack tree analysis methods: we can handle more complex gates, temporal dependencies between attack steps, shared subtrees, and realistic, multi-parametric cost structures. Furthermore, due to its compositionality, our approach is flexible and easy to extend. We illustrate our approach with several standard case studies from the literature, showing that our method agrees with existing analyses of these cases, and can incorporate additional data, leading to more informative results.

AB - The success of a security attack crucially depends on the resources available to an attacker: time, budget, skill level, and risk appetite. Insight in these dependencies and the most vulnerable system parts is key to providing effective counter measures. This paper considers attack trees, one of the most prominent security formalisms for threat analysis. We provide an effective way to compute the resources needed for a successful attack, as well as the associated attack paths. These paths provide the optimal ways, from the perspective of the attacker, to attack the system, and provide a ranking of the most vulnerable system parts. By exploiting the priced timed automaton model checker Uppaal CORA, we realize important advantages over earlier attack tree analysis methods: we can handle more complex gates, temporal dependencies between attack steps, shared subtrees, and realistic, multi-parametric cost structures. Furthermore, due to its compositionality, our approach is flexible and easy to extend. We illustrate our approach with several standard case studies from the literature, showing that our method agrees with existing analyses of these cases, and can incorporate additional data, leading to more informative results.

KW - EC Grant Agreement nr.: FP7/318003

KW - EWI-25869

KW - FMT-MC: MODEL CHECKING

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - Model Checking

KW - IR-97025

KW - Socio-technical security

KW - Case Studies

KW - Attack Tree

KW - Attacker Profile

KW - METIS-312524

KW - Uppaal Cora

U2 - 10.1007/978-3-319-22975-1_11

DO - 10.1007/978-3-319-22975-1_11

M3 - Conference contribution

SN - 978-3-319-22974-4

T3 - Lecture Notes in Computer Science

SP - 156

EP - 171

BT - Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015)

PB - Springer International Publishing

CY - Zurich

ER -

Kumar R, Ruijters EJJ, Stoelinga MIA. Quantitative Attack Tree Analysis via Priced Timed Automata. In Sankaranarayanan S, Vicario E, editors, Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015). Zurich: Springer International Publishing. 2015. p. 156-171. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-22975-1_11