A sound and complete model-generation procedure for consistent and confidentiality-preserving databases

This article introduces and investigates a new model-theoretic mechanism to enforce confidentiality (or privacy) requirements in a database instance; at the same time it ensures maximum availability of correct database answers. The aim is to materialize and publish a secure view that satisfies the properties of “inference-proofness” and “distortion minimality”. A comprehensive class of first-order constraints (representing a user’s a priori knowledge and a confidentiality policy) can be handled by the presented algorithm in a sound and complete way: tuple-generating dependencies, denial constraints and existential constraints. The due proof of refutation soundness makes use of Herbrand’s theorem and semantic trees.