Incremental development of RBAC-Controlled E-Marking System using the B Method

Nasser Al-Hadhrami, Benjamin Aziz, Shantanu Sardesai, Lotfi ben Othmane

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Role Based Access Control (RBAC) models are access policies that associate access rights to roles of subjects on objects. The incremental development of software by adding new features and the insertion of new access rules potentially render the model inconsistent and create security flaws. This paper proposes modeling RBAC models using the B language such that it is possible to reevaluate 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.
Original languageEnglish
Title of host publicationProceedings of 2015 10th International Conference on Availability, Reliability and Security (ARES)
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages539
ISBN (Electronic)978-1-4673-6590-1
ISBN (Print)978-1-4673-6589-5
Publication statusPublished - 2015


  • incremental development
  • E-Marking Systems
  • role based access control
  • B Method


Dive into the research topics of 'Incremental development of RBAC-Controlled E-Marking System using the B Method'. Together they form a unique fingerprint.

Cite this