Differential privacy in probabilistic systems

Ever since proposed by Dwork, differential privacy has been a hot topic in academia. However, few attempts have been made on reasoning about differential privacy at a system level. In this paper, we propose a formal framework to verify differential privacy in probabilistic systems. With a metric on the states of a system, we formalize differential privacy by the ratio of the probabilities in the distributions after the same labeled transitions of relevant states. We explain how traditional differential privacy can be embedded in our framework and raise an infimum metric, the least distance between two states, while not violating differential privacy. It is proven that the infimum metric is also a metric instance of differential privacy itself. Furthermore, we propose a two-level logic, a privacy variant of the familiar Hennessy-Milner logic, to characterize differential privacy in our framework. Our results have close relations to probabilistic bisimilarity as well.