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 条
  • [1] Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies Using mCRL2
    Arshad, Hamed
    Horne, Ross
    Johansen, Christian
    Owe, Olaf
    Willemse, Tim A. C.
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2022, 2022, 13273 : 11 - 30
  • [2] Analysing AWN-Specifications Using mCRL2
    van Glabbeek, Rob
    Hofner, Peter
    van der Wal, Djurre
    [J]. INTEGRATED FORMAL METHODS, IFM 2018, 2018, 11023 : 398 - 418
  • [3] Towards model checking executable UML specifications in mCRL2
    Hansen, Helle Hvid
    Ketema, Jeroen
    Luttik, Bas
    Mousavi, MohammadReza
    van de Pol, Jaco
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) : 83 - 90
  • [4] Formal Verification of OIL Component Specifications using mCRL2
    Bunte, Olav
    van Gool, Louis C. M.
    Willemse, Tim A. C.
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2020, 2020, 12327 : 231 - 251
  • [5] Formal verification of OIL component specifications using mCRL2
    Olav Bunte
    Louis C. M. van Gool
    Tim A. C. Willemse
    [J]. International Journal on Software Tools for Technology Transfer, 2022, 24 : 441 - 472
  • [6] Formalising the Industrial Language SMMT in mCRL2
    van Laarhoven, Jordi E. P. M.
    Bunte, Olav
    van Gool, Louis C. M.
    Willemse, Tim A. C.
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2024, 2024, 14952 : 63 - 79
  • [7] Formal verification of OIL component specifications using mCRL2
    Bunte, Olav
    van Gool, Louis C. M.
    Willemse, Tim A. C.
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (03) : 441 - 472
  • [8] Sarir: A Rebeca to mCRL2 translator
    Hojjat, H.
    Siriani, M.
    Mousavi, M. R.
    Groote, J. F.
    [J]. SEVENTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2007, : 216 - +
  • [9] Experiences in developing the mCRL2 toolset
    Groote, J. F.
    Keiren, J. J. A.
    Stappers, F. P. M.
    Wesselink, J. W.
    Willemse, T. A. C.
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 2011, 41 (02): : 143 - 153
  • [10] Modelling and Analysing Software in mCRL2
    Groote, Jan Friso
    Keiren, Jeroen J. A.
    Luttik, Bas
    de Vink, Erik P.
    Willemse, Tim A. C.
    [J]. FORMAL ASPECTS OF COMPONENT SOFTWARE, FACS 2019, 2020, 12018 : 25 - 48
12345