On the Satisfiability of Constraints in Workflow Systems

The specification and enforcement of authorization policies such as separation of duty and binding of duty in workflow systems is an important area of current research in computer security. We introduce a formal model for constrained workflow systems that incorporate constraints for implementing such policies. We define an entailment constraint, which is defined on a pair of tasks in a workflow, and show that such constraints can be used to model many familiar authorization policies. We show that a set of entailment constraints can be manipulated algebraically in order to compute all possible dependencies between tasks in the workflow. The resulting set of constraints form the basis for an analysis of the satisfiability of a workflow. We briefly consider how this analysis can be used to implement a reference monitor for workflow systems