Attack trees in Isabelle extended with probabilities for quantum cryptography
Attack trees in Isabelle extended with probabilities for quantum cryptography
复制标题
DOI：
10.1016/j.cose.2019.101572
复制
发表时间：
2019-11-01
影响因子：
5.6
通讯作者：
Kammueller, Florian
中科院分区：
文献类型：
--
作者：
Kammueller, Florian
在本文中，我们给出了攻击树的证明演算，并通过将该框架扩展到攻击的概率推理，使其在量子密码学中的应用成为可能。攻击树是构建对系统的攻击的一个成熟且有用的模型，因为它们允许逐步探索应用程序场景中的高级攻击。利用高阶逻辑在Isabelle中的表达能力，我们成功地发展了一种通用的攻击树理论，该理论具有基于Klipke结构和CTL的基于状态的语义。由此产生的框架允许对攻击树的证明演算的元理论进行机械支持的逻辑分析，同时，所开发的证明理论能够应用于案例研究。Isabelle证明的一个中心正确性和完备性结果建立了攻击树有效性的概念与CTL之间的联系，并以量子密钥分配(QKD)算法为例说明了攻击树在安全协议中的应用。该应用程序通过概率激励攻击树证明演算的扩展。因此，我们引入概率来量化有限事件序列，并展示了如何使用这种扩展来将CTL扩展到其概率版本PCTL。我们以量子密钥分发为例，说明了基于PCTL的概率推理是如何证明量化安全性质的。(C)2019爱思唯尔有限公司。保留所有权利。
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.