Model Checking of Security-Sensitive Business Processes
Security-sensitive business processes are business processes that must comply with security requirements (e.g. authorization constraints). In this paper, it has been shown that model checking can be profitably used for the automatic analysis of security-sensitive business processes. But building a formal model that simultaneously accounts for both the work flow and the access control policy is a time consuming and error-prone activity. In this paper, the authors present a new approach to model checking security-sensitive business processes that allows for the separate specification of the work flow and of the associated security policy while retaining the ability to carry out a fully automatic analysis of the process.