Constraining Credential Usage in Logic-Based Access Control

Authorization logics allow concise specification of flexible access-control policies, and are the basis for logic-based access-control systems. In such systems, resource owners issue credentials to specify policies, and the consequences of these policies are derived using logical inference rules. Proofs in authorization logics can serve as capabilities for gaining access to resources. Because a proof is derived from a set of credentials possibly issued by different parties, the issuer of a specific credential may not be aware of all the proofs that her credential may make possible. From this credential issuer's standpoint, the policy expressed in her credential may thus have unexpected consequences. To solve this general problem, we propose a system in which credentials can specify constraints on how they are to be used. We show how to modularly extend well-studied authorization logics to support the specification and enforcement of such constraints. A novelty of our design is that we allow the constraints to be arbitrary well-behaved functions over authorization proofs. Since all the information about an access is contained in the proofs, this makes it possible to express many interesting constraints. We study the formal properties of such a system, and give examples of constraints.