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.
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.
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.