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.

30 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu