Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems

Jaime Arias; Carlos E. Budde; Wojciech Penczek; Laure Petrucci; Teofil Sidoruk; Mariëlle Stoelinga

doi:10.1007/978-3-030-63406-3_1

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems

Jaime Arias, Carlos E. Budde^*, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk, Mariëlle Stoelinga

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

12 Citations (Scopus)

69 Downloads (Pure)

Abstract

Attack-Defence Trees (ADTrees) are a well-suited formalism to assess possible attacks to systems and the efficiency of counter-measures. This paper extends the available ADTree constructs with reactive patterns that cover further security scenarios, and equips all constructs with attributes such as time and cost to allow for quantitative analyses. We model ADTrees as (an extension of) Asynchronous Multi-Agents Systems: EAMAS. The ADTree–EAMAS transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction, e.g. the maximum time a defence can take to block an attack. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools. We developed the open-source tool adt2amas implementing our transformation.

Original language	English
Title of host publication	Formal Methods and Software Engineering
Subtitle of host publication	22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings
Editors	Shang-Wei Lin, Zhe Hou, Brendan Mahoney
Place of Publication	Cham
Publisher	Springer
Pages	3-19
Number of pages	17
ISBN (Electronic)	978-3-030-63406-3
ISBN (Print)	978-3-030-63405-6
DOIs	https://doi.org/10.1007/978-3-030-63406-3_1
Publication status	Published - 19 Dec 2020
Event	22nd International Conference on Formal Engineering Methods, ICFEM 2020 - National University of Singapore, Singapore, Singapore Duration: 1 Mar 2021 → 3 Mar 2021 Conference number: 22 https://formal-analysis.com/icfem/2020/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12531
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Conference on Formal Engineering Methods, ICFEM 2020
Abbreviated title	ICFEM
Country/Territory	Singapore
City	Singapore
Period	1/03/21 → 3/03/21
Internet address	https://formal-analysis.com/icfem/2020/

Keywords

2021 OA procedure

Access to Document

10.1007/978-3-030-63406-3_1

Arias2020hackersFinal published version, 609 KBLicence: Taverne

Cite this

Arias, J., Budde, C. E., Penczek, W., Petrucci, L., Sidoruk, T., & Stoelinga, M. (2020). Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. In S.-W. Lin, Z. Hou, & B. Mahoney (Eds.), Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings (pp. 3-19). (Lecture Notes in Computer Science; Vol. 12531). Springer. https://doi.org/10.1007/978-3-030-63406-3_1

Arias, Jaime ; Budde, Carlos E. ; Penczek, Wojciech et al. / Hackers vs. Security : Attack-Defence Trees as Asynchronous Multi-agent Systems. Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings. editor / Shang-Wei Lin ; Zhe Hou ; Brendan Mahoney. Cham : Springer, 2020. pp. 3-19 (Lecture Notes in Computer Science).

@inbook{8241e78b6000460d8e03ccc79f808de8,

title = "Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems",

abstract = "Attack-Defence Trees (ADTrees) are a well-suited formalism to assess possible attacks to systems and the efficiency of counter-measures. This paper extends the available ADTree constructs with reactive patterns that cover further security scenarios, and equips all constructs with attributes such as time and cost to allow for quantitative analyses. We model ADTrees as (an extension of) Asynchronous Multi-Agents Systems: EAMAS. The ADTree–EAMAS transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction, e.g. the maximum time a defence can take to block an attack. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools. We developed the open-source tool adt2amas implementing our transformation.",

keywords = "2021 OA procedure",

author = "Jaime Arias and Budde, \{Carlos E.\} and Wojciech Penczek and Laure Petrucci and Teofil Sidoruk and Mari{\"e}lle Stoelinga",

note = "Funding Information: This work was partially funded by the NWO project SEQUOIA, the PHC van Gogh project PAMPAS, the BQR project AMoJAS, and the IEA project PARTIES. Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 22nd International Conference on Formal Engineering Methods, ICFEM 2020, ICFEM ; Conference date: 01-03-2021 Through 03-03-2021",

year = "2020",

month = dec,

day = "19",

doi = "10.1007/978-3-030-63406-3\_1",

language = "English",

isbn = "978-3-030-63405-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "3--19",

editor = "Shang-Wei Lin and Zhe Hou and Brendan Mahoney",

booktitle = "Formal Methods and Software Engineering",

address = "Germany",

url = "https://formal-analysis.com/icfem/2020/",

}

Arias, J, Budde, CE, Penczek, W, Petrucci, L, Sidoruk, T & Stoelinga, M 2020, Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. in S-W Lin, Z Hou & B Mahoney (eds), Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12531, Springer, Cham, pp. 3-19, 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, 1/03/21. https://doi.org/10.1007/978-3-030-63406-3_1

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. / Arias, Jaime; Budde, Carlos E.; Penczek, Wojciech et al.
Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings. ed. / Shang-Wei Lin; Zhe Hou; Brendan Mahoney. Cham: Springer, 2020. p. 3-19 (Lecture Notes in Computer Science; Vol. 12531).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Hackers vs. Security

T2 - 22nd International Conference on Formal Engineering Methods, ICFEM 2020

AU - Arias, Jaime

AU - Budde, Carlos E.

AU - Penczek, Wojciech

AU - Petrucci, Laure

AU - Sidoruk, Teofil

AU - Stoelinga, Mariëlle

N1 - Conference code: 22

PY - 2020/12/19

Y1 - 2020/12/19

N2 - Attack-Defence Trees (ADTrees) are a well-suited formalism to assess possible attacks to systems and the efficiency of counter-measures. This paper extends the available ADTree constructs with reactive patterns that cover further security scenarios, and equips all constructs with attributes such as time and cost to allow for quantitative analyses. We model ADTrees as (an extension of) Asynchronous Multi-Agents Systems: EAMAS. The ADTree–EAMAS transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction, e.g. the maximum time a defence can take to block an attack. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools. We developed the open-source tool adt2amas implementing our transformation.

AB - Attack-Defence Trees (ADTrees) are a well-suited formalism to assess possible attacks to systems and the efficiency of counter-measures. This paper extends the available ADTree constructs with reactive patterns that cover further security scenarios, and equips all constructs with attributes such as time and cost to allow for quantitative analyses. We model ADTrees as (an extension of) Asynchronous Multi-Agents Systems: EAMAS. The ADTree–EAMAS transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction, e.g. the maximum time a defence can take to block an attack. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools. We developed the open-source tool adt2amas implementing our transformation.

KW - 2021 OA procedure

U2 - 10.1007/978-3-030-63406-3_1

DO - 10.1007/978-3-030-63406-3_1

M3 - Chapter

SN - 978-3-030-63405-6

T3 - Lecture Notes in Computer Science

SP - 3

EP - 19

BT - Formal Methods and Software Engineering

A2 - Lin, Shang-Wei

A2 - Hou, Zhe

A2 - Mahoney, Brendan

PB - Springer

CY - Cham

Y2 - 1 March 2021 through 3 March 2021

ER -

Arias J, Budde CE, Penczek W, Petrucci L, Sidoruk T, Stoelinga M. Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. In Lin SW, Hou Z, Mahoney B, editors, Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings. Cham: Springer. 2020. p. 3-19. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-63406-3_1

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this