XACML2mCRL2: automatic transformation of XACML policies into mCRL2 specifications

Hamed Arshad; Ross Horne; Christian Johansen; Olaf Owe; Tim A.C. Willemse

doi:10.1016/j.scico.2023.103046

XACML2mCRL2: automatic transformation of XACML policies into mCRL2 specifications

Hamed Arshad, Ross Horne, Christian Johansen, Olaf Owe, Tim A.C. Willemse

Research output: Contribution to journal › Article › peer-review

34 Downloads (Pure)

Abstract

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.

Original language	English
Article number	103046
Number of pages	10
Journal	Science of Computer Programming
Volume	232
Early online date	31 Oct 2023
DOIs	https://doi.org/10.1016/j.scico.2023.103046 https://doi.org/10.1016/j.scico.2023.103046
Publication status	Published - 31 Jan 2024

Keywords

XACML
mCRL2
formal verification
access control

Access to Document

Arshad-etal-SCP-2023-XACML2mCRL2-automatic-transformation-of-XACML-policies-into-mCRL2-specificationsFinal published version, 1.81 MBLicence: CC BY-NC-ND 4.0

Cite this

@article{f20d63747a354eb4b30ae0cb74ad2d20,

title = "XACML2mCRL2: automatic transformation of XACML policies into mCRL2 specifications",

abstract = "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.",

keywords = "XACML, mCRL2, formal verification, access control",

author = "Hamed Arshad and Ross Horne and Christian Johansen and Olaf Owe and Willemse, {Tim A.C.}",

year = "2024",

month = jan,

day = "31",

doi = "10.1016/j.scico.2023.103046",

language = "English",

volume = "232",

journal = "Science of Computer Programming",

issn = "0167-6423",

}

TY - JOUR

T1 - XACML2mCRL2

T2 - automatic transformation of XACML policies into mCRL2 specifications

AU - Arshad, Hamed

AU - Horne, Ross

AU - Johansen, Christian

AU - Owe, Olaf

AU - Willemse, Tim A.C.

PY - 2024/1/31

Y1 - 2024/1/31

N2 - 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.

AB - 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.

KW - XACML

KW - mCRL2

KW - formal verification

KW - access control

U2 - 10.1016/j.scico.2023.103046

DO - 10.1016/j.scico.2023.103046

M3 - Article

SN - 0167-6423

VL - 232

JO - Science of Computer Programming

JF - Science of Computer Programming

M1 - 103046

ER -

XACML2mCRL2: automatic transformation of XACML policies into mCRL2 specifications

Abstract

Keywords

Access to Document

Fingerprint

Cite this