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

28 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

Model checking
Radio frequency identification (RFID)
Costs
Statistical Models

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
Aslanyan, Zaruhi ; Nielson, Flemming ; Parker, David. / Quantitative Verification and Synthesis of Attack-Defence Scenarios Conference. 29th IEEE Computer Security Foundations Symposium, CSF 2016. Piscataway, NJ : IEEE Computer Society, 2016. pp. 105-119 (IEEE Computer Security Foundations Symposium (CSF)).
@inproceedings{058b06af717c41679669efc0bdb2b03a,
title = "Quantitative Verification and Synthesis of Attack-Defence Scenarios Conference",
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.",
keywords = "EC Grant Agreement nr.: FP7/318003, Security, Semantics, Probabilistic logic, Markov processes, Model checking, EC Grant Agreement nr.: FP7/2007-2013, Games",
author = "Zaruhi Aslanyan and Flemming Nielson and David Parker",
year = "2016",
month = "6",
doi = "10.1109/CSF.2016.15",
language = "English",
isbn = "978-1-5090-2607-4",
series = "IEEE Computer Security Foundations Symposium (CSF)",
publisher = "IEEE Computer Society",
pages = "105--119",
booktitle = "29th IEEE Computer Security Foundations Symposium, CSF 2016",
address = "United States",

}

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. IEEE Computer Security Foundations Symposium (CSF), vol. 2016, IEEE Computer Society, Piscataway, NJ, pp. 105-119. https://doi.org/10.1109/CSF.2016.15

Quantitative Verification and Synthesis of Attack-Defence Scenarios Conference. / Aslanyan, Zaruhi; Nielson, Flemming; Parker, David.

29th IEEE Computer Security Foundations Symposium, CSF 2016. Piscataway, NJ : IEEE Computer Society, 2016. p. 105-119 (IEEE Computer Security Foundations Symposium (CSF); Vol. 2016).

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

TY - GEN

T1 - Quantitative Verification and Synthesis of Attack-Defence Scenarios Conference

AU - Aslanyan, Zaruhi

AU - Nielson, Flemming

AU - Parker, David

PY - 2016/6

Y1 - 2016/6

N2 - 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.

AB - 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.

KW - EC Grant Agreement nr.: FP7/318003

KW - Security

KW - Semantics

KW - Probabilistic logic

KW - Markov processes

KW - Model checking

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - Games

U2 - 10.1109/CSF.2016.15

DO - 10.1109/CSF.2016.15

M3 - Conference contribution

SN - 978-1-5090-2607-4

T3 - IEEE Computer Security Foundations Symposium (CSF)

SP - 105

EP - 119

BT - 29th IEEE Computer Security Foundations Symposium, CSF 2016

PB - IEEE Computer Society

CY - Piscataway, NJ

ER -

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