Quantitative Verification and Synthesis of Attack-Defence Scenarios Conference

Zaruhi Aslanyan, Flemming Nielson, David Parker

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

    30 Citations (Scopus)

    Abstract

    Attack-defence trees are a powerful technique for formally evaluating attack-defence scenarios. They represent in an intuitive, graphical way the interaction between an attacker and a defender who compete in order to achieve conflicting objectives. We propose a novel framework for the formal analysis of quantitative properties of complex attack-defence scenarios, using an extension of attack-defence trees which models temporal ordering of actions and allows explicit dependencies in the strategies adopted by attackers and defenders. We adopt a game-theoretic approach, translating attack-defence trees to two-player stochastic games, and then employ probabilistic model checking techniques to formally analyse these models. This provides a means to both verify formally specified security properties of the attack-defence scenarios and, dually, to synthesise strategies for attackers or defenders which guarantee or optimise some quantitative property, such as the probability of a successful attack, the expected cost incurred, or some multi-objective trade-off between the two. We implement our approach, building upon the PRISM-games model checker, and apply it to a case study of an RFID goods management system.
    Original languageEnglish
    Title of host publication29th IEEE Computer Security Foundations Symposium, CSF 2016
    Place of PublicationPiscataway, NJ
    PublisherIEEE Computer Society
    Pages105-119
    Number of pages15
    ISBN (Print)978-1-5090-2607-4
    DOIs
    Publication statusPublished - Jun 2016

    Publication series

    NameIEEE Computer Security Foundations Symposium (CSF)
    PublisherIEEE Computer Society
    Volume2016
    ISSN (Print)2374-8303

      Fingerprint

    Keywords

    • EC Grant Agreement nr.: FP7/318003
    • Security
    • Semantics
    • Probabilistic logic
    • Markov processes
    • Model checking
    • EC Grant Agreement nr.: FP7/2007-2013
    • Games

    Cite this

    Aslanyan, Z., Nielson, F., & Parker, D. (2016). Quantitative Verification and Synthesis of Attack-Defence Scenarios Conference. In 29th IEEE Computer Security Foundations Symposium, CSF 2016 (pp. 105-119). (IEEE Computer Security Foundations Symposium (CSF); Vol. 2016). Piscataway, NJ: IEEE Computer Society. https://doi.org/10.1109/CSF.2016.15