Towards Unconditional Soundness: Computationally Complete Symbolic Attacker
Towards Unconditional Soundness: Computationally Complete Symbolic Attacker
复制标题
DOI：
10.1007/978-3-642-28641-4_11
复制
发表时间：
2012-03
期刊：
影响因子：
--
通讯作者：
G. Bana;Hubert Comon-Lundh
中科院分区：
文献类型：
--
作者：
G. Bana;Hubert Comon-Lundh
我们考虑的问题，充分的符号模型与计算模型的安全协议的验证。我们既不试图在符号模型中包含反映计算原语属性的属性，也不添加强制符号模型可靠性的计算要求。在本文中，我们提出了一种不同的方法：在符号模型中，一切都是可能的，除非它与计算假设相矛盾。这样，我们几乎通过构造获得了无条件的可靠性。我们不需要假设不存在动态腐败或不存在关键周期，这些都是相关作品中经常使用的假设的例子。我们为任意密码原语和任意协议设置了基本框架，但仅用于跟踪安全属性。
We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.