Breaking and (Partially) Fixing Provably Secure Onion Routing
Breaking and (Partially) Fixing Provably Secure Onion Routing
复制标题
破坏和（部分）修复可证明安全的洋葱路由
DOI：
10.1109/sp40000.2020.00039
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
T. Strufe
中科院分区：
文献类型：
--
作者：
C. Kuhn;Martin Beck;T. Strufe
在对洋葱路由进行了几年的研究之后，Camenisch和Lysyanskaya试图进行严格的分析，在通用可组合性模型中定义了一个理想的功能，以及协议必须满足以实现可证明安全性的属性。整个系统家族都基于这项工作进行安全证明。然而，分析HORNET和Sphinx，从这个家庭的两个例子，我们表明，这种证明策略是打破。我们发现了一个以前未知的漏洞，完全打破了匿名性，并解释了一个已知的。在这项工作中，我们分析并修复了用于这一系列系统的证明策略。在证明了理想功能的有效性后，我们展示了原始属性是如何存在缺陷的，并提出了改进的有效属性。最后，我们发现了证明中的另一个常见错误。我们演示了如何避免它，通过展示我们的改进性能的一个协议，从而部分地固定家庭的可证明安全的洋葱路由协议。
After several years of research on onion routing, Camenisch and Lysyanskaya, in an attempt at rigorous analysis, defined an ideal functionality in the universal composability model, together with properties that protocols have to meet to achieve provable security. A whole family of systems based their security proofs on this work. However, analyzing HORNET and Sphinx, two instances from this family, we show that this proof strategy is broken. We discover a previously unknown vulnerability that breaks anonymity completely, and explain a known one. Both should not exist if privacy is proven correctly.In this work, we analyze and fix the proof strategy used for this family of systems. After proving the efficacy of the ideal functionality, we show how the original properties are flawed and suggest improved, effective properties in their place. Finally, we discover another common mistake in the proofs. We demonstrate how to avoid it by showing our improved properties for one protocol, thus partially fixing the family of provably secure onion routing protocols.