Sound Computational Interpretation of Symbolic Hashes in the Standard Model
Sound Computational Interpretation of Symbolic Hashes in the Standard Model
复制标题
标准模型中符号哈希的合理计算解释
DOI：
10.1007/11908739_3
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
P. Rossum
中科院分区：
文献类型：
--
作者：
Flavio D. Garcia;P. Rossum
本文为弥合加密协议验证的形式方法和计算方法之间的差距又迈出了一步。我们扩展了著名的阿巴迪-Rogaway逻辑与概率散列，我们给出了一个精确的语义解释，它使用Canetti的甲骨文散列。这些是隐藏所有部分信息的概率多项式时间散列。最后，我们表明，这种解释是计算的声音。
This paper provides one more step towards bridging the gap between the formal and computational approaches to the verification of cryptographic protocols. We extend the well-known Abadi-Rogaway logic with probabilistic hashes and we give a precise semantic interpretation to it using Canetti’s oracle hashes. These are probabilistic polynomialtime hashes that hide all partial information. Finally, we show that this interpretation is computationally sound.