Verification of Workflow processes under multilevel security considerations

Traditional modelling and analysis of workflow aims at verifying the correctness of its control flow. When dealing with workflow security, the compliance of information flow with the adopted security policies needs also to be analyzed. In this paper, we propose a two-steps verification approach. While the first step is concerned by soundness of the workflow, the second one is concerned by the data consistency with respect to a multilevel security policy where the granting of access rights to objects by the workflow system is done according to information flow rules of Bell-LaPadula model. Our approach is based on the ECATNet formalism. It offers means to incorporate the security 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 security rules on the whole Workflow through the model checker of the MAUDE environment and how to relax them before producing the correct specification and submitting it to the workflow system.