Computer Science Department
School of Computer Science, Carnegie Mellon University
Proof Search in an Authorization Logic
We consider the problem of proof search in an expressive authorization logic that contains a "says" modality and an ordering on principals. After a description of the proof system for the logic, we identify two fragments that admit complete goal-directed and saturating proof search strategies. A smaller fragment is then presented, which supports both goal-directed and saturating search, and has a sound and complete translation to first-order logic. We conclude with a brief description of our implementation of goal-directed search.