Proof Search in an Authorization Logic
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 14, 2009
- Accession Number
- ADA507017
Entities
People
- Deepak Garg
Organizations
- Carnegie Mellon University