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.

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems / Arias, J.; Budde, C. E.; Penczek, W.; Petrucci, L.; Sidoruk, T.; Stoelinga, M.. - ELETTRONICO. - 12531:(2020), pp. 3-19. (Intervento presentato al convegno 22nd International Conference on Formal Engineering Methods, ICFEM 2020 tenutosi a Singapore nel 1-3 March 2020) [10.1007/978-3-030-63406-3_1].

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

Budde, C. E.;Petrucci, L.;
2020-01-01

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.
2020
Proceedings of the 22nd International Conference on Formal Engineering Methods, ICFEM 2020
Switzerland
Springer Nature Switzerland AG
978-3-030-63405-6
978-3-030-63406-3
Arias, J.; Budde, C. E.; Penczek, W.; Petrucci, L.; Sidoruk, T.; Stoelinga, M.
Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems / Arias, J.; Budde, C. E.; Penczek, W.; Petrucci, L.; Sidoruk, T.; Stoelinga, M.. - ELETTRONICO. - 12531:(2020), pp. 3-19. (Intervento presentato al convegno 22nd International Conference on Formal Engineering Methods, ICFEM 2020 tenutosi a Singapore nel 1-3 March 2020) [10.1007/978-3-030-63406-3_1].
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Descrizione: Article camera-ready
Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 517.55 kB
Formato Adobe PDF
517.55 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/314668
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact