Role updating in information systems using model checking

The role-based access control (RBAC) has significantly simplified the management of users and permissions in information systems. In dynamic environments, systems are constantly undergoing changes, and accordingly, the associated configurations need to be updated in order to reflect the systems' security evolutions. However, such updating process is generally complicated as the resulting system state is expected to meet necessary constraints. This paper presents an approach for assisting administrators to make a desirable update, in light of changes in RBAC systems. We propose a formalization of the update approach, investigate its properties, and develop an updating algorithm based on model checking techniques. Our experimental results demonstrate the effectiveness of the proposed approach.