Validating the RBAC ANSI 2012 standard using B

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

doi:10.1007/978-3-662-43652-3_22

Validating the RBAC ANSI 2012 standard using B

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › 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
Title of host publication	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings
Publisher	Springer Verlag
Pages	255-270
Number of pages	16
ISBN (Print)	9783662436516
DOIs	https://doi.org/10.1007/978-3-662-43652-3_22
Publication status	Published - 1 Jan 2014
Externally published	Yes
Event	4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014 - Toulouse, France Duration: 2 Jun 2014 → 6 Jun 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8477 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014
Country/Territory	France
City	Toulouse
Period	2/06/14 → 6/06/14

Keywords

B method
Role-Based Access Control
invariant preservation

Access to Document

10.1007/978-3-662-43652-3_22

Cite this

Huynh, N., Frappier, M., Mammar, A., Laleau, R., & Desharnais, J. (2014). Validating the RBAC ANSI 2012 standard using B. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings (pp. 255-270). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8477 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-43652-3_22

Huynh, Nghi ; Frappier, Marc ; Mammar, Amel et al. / Validating the RBAC ANSI 2012 standard using B. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings. Springer Verlag, 2014. pp. 255-270 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{c40bca835376478887f672dcb9f5fd06,

title = "Validating 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, Role-Based Access Control, invariant preservation",

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

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-662-43652-3\_22",

language = "English",

isbn = "9783662436516",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "255--270",

booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings",

note = "4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014 ; Conference date: 02-06-2014 Through 06-06-2014",

}

Huynh, N, Frappier, M, Mammar, A, Laleau, R & Desharnais, J 2014, Validating the RBAC ANSI 2012 standard using B. in Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8477 LNCS, Springer Verlag, pp. 255-270, 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014, Toulouse, France, 2/06/14. https://doi.org/10.1007/978-3-662-43652-3_22

Validating the RBAC ANSI 2012 standard using B. / Huynh, Nghi; Frappier, Marc; Mammar, Amel et al.
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings. Springer Verlag, 2014. p. 255-270 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8477 LNCS).

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

TY - GEN

T1 - Validating the RBAC ANSI 2012 standard using B

AU - Huynh, Nghi

AU - Frappier, Marc

AU - Mammar, Amel

AU - Laleau, Régine

AU - Desharnais, Jules

PY - 2014/1/1

Y1 - 2014/1/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 - Role-Based Access Control

KW - invariant preservation

U2 - 10.1007/978-3-662-43652-3_22

DO - 10.1007/978-3-662-43652-3_22

M3 - Conference contribution

AN - SCOPUS:84903642222

SN - 9783662436516

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 255

EP - 270

BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings

PB - Springer Verlag

T2 - 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014

Y2 - 2 June 2014 through 6 June 2014

ER -

Huynh N, Frappier M, Mammar A, Laleau R, Desharnais J. Validating the RBAC ANSI 2012 standard using B. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings. Springer Verlag. 2014. p. 255-270. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-43652-3_22

Validating the RBAC ANSI 2012 standard using B

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this