Formalizing provable anonymity in Isabelle/HOL.

We formalize in a theorem prover the notion of 1 provable anonymity. Our formalization relies oninductive definitions of message distinguishing ability and observational equivalence on traces observed by theintruder. Our theory differs from its original proposal and essentially boils down to