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

    45 Citations (Scopus)


    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
    Number of pages15
    ISBN (Print)978-1-5090-2607-4
    Publication statusPublished - Jun 2016
    Event29th IEEE Computer Security Foundations Symposium, CSF 2016 - Lisbon, Portugal
    Duration: 27 Jun 20161 Jul 2016
    Conference number: 29

    Publication series

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


    Conference29th IEEE Computer Security Foundations Symposium, CSF 2016
    Abbreviated titleCSF


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


    Dive into the research topics of 'Quantitative Verification and Synthesis of Attack-Defence Scenarios Conference'. Together they form a unique fingerprint.

    Cite this