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 language | English |
---|---|
Title of host publication | 29th IEEE Computer Security Foundations Symposium, CSF 2016 |
Place of Publication | Piscataway, NJ |
Publisher | IEEE |
Pages | 105-119 |
Number of pages | 15 |
ISBN (Print) | 978-1-5090-2607-4 |
DOIs | |
Publication status | Published - Jun 2016 |
Event | 29th IEEE Computer Security Foundations Symposium, CSF 2016 - Lisbon, Portugal Duration: 27 Jun 2016 → 1 Jul 2016 Conference number: 29 |
Publication series
Name | IEEE Computer Security Foundations Symposium (CSF) |
---|---|
Publisher | IEEE Computer Society |
Volume | 2016 |
ISSN (Print) | 2374-8303 |
Conference
Conference | 29th IEEE Computer Security Foundations Symposium, CSF 2016 |
---|---|
Abbreviated title | CSF |
Country/Territory | Portugal |
City | Lisbon |
Period | 27/06/16 → 1/07/16 |
Keywords
- EC Grant Agreement nr.: FP7/318003
- Security
- Semantics
- Probabilistic logic
- Markov processes
- Model checking
- EC Grant Agreement nr.: FP7/2007-2013
- Games