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

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

doi:10.1109/ARES.2015.95

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

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

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Proceedings of 2015 10th International Conference on Availability, Reliability and Security (ARES)
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	532
Number of pages	539
ISBN (Electronic)	978-1-4673-6590-1
ISBN (Print)	978-1-4673-6589-5
DOIs	https://doi.org/10.1109/ARES.2015.95
Publication status	Published - 2015

Keywords

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

Access to Document

10.1109/ARES.2015.95

Cite this

@inproceedings{2f4f670bb70b461997f19a7d5375f475,

title = "Incremental development of RBAC-Controlled E-Marking System using the B Method",

abstract = "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.",

keywords = "incremental development, E-Marking Systems, role based access control, B Method",

author = "Nasser Al-Hadhrami and Benjamin Aziz and Shantanu Sardesai and {ben Othmane}, Lotfi",

year = "2015",

doi = "10.1109/ARES.2015.95",

language = "English",

isbn = "978-1-4673-6589-5",

pages = "532",

booktitle = "Proceedings of 2015 10th International Conference on Availability, Reliability and Security (ARES)",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

address = "United States",

}

Incremental development of RBAC-Controlled E-Marking System using the B Method. / Al-Hadhrami, Nasser; Aziz, Benjamin; Sardesai, Shantanu et al.
Proceedings of 2015 10th International Conference on Availability, Reliability and Security (ARES). Institute of Electrical and Electronics Engineers Inc., 2015. p. 532.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Al-Hadhrami, Nasser

AU - Aziz, Benjamin

AU - Sardesai, Shantanu

AU - ben Othmane, Lotfi

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - incremental development

KW - E-Marking Systems

KW - role based access control

KW - B Method

U2 - 10.1109/ARES.2015.95

DO - 10.1109/ARES.2015.95

M3 - Conference contribution

SN - 978-1-4673-6589-5

SP - 532

BT - Proceedings of 2015 10th International Conference on Availability, Reliability and Security (ARES)

PB - Institute of Electrical and Electronics Engineers Inc.

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Cite this