I am studying about TOR. I require to formally verify that the involved protocols provide anonymity. However, I could not find a suitable formalism of anonymity. If there exist any formulation/property that denotes privacy? Your help is appreciated.

  • Questions seeking product recommendations are off-topic as they become obsolete quickly. Instead, describe your situation and the specific problem you're trying to solve. – Lucas Kauffman Jun 4 '15 at 15:28
  • I changed the question here. Please let me know where can I ask about security tools? – remo Jun 4 '15 at 15:50
  • Maybe one of the lists at insecure.org? – Neil Smithline Jun 4 '15 at 16:21
  • 1
    anonymity != privacy. Which property do you want to know about? – schroeder Jun 4 '15 at 19:22
  • 1
    Lookup papers in Google Scholar, using the words "tor", "anonymity", "fingerprinting", look up StegoTorus, and also papers from Danezis and Murdoch who have performed analyses of Tor traffic in the past. – Steve Dodier-Lazaro Jun 5 '15 at 10:58

A formal proof might only be made against a formal specification. In other words: you cannot mathematically prove that a software matches a behavior if you are not able first to mathematically define this behavior.

I have serious doubts that a general concept such as "anonymity" or "privacy" may be formally specified, and therefore that they can be formally proved in any way.

At best you could formally prove that some subset of Tor's technical features work as designed, but not that this designs fulfill any privacy or anonymity goal.

| improve this answer | |

There has been quite amount of work on anonymity in cryptographic protocols. The approaches to this problem are based on various models and proof techniques, e.g., information-theoretic (also called semantics security), complexity theory, and formal methods. Recently, the security of TOR was formally proved in the universal composition (UC) model. You can take a look at this paper "AnoA: A Framework For Analyzing Anonymous Communication Protocols" by Michael Backes and others. Note that the notion of anonymity in this paper is quite weak as it does not consider multiple protocol rounds. In my opinion, there is another definition that captures anonymity better which is based on differential privacy. This might be the right approach you should go for.

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.