Satisfiability and feasibility in a relationship-based workflow authorization model

Abstract

A workflow authorization model is defined in the framework of Relationship-Based Access Control (ReBAC), in which the protection state is a social network. Armed with this model, a new decision problem called workflow feasibility is studied. The goal is to ensure that the space of protection states contains at least one member in which the workflow specification can be executed to completion. A sufficient condition is identified under which feasibil­ity can be decided by a refutation procedure that is both sound and complete. A formal specification language, based on a monotonic fragment of the Propositional Dynamic Logic (PDL), is proposed for specifying protection state spaces. The adoption of this language renders workflow feasibility NP-complete in the general case but polynomial-time decidable for an important family of workflows. A model checker for this POL-based language is im­plemented. Hybridization of this PDL-fragment is examined. Satisfiability and feasibility of workflows with XOR-patterns are analyzed as well.