Quantitative Verification and Synthesis of Attack-Defence Scenarios

Zaruhi Aslanyan, Flemming Nielson, David Parker

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

424 Downloads (Pure)

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 publicationProceedings of the 29th IEEE Computer Security Foundations Symposium (CSF 2016)
PublisherIEEE
Publication date2016
Pages105-119
ISBN (Print)978-1-5090-2607-4
DOIs
Publication statusPublished - 2016
Event29th IEEE Computer Security Foundations Symposium (CSF 2016) - Lisaboa, Portugal
Duration: 27 Jun 20161 Jul 2016
Conference number: 29
http://csf2016.tecnico.ulisboa.pt/

Conference

Conference29th IEEE Computer Security Foundations Symposium (CSF 2016)
Number29
CountryPortugal
CityLisaboa
Period27/06/201601/07/2016
Internet address
SeriesI E E E Computer Security Foundations Symposium. Proceedings
ISSN1940-1434

Keywords

  • Attack-defence trees
  • Stochastic games
  • Formal verification
  • Probabilistic model checking

Cite this

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