A Novel Analysis of Utility in Privacy Pipelines, Using Kronecker Products and Quantitative Information Flow

We combine Kronecker products, and quantitative information flow, to give a novel formal analysis for the fine-grained verification of utility in complex privacy pipelines. The combination explains a surprising anomaly in the behaviour of utility of privacy-preserving pipelines -that sometimes a reduction in privacy results also in a decrease in utility. We use the standard measure of utility for Bayesian analysis, introduced by Ghosh at al. [1] , to produce tractable and rigorous proofs of the fine-grained statistical behaviour leading to the anomaly. More generally, we offer the prospect of formalanalysis tools for utility that complement extant formal analyses of privacy. We demonstrate our results on a number of common privacy-preserving designs. CCS CONCEPTS • Formal Methods; • Security and Privacy;