Formal Analysis of Graphical Security Models

Zaruhi Aslanyan

Research output: Book/ReportPh.D. thesisResearch

592 Downloads (Pure)

Abstract

The increasing usage of computer-based systems in almost every aspects of our daily life makes more and more dangerous the threat posed by potential attackers, and more and more rewarding a successful attack. Moreover, the complexity of these systems is also increasing, including physical devices, software components and human actors interacting with each other to form so-called socio-technical systems. The importance of socio-technical systems to modern societies requires verifying their security properties formally, while their inherent complexity makes manual analyses impracticable.

Graphical models for security offer an unrivalled opportunity to describe socio-technical systems, for they allow to represent different aspects like human behaviour, computation and physical phenomena in an abstract yet uniform manner. Moreover, these models can be assigned a formal semantics, thereby allowing formal verification of their properties. Finally, their appealing graphical notations enable to communicate security concerns in an understandable way also to non-experts, often in charge of the decision making.

This dissertation argues that automated techniques can be developed on graphical security models to evaluate qualitative and quantitative security properties of socio-technical systems and to synthesise optimal attack and defence strategies.

In support to this claim we develop analysis techniques for widely-used graphical security models such as attack trees and attack-defence trees. Our analyses cope with the optimisation of multiple parameters of an attack and defence scenario. Improving on the literature, in case of conflicting parameters such as probability and cost we compute the set of optimal solutions in terms of Pareto efficiency. Moreover, we investigate the relation between attack and attack-defence trees and stochastic models in a verification-oriented setting, with the aim of levering the great many mature tools and analysis techniques developed for instance in the area of games.
Original languageEnglish
Place of PublicationKgs. Lyngby
PublisherTechnical University of Denmark
Number of pages208
Publication statusPublished - 2017
SeriesDTU Compute PHD-2016
Number421
ISSN0909-3192

Projects

Stochastic Model Checking of Socio- Technical Models

Aslanyan, Z., Nielson, F., Probst, C. W., Lluch Lafuente, A., Hansen, R. R. & Legay, A.

1/3 FUU, 1/3 inst 1/3 Andet

01/07/201323/11/2016

Project: PhD

Cite this

Aslanyan, Z. (2017). Formal Analysis of Graphical Security Models. Technical University of Denmark. DTU Compute PHD-2016, No. 421