Quantifying the Odds in Real World Attack Scenarios

In cyber security an important part of risk analysis for IT systems is threat analysis. Threat analysis is an indispensable prerequisite for the planning and budgeting of efficient defense measures. This paper describes a strictly formal method for modeling realistic cyber-attack scenarios. These scenarios are modeled as Discrete Time Markov Decision Processes, opening the opportunity for the application of formal methods to calculate quantitative success probabilities of cyber threats depending on the attacker's skill level and the victim's infrastructure and defense measures. Techniques and tools of probabilistic model checking are applied to find quantitative answers to important questions relevant in threat analysis, such as the attacker's minimum and maximum success probabilities in the victim's IT environment. This provides valuable decision support for security managers when they are forced to assess different security measures in the course of deciding which measure to implement under given budget constraints. To guarantee the practical relevance of the method, a list of 159 attack actions and a list of 118 defense actions are compiled, where the information is gained from several proven tactical and technical knowledge bases. An example - stealing confidential data - shows the application of the method. For calculating probabilities, the model checking tool PRISM is used.