[tor-dev] [paper] Breaking and (Partially) Fixing Provably Secure Onion Routing

[Eugen Leitl]

https://arxiv.org/abs/1910.13772

Breaking and (Partially) Fixing Provably Secure Onion Routing

Christiane Kuhn, Martin Beck, Thorsten Strufe

(Submitted on 30 Oct 2019)

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. 

Subjects: 	Cryptography and Security (cs.CR)

Cite as: 	arXiv:1910.13772 [cs.CR] (or arXiv:1910.13772v1 [cs.CR] for
this version)