Institute of Electrical and Electronics Engineers
Role Based Access Control (RBAC) is an increasingly popular and efficient security solution. An approach for combined modeling of Role-Based Access Control systems (RBAC) together with business workflows is presented. The model allows to model check various security properties. Several techniques to confine the state explosion, which may occur during model checking are presented and experimentally evaluated using the model checker Spin. The techniques allow the verification of the business workflow and associated RBAC for a reasonable number of users of a medium sized company.