Quantitative Attack Tree Analysis via Priced Timed Automata

Rajesh Kumar, Enno Jozef Johannes Ruijters, Mariëlle Ida Antoinette Stoelinga

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

    27 Citations (Scopus)

    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.
    Original 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
    Pages156-171
    Number of pages16
    ISBN (Print)978-3-319-22974-4
    DOIs
    Publication statusPublished - 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. https://doi.org/10.1007/978-3-319-22975-1_11