Quantitative Verification and Synthesis of Attack-Defence Scenarios

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

Standard

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

Proceedings 29th IEEE Computer Security Foundations Symposium (CSF'16). IEEE Xplore, 2016.

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

Harvard

Aslanyan, Z, Nielson , F & Parker, D 2016, Quantitative Verification and Synthesis of Attack-Defence Scenarios. in Proceedings 29th IEEE Computer Security Foundations Symposium (CSF'16). IEEE Xplore, 29th IEEE Computer Security Foundations Symposium (CSF'16), Lisbon, Portugal, 29/06/16. https://doi.org/10.1109/CSF.2016.15

APA

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

Vancouver

Aslanyan Z, Nielson F, Parker D. Quantitative Verification and Synthesis of Attack-Defence Scenarios. In Proceedings 29th IEEE Computer Security Foundations Symposium (CSF'16). IEEE Xplore. 2016 https://doi.org/10.1109/CSF.2016.15

Author

Aslanyan, Zaruhi ; Nielson , Flemming ; Parker, David. / Quantitative Verification and Synthesis of Attack-Defence Scenarios. Proceedings 29th IEEE Computer Security Foundations Symposium (CSF'16). IEEE Xplore, 2016.

Bibtex

@inproceedings{96003246ba4a4f2d979577e477144588,
title = "Quantitative Verification and Synthesis of Attack-Defence Scenarios",
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 conflictingobjectives. 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 adopta 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, tosynthesise 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, andapply it to a case study of an RFID goods management system.",
keywords = "attack-defence trees, stochastic games, formal verification, probabilistic model checking",
author = "Zaruhi Aslanyan and Flemming Nielson and David Parker",
year = "2016",
month = aug,
day = "11",
doi = "10.1109/CSF.2016.15",
language = "English",
booktitle = "Proceedings 29th IEEE Computer Security Foundations Symposium (CSF'16)",
publisher = "IEEE Xplore",
note = "29th IEEE Computer Security Foundations Symposium (CSF'16) ; Conference date: 29-06-2016 Through 01-07-2016",

}

RIS

TY - GEN

T1 - Quantitative Verification and Synthesis of Attack-Defence Scenarios

AU - Aslanyan, Zaruhi

AU - Nielson , Flemming

AU - Parker, David

PY - 2016/8/11

Y1 - 2016/8/11

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 conflictingobjectives. 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 adopta 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, tosynthesise 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, andapply 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 conflictingobjectives. 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 adopta 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, tosynthesise 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, andapply it to a case study of an RFID goods management system.

KW - attack-defence trees

KW - stochastic games

KW - formal verification

KW - probabilistic model checking

U2 - 10.1109/CSF.2016.15

DO - 10.1109/CSF.2016.15

M3 - Conference contribution

BT - Proceedings 29th IEEE Computer Security Foundations Symposium (CSF'16)

PB - IEEE Xplore

T2 - 29th IEEE Computer Security Foundations Symposium (CSF'16)

Y2 - 29 June 2016 through 1 July 2016

ER -