Formalizing Real-World Threat Scenarios

Using formal methods in threat analysis would be of great benefit to securing modern IT systems. To this end a strictly formal description of attacker-defender scenarios is vital. This paper demonstrates how attacker and defender behavior and its interrelationship can be defined using Markov decision processes and stochastic game theory. Based on these definitions, model checking methods can be applied to find quantitative answers to important questions relevant in threat analysis. A main focus lies on the applicability of the method to real-world situations. This is accomplished by incorporating information from several proven tactical and technical knowledge bases. Practicability of the method is shown by using the model checking tool PRISM-games.