A Framework for Provably Secure Onion Routing against a Global Adversary

Onion routing and mix networks are a central technology to enable anonymous communication on the Internet. As such, a large number of protocols and model variants have been explored in the field, which offer differing levels of privacy, exhibit vulnerabilities, or even supersede each other. These factors make discovering the appropriate formalization for new developments difficult, and some model variants have not been formalized at all. We address this issue by creating one parametrized framework that encompasses the onion routing and mix network models and functionalities with a global adversary in the related work. In doing so, we create a categorization of the variants of onion routing models in use in the related work and map common OR and mix network protocols to their variants. For each identified variant: Our framework offers i) an ideal functionality in the Universal Composability framework, and ii) game-based properties that imply realization of the ideal functionality when a protocol satisfies them. In effect, our framework both unifies and extends previous formalization efforts in the field.