Model checking exact cost for attack scenarios

Zaruhi Aslanyan, Flemming Nielson

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


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
Publication date2017
ISBN (Print)9783662544549
Publication statusPublished - 2017
EventPrinciples of Security and Trust. 6th International Conference - Uppsala, Sweden
Duration: 22 Apr 201729 Apr 2017


ConferencePrinciples of Security and Trust. 6th International Conference
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


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


Dive into the research topics of 'Model checking exact cost for attack scenarios'. Together they form a unique fingerprint.

Cite this