Inference-security analysis using resolution theorem-proving

Abstract

Indirect logical inferences can provide a significant security threat to information processing systems, but they have not been much studied. Classification of data can reduce the threat, but classification decisions are typically left to the intuitive judgment of experts. Progress has been made on analyzing indirect statistical inferences that may compromise security of a database system ([3], chapter 6). We describe and implement a nonnumeric analog of these methods for proving security. Our approach involves analyzing facts and inference rules assumed to be known to a compromiser, deriving all their possible consequences using resolution theorem-proving, a technique which we argue is far more appropriate to this problem than rulebased expert systems or information flow analysis. An important contribution of our work is augmentation of resolution to handle associated time intervals and probabilities of statements being true. Our augmentation is simple to use by domain experts untrained in computers, and we believe it will provide the first truly practical tool for analysis of indirect logical inferences in information systems. We demonstrate capabilities with an example from military security.