XACML2mCRL2: Automatic transformation of XACML policies into mCRL2 specifications

被引：0
|
作者：
Arshad, Hamed [1 ]
Horne, Ross [2 ]
Johansen, Christian [3 ]
Owe, Olaf [1 ]
Willemse, Tim A. C. [4 ]
机构：
[1] Univ Oslo, Oslo, Norway
[2] Univ Strathclyde, Comp & Informat Sci, Glasgow, Scotland
[3] Norwegian Univ Sci & Technol, Gjovik, Norway
[4] Eindhoven Univ Technol, Eindhoven, Netherlands
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2024年 / 232卷
关键词：
XACML; mCRL2; Formal verification; Access control;
D O I：
10.1016/j.scico.2023.103046
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The eXtensible Access Control Markup Language (XACML) is a popular OASIS standard for the specification of fine-grained access control policies. However, the standard does not provide a proper solution for the verification of XACML access control policies before their deployment. The first step for the formal verification of XACML policies is to formally specify such policies. Hence, this paper presents XACML2mCRL2, a tool for the automatic translation of XACML access control policies into mCRL2. The mCRL2 specifications generated by our tool can be used for formal verification of important properties of access control policies, such as completeness or inconsistency, using the well-known mCRL2 toolset.
引用
收藏
页数：10
相关论文
共 50 条
  • [21] Modelling and Analysing a Mechanical Lung Ventilator in mCRL2
    van Dortmont, Danny
    Keiren, Jeroen J. A.
    Willemse, Tim A. C.
    [J]. RIGOROUS STATE-BASED METHODS, ABZ 2024, 2024, 14759 : 341 - 359
  • [22] Modelling the Raft Distributed Consensus Protocol in mCRL2
    Bora, Parth
    Minh, Pham Duc
    Willemse, Tim A. C.
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2024, (399): : 7 - 20
  • [23] Family-Based Model Checking with mCRL2
    ter Beek, Maurice H.
    de Vink, Erik P.
    Willemse, Tim A. C.
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2017, 2017, 10202 : 387 - 405
  • [24] Towards Modular Verification of Software Product Lines with mCRL2
    ter Beek, Maurice H.
    de Vink, Erik P.
    [J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: TECHNOLOGIES FOR MASTERING CHANGE, PT I, 2014, 8802 : 368 - 385
  • [25] Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 Toolset
    Bartholomeus, Maarten
    Luttik, Bas
    Willemse, Tim
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2018, 2018, 11119 : 98 - 114
  • [26] Model Checking Business Processes for Web Service Compositions in mCRL2
    Sun, Meng
    Li, Shaodong
    Ou, Yufei
    [J]. 2014 SIXTH INTERNATIONAL CONFERENCE ON INTELLIGENT HUMAN-MACHINE SYSTEMS AND CYBERNETICS (IHMSC), VOL 2, 2014, : 202 - 205
  • [27] The mCRL2 Toolset for Analysing Concurrent Systems Improvements in Expressivity and Usability
    Bunte, Olav
    Groote, Jan Friso
    Keiren, Jeroen J. A.
    Laveaux, Maurice
    Neele, Thomas
    de Vink, Erik P.
    Wesselink, Wieger
    Wijs, Anton
    Willemse, Tim A. C.
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, 2019, 11428 : 21 - 39
  • [28] Suitability of mCRL2 for Concurrent-System Design: A 2 x 2 Switch Case Study
    Stappers, Frank P. M.
    Reniers, Michel A.
    Groote, Jan Friso
    [J]. FORMAL METHODS FOR COMPONENTS AND OBJECTS, 2010, 6286 : 166 - 185
  • [29] Family-Based Model Checking of SPL based on mCRL2
    Ben Snaiba, Ziad
    de Vink, Erik P.
    Willemse, Tim A. C.
    [J]. 21ST INTERNATIONAL SYSTEM & SOFTWARE PRODUCT LINE CONFERENCE (SPLC 2017), VOL 2, 2017, : 13 - 16
  • [30] Formally modeling and verifying a software component retrieval system using mCRL2
    Pal, Nisha
    Yadav, Dharmendra Kumar
    [J]. INTERNATIONAL JOURNAL OF SYSTEM ASSURANCE ENGINEERING AND MANAGEMENT, 2023, 14 (06) : 2485 - 2496
12345