LAUSR

Separations of Duties (SoDs) are an important class of security requirements in business process management. Their violation may result in system misuse and fraud, leading to economic losses or legal implications. Hence, it is of paramount importance to ensure that a business process meets all SoDs. Existing works usually adopt model checking to verify SoDs. However, building formal models that simultaneously account for both workflow and SoDs is a time-consuming and error-prone activity. In this article, we propose a new approach to specifying and enforcing SoDs in business processes using Petri nets (PNs). First, we derive a necessary and sufficient condition for the SoD violations from the viewpoint of structure and marking of PNs. We show that the SoD constraints can be enforced by disallowing the process to reach certain markings, with the constraints being written as linear inequalities. Then, we design supervisors to enforce SoDs in an off-line and a real-time manner, respectively, based on the linear inequalities. Meanwhile, inequality analysis is provided for the structural simplicity of supervisors. Finally, the complexity analysis of our approach and the comparison with the work in the literature are given to illustrate the effectiveness and efficiency of ours.