Proof Search in an Authorization Logic
Deepak Garg · 2009
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. This work was supported partially by the iCAST project sponsored by the National Science Council,