Inference-security analysis using resolution theorem-proving

A nonnumeric analog of statistical methods for proving security is described and implemented. The approach involves analyzing facts and inference rules assumed to be known to a compromiser and deriving all their possible consequences using resolution theorem-proving, a technique which is argued to be far more appropriate to this problem than rule-based expert systems or information-flow analysis. An important contribution of this method is augmentation of resolution to handle associated time intervals and probabilities of statements being true. The augmentation is simple to use by domain experts untrained in computers, and it is believed to provide the first truly practical tool for analysis of indirect logical inferences in information systems. Its capabilities are demonstrated with an example from military security