Attack trees in Isabelle extended with probabilities for quantum cryptography

In this paper, we present a proof calculus for Attack Trees and how its application to Quantum Cryptography is made possible by extending the framework to probabilistic reasoning on attacks. Attack trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, we succeed in developing a generic theory of attack trees with a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of attack trees and at the same time the developed proof theory enables application to case studies. A central correctness and completeness result proved in Isabelle establishes a connection between the notion of attack tree validity and CTL. Furthermore in this paper, we illustrate the application of Attack Trees to security protocols on the example of the Quantum Key Distribution (QKD) algorithm. The application motivates the extension of the Attack Tree proof calculus by probabilities. We therefore introduce probabilities to quantify finite event sequences and show how this extension can be used to extend CTL to its probabilistic version PCTL. We show on the example of QKD how probabilistic reasoning with PCTL enables proof of quantitative security properties. (C) 2019 Elsevier Ltd. All rights reserved.