Quantitative Verification and Synthesis of Attack-Defence Scenarios

Zaruhi Aslanyan, Flemming Nielson , David Parker

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

41 Citations (Scopus)
248 Downloads (Pure)


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 publicationProceedings 29th IEEE Computer Security Foundations Symposium (CSF'16)
PublisherIEEE Xplore
ISBN (Electronic)2374-8303
Publication statusE-pub ahead of print - 11 Aug 2016
Event29th IEEE Computer Security Foundations Symposium (CSF'16) - Lisbon, Portugal
Duration: 29 Jun 20161 Jul 2016


Conference29th IEEE Computer Security Foundations Symposium (CSF'16)


  • attack-defence trees
  • stochastic games
  • formal verification
  • probabilistic model checking


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

Cite this