Probabilistic Anonymity Via Coalgebraic Simulations

@incollection{citeulike:2373270, abstract = {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.}, author = {Hasuo, Ichiro and Kawabe, Yoshinobu }, citeulike-article-id = {2373270}, doi = {http://dx.doi.org/10.1007/978-3-540-71316-6\_26}, journal = {Programming Languages and Systems}, pages = {379--394}, posted-at = {2008-02-14 10:23:26}, priority = {2}, title = {Probabilistic Anonymity Via Coalgebraic Simulations}, url = {http://dx.doi.org/10.1007/978-3-540-71316-6\_26}, year = {2007} }

TY - CHAP ID - citeulike:2373270 L3 - citeulike-article-id:2373270 TI - Probabilistic Anonymity Via Coalgebraic Simulations JF - Programming Languages and Systems SP - 379 EP - 394 N2 - 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. AU - Hasuo, Ichiro AU - Kawabe, Yoshinobu PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-71316-6_26 ER -