An Incremental B-Model for RBAC-Controlled Electronic Marking System

The incremental development of software through the addition of new features and the insertion of new access rules potentially renders the access control models inconsistent and creates security flaws. This paper proposes modeling Role Based Access Control (RBAC) models of these software using the B language and re-evaluating the consistency of the models following model changes. It shows the mechanism of formalizing RBAC policies of an Electronic Marking System (EMS) using B specifications and illustrates the verification of the consistency of the RBAC specification, using model checking and proof obligations. In addition, it shows how to address inconsistencies that result from incremental specification of system' architectures.