A formal validation of the RBAC ANSI 2012 standard using B

Nghi Huynh; Marc Frappier; Amel Mammar; Régine Laleau; Jules Desharnais

doi:10.1016/j.scico.2016.04.011

A formal validation of the RBAC ANSI 2012 standard using B

Nghi Huynh, Marc Frappier, Amel Mammar, Régine Laleau, Jules Desharnais

Research output: Contribution to journal › Article › peer-review

Abstract

We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.

Original language	English
Pages (from-to)	76-93
Number of pages	18
Journal	Science of Computer Programming
Volume	131
DOIs	https://doi.org/10.1016/j.scico.2016.04.011
Publication status	Published - 1 Dec 2016
Externally published	Yes

Keywords

B method
Invariant preservation
Role-Based Access Control

Access to Document

10.1016/j.scico.2016.04.011

Cite this

@article{2a9aa78574734f6fb48aef2f105e677a,

title = "A formal validation of the RBAC ANSI 2012 standard using B",

abstract = "We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.",

keywords = "B method, Invariant preservation, Role-Based Access Control",

author = "Nghi Huynh and Marc Frappier and Amel Mammar and R{\'e}gine Laleau and Jules Desharnais",

note = "Publisher Copyright: {\textcopyright} 2016 Elsevier B.V.",

year = "2016",

month = dec,

day = "1",

doi = "10.1016/j.scico.2016.04.011",

language = "English",

volume = "131",

pages = "76--93",

journal = "Science of Computer Programming",

issn = "0167-6423",

}

TY - JOUR

T1 - A formal validation of the RBAC ANSI 2012 standard using B

AU - Huynh, Nghi

AU - Frappier, Marc

AU - Mammar, Amel

AU - Laleau, Régine

AU - Desharnais, Jules

PY - 2016/12/1

Y1 - 2016/12/1

N2 - We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.

AB - We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards.

KW - B method

KW - Invariant preservation

KW - Role-Based Access Control

U2 - 10.1016/j.scico.2016.04.011

DO - 10.1016/j.scico.2016.04.011

M3 - Article

AN - SCOPUS:84967328450

SN - 0167-6423

VL - 131

SP - 76

EP - 93

JO - Science of Computer Programming

JF - Science of Computer Programming

ER -

A formal validation of the RBAC ANSI 2012 standard using B

Abstract

Keywords

Access to Document

Fingerprint

Cite this