Probabilistic Anonymity Via Coalgebraic Simulations

9 years 8 months ago
Probabilistic Anonymity Via Coalgebraic Simulations
There is a growing concern on anonymity and privacy on the Internet, resulting in lots of work on formalization and verification of anonymity. Especially, importance of probabilistic aspect of anonymity is claimed recently by many authors. Among them are Bhargava and Palamidessi who present the definition of probabilistic anonymity for which, however, proof methods are not yet elaborated. In this paper we introduce a simulation-based proof method for probabilistic anonymity. It is a probabilistic adaptation of the method by Kawabe et al. for non-deterministic anonymity: anonymity of a protocol is proved by finding out a forward/backward simulation between certain automata. For the jump from non-determinism to probability we fully exploit a generic, coalgebraic theory of traces and simulations developed by Hasuo and others. In particular, an appropriate notion of probabilistic simulations is obtained by instantiating a generic definition with suitable parameters.
Ichiro Hasuo, Yoshinobu Kawabe
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ESOP
Authors Ichiro Hasuo, Yoshinobu Kawabe
Comments (0)