Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Incremental development of RBAC-controlled E-marking system using the B method

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


Institute of Electrical and Electronics Engineers -IEEE-; IEEE Computer Society:
10th International Conference on Availability, Reliability and Security, ARES 2015. Proceedings : 24-28 August 2015, Toulouse, France
Los Alamitos, Calif.: IEEE Computer Society Conference Publishing Services (CPS), 2015
ISBN: 978-1-4673-6590-1
ISBN: 978-1-4673-6591-8
ISBN: 978-1-4673-6589-5
International Conference on Availability, Reliability and Security (ARES) <10, 2015, Toulouse>
International Workshop on Agile Secure Software Development (ASSD) <1, 2015, Toulouse>
Fraunhofer SIT ()
Role Based Access Control (RBAC); formal specification; RBAC constraints; separation of duties; role hierarchy; cardinality constraints; model checking; proof obligations

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.