A Correct-by-Construction Model for Attribute-Based Access Control

被引：0
作者：
Gadouche, Hania [1 ]
Farah, Zoubeyr [1 ]
Tari, Abdelkamel [1 ]
机构：
[1] Univ Bejaia, Fac Exact Sci, LIMED Lab, Bejaia, Algeria
来源：
MODEL AND DATA ENGINEERING, MEDI 2018 | 2018年 / 11163卷
关键词：
ABAC; A priori verification; Correct-by-Construction; Event-B; Formal methods; Proof and refinement; Specification and validation;
D O I：
10.1007/978-3-030-00856-7_15
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper, a formal specification approach of the Attribute-Based Access Control (ABAC) is proposed using the Event-B method. We apply an a-priori formal verification to build a correct model in a stepwise manner. Correctness of the specification model is insured during the construction steps. The model is composed of abstraction levels that are generated through refinement operations. A set of ABAC properties is defined in each level of refinement starting from the highest abstract level to the most concrete one. These properties are preserved by proofs with the behavior specification.
引用
收藏
页码：233 / 247
页数：15
相关论文
共 26 条
  • [1] Rodin: An open toolset for modelling and reasoning in Event-B
    Abrial J.-R.
    Butler M.
    Hallerstede S.
    Hoang T.S.
    Mehta F.
    Voisin L.
    [J]. International Journal on Software Tools for Technology Transfer, 2010, 12 (06) : 447 - 466
  • [2] Anderson A., 2003, EXTENSIBLE ACCESS CO
  • [3] [Anonymous], 2010, Modeling in Event-B: system and software engineering
  • [4] Incremental Construction of Realizable Choreographies
    Benyagoub, Sarah
    Ouederni, Meriem
    Ait-Ameur, Yamine
    Mashkoor, Atif
    [J]. NASA FORMAL METHODS, NFM 2018, 2018, 10811 : 1 - 19
  • [5] Chong S., 2016, TECHNICAL REPORT
  • [6] A correct-by-construction model for asynchronously communicating systems
    Farah, Zoubeyr
    Ait-Ameur, Yamine
    Ouederni, Meriem
    Tari, Kamel
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2017, 19 (04) : 465 - 485
  • [7] Heljanko K, 2006, LECT NOTES COMPUT SC, V4144, P95, DOI 10.1007/11817963_12
  • [8] Hoang T. S., 2009, SPECIFYING ACCESS CO
  • [9] Hu C. T, 2014, TECHNICAL REPORT
  • [10] Attribute-Based Access Control
    Hu, Vincent C.
    Kuhn, D. Richard
    Ferraiolo, David F.
    [J]. COMPUTER, 2015, 48 (02) : 85 - 88
123