Title :
Formal Verification of Business Workflows and Role Based Access Control Systems
Author :
Dury, Arnaud ; Boroday, Sergiy ; Petrenko, Alexandre ; Lotz, Volkmar
Author_Institution :
Comput. Res. Inst. of Montreal, Paris
Abstract :
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.
Keywords :
authorisation; formal verification; workflow management software; business workflows; formal verification; medium sized company; model checker Spin; role based access control system; security property; Access control; Automata; Automatic control; Companies; Computer security; Context modeling; Explosions; Formal verification; Information security; Web services;
Conference_Titel :
Emerging Security Information, Systems, and Technologies, 2007. SecureWare 2007. The International Conference on
Conference_Location :
Valencia
Print_ISBN :
978-0-7695-2989-9
DOI :
10.1109/SECUREWARE.2007.4385334
