Model checking exact cost for attack scenarios

Zaruhi Aslanyan, Flemming Nielson

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Attack trees constitute a powerful tool for modelling security threats. Many security analyses of attack trees can be seamlessly expressed as model checking of Markov Decision Processes obtained from the attack trees, thus reaping the benefits of a coherent framework and a mature tool support. However, current model checking does not encompass the exact cost analysis of an attack, which is standard for attack trees. Our first contribution is the logic erPCTL with cost-related operators. The extended logic allows to analyse the probability of an event satisfying given cost bounds and to compute the exact cost of an event. Our second contribution is the model checking algorithm for erPCTL. Finally, we apply our framework to the analysis of attack trees.
Original languageEnglish
Title of host publicationPrinciples of Security and Trust
PublisherSpringer
Publication date2017
Pages210-31
ISBN (Print)9783662544549
DOIs
Publication statusPublished - 2017
EventPrinciples of Security and Trust. 6th International Conference - Uppsala, Sweden
Duration: 22 Apr 201729 Apr 2017

Conference

ConferencePrinciples of Security and Trust. 6th International Conference
CountrySweden
CityUppsala
Period22/04/201729/04/2017
SeriesPrinciples of Security and Trust. 6th International Conference, Post 2017, Held As Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2017. Proceedings: Lncs 10204
SeriesLecture Notes in Computer Science
Volume10204
ISSN0302-9743

Keywords

  • Data security
  • Markov processes
  • Formal logic
  • Formal methods
  • Markov decision processes

Cite this

Aslanyan, Z., & Nielson, F. (2017). Model checking exact cost for attack scenarios. In Principles of Security and Trust (pp. 210-31). Springer. Principles of Security and Trust. 6th International Conference, Post 2017, Held As Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2017. Proceedings: Lncs 10204, Lecture Notes in Computer Science, Vol.. 10204 https://doi.org/10.1007/978-3-662-54455-6_10