<div dir="ltr"><div class="gmail_quote"><div dir="ltr" class="gmail_attr">From: <strong class="gmail_sendername" dir="auto">grarpamp</strong> <span dir="auto"><<a href="mailto:grarpamp@gmail.com">grarpamp@gmail.com</a>></span><br><br></div><div dir="ltr" class="gmail_attr">(Posted on <a href="mailto:cypherpunks@cpunks.org">cypherpunks@cpunks.org</a>)</div><br><a href="https://arxiv.org/abs/1910.13772" rel="noreferrer" target="_blank">https://arxiv.org/abs/1910.13772</a><br>
<br>
After several years of research on onion routing, Camenisch and<br>
Lysyanskaya, in an attempt at rigorous analysis, defined an ideal<br>
functionality in the universal composability model, together with<br>
properties that protocols have to meet to achieve provable security. A<br>
whole family of systems based their security proofs on this work.<br>
However, analyzing HORNET and Sphinx, two instances from this family,<br>
we show that this proof strategy is broken. We discover a previously<br>
unknown vulnerability that breaks anonymity completely, and explain a<br>
known one. Both should not exist if privacy is proven correctly. In<br>
this work, we analyze and fix the proof strategy used for this family<br>
of systems. After proving the efficacy of the ideal functionality, we<br>
show how the original properties are flawed and suggest improved,<br>
effective properties in their place. Finally, we discover another<br>
common mistake in the proofs. We demonstrate how to avoid it by<br>
showing our improved properties for one protocol, thus partially<br>
fixing the family of provably secure onion routing protocols.<br>
</div></div>