Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability
Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability
复制标题
DOI：
10.1145/3343508
复制
发表时间：
2019-10
期刊：
影响因子：
--
通讯作者：
G. Bana;Rohit Chadha
中科院分区：
文献类型：
--
作者：
G. Bana;Rohit Chadha
近年来，一种新的安全协议验证方法被开发出来，其目的是结合符号攻击者的优点和无条件可靠性的优点：Bana和Comon(BC)[8]的计算完全的符号攻击者的技术。在这篇文章中，我们认为这种技术的真正突破是最近引入了它的不可区分版本[9]，因为随着我们在这里介绍的扩展，第一次有了一种计算上可靠的符号技术，它在语法上是惊人的简单的，翻译标准的计算安全概念是一件直截了当的事情，而且不仅可以有效地用于验证协议的等价性质，而且还可以有效地用于验证协议的踪迹性质。我们首先通过引入几个新的公理来充分开发这个较新版本的核心元素。我们首先通过简单的例子来说明所介绍的公理的威力和不同的用法。我们引入了一个公理来表示决策的Diffie-Hellman性质。我们分析了Diffie-Hellman密钥交换，包括其最简单的形式和认证版本。我们为多个会话的Diffie-Hellman密钥交换协议的真实或随机保密性提供了计算上可靠的验证，除了DDH假设之外，没有对计算实现的任何限制。我们还展示了使用用于数字签名的UF-CMA假设的站到站协议的简化版本的认证。最后，我们对IND-CPA、IND-CCA1和IND-CCA2安全属性进行了公理化，并举例说明了它们的用法。我们在交互式定理证明器Coq中形式化了公理系统，并对Diffie-Hellman和站到站协议的各种辅助定理和安全性质的证明进行了机器验证。
In recent years, a new approach has been developed for verifying security protocols with the aim of combining the benefits of symbolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [8]. In this article, we argue that the real breakthrough of this technique is the recent introduction of its version for indistinguishability [9], because, with the extensions we introduce here, for the first time, there is a computationally sound symbolic technique that is syntactically strikingly simple, to which translating standard computational security notions is a straightforward matter, and that can be effectively used for verification of not only equivalence properties but trace properties of protocols as well. We first fully develop the core elements of this newer version by introducing several new axioms. We illustrate the power and the diverse use of the introduced axioms on simple examples first. We introduce an axiom expressing the Decisional Diffie-Hellman property. We analyze the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. We provide computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol for multiple sessions, without any restrictions on the computational implementation other than the DDH assumption. We also show authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, we axiomatize IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. We have formalized the axiomatic system in an interactive theorem prover, Coq, and have machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol.