Design and Verification of Time-Constrained Workflows With Multi-Level Security

When dealing with workflow security requirements, the compliance of information flow with the adopted security policies needs to be analyzed. For this purpose, we adopt in this paper a two-step verification approach. While the first step is concerned by the verification of the soundness of the workflow, the second one is concerned by the control of access rights on information under both time constraints and security requirements (through multilevel security policies such as Bell-LaPadula). We propose a model for such workflow specification based on the Time ECATNet formalism. This latter offers means to incorporate the security and time constraints on information flow into an initial WF-net modeling the control flow of a workflow specification. We then show how to analyze the impact of the introduced security rules on the workflow execution, using the Maude LTL model checker, and show how to relax them to derive a correct workflow specification.