An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints

Business processes under authorization control are sets of coordinated activities subject to a security policy stating which agent can access which resource. Their behavior is difficult to predict due to the complex and unexpected interleaving of different execution flows within the process. Serious flaws may thus go undetected and manifest themselves only after deployment. For this reason, business processes are being considered a new, promising application domain for formal methods and model checking techniques in particular. In this paper we show that action-based languages provide a rich and natural framework for the formal specification of and automated reasoning about business processes under authorization constraints. We do this by discussing the application of the action language C to the specification of a business process from the banking domain that is representative of an important class of business processes of practical relevance. Furthermore we show that a number of reasoning tasks that arise in this context (namely checking whether the control flow together with the security policy meets the expected security properties, building a security policy for the given business process under given security requirements, and finding an allocation of tasks to agents that guarantees the completion of the business process) can be carried out automatically using the Causal Calculator CCALC. We also compare C with the prominent specification language used in model-checking.(1) (C) 2011 Elsevier Inc. All rights reserved.