What is the Exact Security of the Signal Protocol?
What is the Exact Security of the Signal Protocol?
复制标题
信号协议的确切安全性是什么？
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Srinivasan Raghuraman
中科院分区：
文献类型：
--
作者：
Alexander Bienstock;Jaiden Fairoze;Sanjam Garg;Pratyay Mukherjee;Srinivasan Raghuraman
在这项工作中，我们在通用可组合性框架中开发了全面的定义，以研究信号双棘轮（简称信号）协议。我们的定义通过明确捕获许多新的安全保证，除了Alwen，Coretti和Dodis在最先进的工作中已经确定的安全保证之外，还可以对Signal的确切安全性进行更细粒度和更严格的分析[Eurocrypt 2019]。此外，我们的定义提供了使用UC合成定理更容易在Signal之上构建的能力。如白皮书中所述，Signal协议安全地实现了我们理想的功能FSignal。然而，正如我们从白皮书中的高级描述中所解释的那样，FSignal的保证似乎比人们期望Signal满足的保证略弱。因此，我们提供了一个更强大，更自然的定义，通过理想的功能FSignal+形式化。基于我们的定义，我们能够做出如下许多重要的见解：·我们观察到Alwen等人的几个缺点。基于游戏的安全概念。为了证明它们，我们构建了四个不同的Signal协议的修改版本，根据我们较弱的FSignal定义，所有这些版本都是不安全的，但根据它们的定义仍然是安全的。其中，Alwen等人建议使用一种变体;另一个建议由Signal白皮书本身使用。·我们确定了Signal完全安全所需的确切假设。特别是，我们的安全性证明使用了gap-Diffie-Hellman假设和随机预言模型，而不是Alwen等人使用的DDH假设和标准模型。·我们通过展示一个关于该定义的非平凡（尽管很小）弱点，证明了Signal相对于我们更强的功能FSignal+的缺点。·最后，我们通过对Signal进行最小化修改（我们称之为Triple Ratchet）来补充上述弱点，并表明由此产生的协议安全地实现了更强大的功能FSignal+。值得注意的是，这种修改不会产生额外的通信成本，也几乎不会产生额外的计算成本。
In this work we develop comprehensive definitions in the Universal Composability framework to study the Signal Double Ratchet (Signal for short) protocol. Our definitions enable a more fine-grained and rigorous analysis of the exact security of Signal by explicitly capturing many new security guarantees, in addition to the ones that were already identified in the state-of-art work by Alwen, Coretti and Dodis [Eurocrypt 2019]. Moreover, our definitions provide the ability to more easily build on top of Signal, using the UC Composition Theorem. The Signal protocol, as it is described in the whitepaper, securely realizes our ideal functionality FSignal. However, as we interpret from the high-level description in the whitepaper, the guarantees of FSignal seem slightly weaker than those one would expect Signal to satisfy. Therefore we provide a stronger, more natural definition, formalized through the ideal functionality FSignal+ . Based on our definitions we are able to make many important insights as follows: • We observe several shortcomings of Alwen et al.’s game-based security notions. To demonstrate them, we construct four different modified versions of the Signal protocol, all of which are insecure according to our weaker FSignal definition, but remain secure according to their definitions. Among them, one variant was suggested for use by Alwen et al.; another one was suggested for use by the Signal whitepaper itself. • We identify the exact assumptions required for the full security of Signal. In particular, our security proofs use the gap-Diffie-Hellman assumption and the random oracle model, as opposed to the DDH assumption and standard model used in Alwen et al. • We demonstrate the shortcomings of Signal with respect to our stronger functionality FSignal+ by showing a non-trivial (albeit minor) weakness with respect to that definition. • Finally, we complement the above weakness by providing a minimalistic modification to Signal (that we call the Triple Ratchet) and show that the resulting protocol securely realizes the stronger functionality FSignal+ . Remarkably, the modification incurs no additional communication cost and virtually no additional computational cost.