Provable Security for the Onion Routing and Mix Network Packet Format Sphinx

Onion routing and mix networks are fundamental concepts to provide users with anonymous access to the Internet. Various corresponding solutions rely on the Sphinx packet format. However, flaws in Sphinx's underlying proof strategy were found recently. It is thus currently unclear which guarantees Sphinx actually provides, and, even worse, there is no suitable proof strategy available. In this paper, we restore the security foundation for all these works by building an analytical framework for Sphinx. We discover that the previously-used Decisional Diffie-Hellman (DDH) assumption is insufficient for a security proof and show that the Gap Diffie-Hellman (GDH) assumption is required instead. We apply it to prove that a slightly adapted version of the Sphinx packet format is secure under the GDH assumption. We are thus, to the best of our knowledge, the first to provide a detailed, in-depth security proof for Sphinx that holds. Our adaptations to Sphinx are necessary, as we demonstrate with an attack on sender privacy that would otherwise be possible in Sphinx's adversary model.