Deciding Differential Privacy of Online Algorithms with Multiple Variables

We consider the problem of checking the differential privacy of online randomized algorithms that process a stream of inputs and produce outputs corresponding to each input. This paper generalizes an automaton model called DiP automata [10] to describe such algorithms by allowing multiple real-valued storage variables. A DiP automaton is a parametric automaton whose behavior depends on the privacy budget 𝜖. An automaton A will be said to be differentially private if, for some 𝔇, the automaton is 𝔇𝜖-differentially private for all values of 𝜖 > 0. We identify a precise characterization of the class of all differentially private DiP automata. We show that the problem of determining if a given DiP automaton belongs to this class is PSPACE-complete. Our PSPACE algorithm also computes a value for 𝔇 when the given automaton is differentially private. The algorithm has been implemented, and experiments demonstrating its effectiveness are presented. CCS CONCEPTS • Security and privacy → Logic and verification; Formal security models.