A correct-by-construction model for attribute-based access control: Illustration: web-based healthcare services

被引：4

作者：

Gadouche, Hania ^{[1
]}

Farah, Zoubeyr ^{[1
]}

Tari, Abdelkamel ^{[1
]}

机构：

[1] Univ Bejaia, Dept Comp Sci, Fac Exact Sci, Med Comp Lab LIMED, Bejaia, Algeria

来源：

CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS | 2020年 / 23卷 / 03期

关键词：

ABAC; Correct-by-construction; Event-B; Formal methods; Proof and refinement; Specification and validation; A priori verification; Web services; Healthcare systems;

D O I：

10.1007/s10586-019-02976-4

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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. The approach is illustrated in healthcare web services.

引用

页码：1517 / 1528

页数：12

共 27 条

[1] Rodin: An open toolset for modelling and reasoning in Event-B [J].

Abrial J.-R. ;

Butler M. ;

Hallerstede S. ;

Hoang T.S. ;

Mehta F. ;

Voisin L. .

International Journal on Software Tools for Technology Transfer, 2010, 12 (06) :447-466

[2]

Abrial J.-R., 2010, MODELING EVENT B SYS, V1st

[3] Formal Modelling of Data Integration Systems Security Policies [J].

Akeel, Fatimah ;

Salehi Fathabadi, Asieh ;

Paci, Federica ;

Gravell, Andrew ;

Wills, Gary .

DATA SCIENCE AND ENGINEERING, 2016, 1 (03) :139-148

[4]

Anderson, 2003, extensible access control markup language (XACML) version 1.0

[5]

[Anonymous], 2004, Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, DOI [10.1145/1029133.1029140, DOI 10.1145/1029133.1029140]

[6] Incremental Construction of Realizable Choreographies [J].

Benyagoub, Sarah ;

Ouederni, Meriem ;

Ait-Ameur, Yamine ;

Mashkoor, Atif .

NASA FORMAL METHODS, NFM 2018, 2018, 10811 :1-19

[7] A correct-by-construction model for asynchronously communicating systems [J].

Farah, Zoubeyr ;

Ait-Ameur, Yamine ;

Ouederni, Meriem ;

Tari, Kamel .

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2017, 19 (04) :465-485

[8]

Heljanko K, 2006, LECT NOTES COMPUT SC, V4144, P95, DOI 10.1007/11817963_12

[9]

Hoang TS, 2009, SPECIFYING ACCESS CO, DOI [10.3929/ethz-a-006733720, DOI 10.3929/ETHZ-A-006733720]

[10]

Hu V.C., 2014, NIST Special Publication 800-30, V800, P1, DOI 10.6028/nist.sp.800-162

← 1 2 3 →