XACML2mCRL2: Automatic transformation of XACML policies into mCRL2 specifications.

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. • XACML2mCRL2 automatically converts XACML policies into mCRL2 specifications that can be analyzed using the mCRL2 toolset. • XACML2mCRL2 requires no installation and can be executed on various operating systems such as Windows, Linux, macOS, etc. • XACML2mCRL2 is easy to use, and users do not need to know formal methods or understand the generated mCRL2 specifications. • XACML2mCRL2 makes the mCRL2 toolset a proper fully automated tool for formal verification of XACML access control policies. • XACML2mCRL2 transforms obligations attached to rules and policies, as well as other elements of the XACML policy model. [ABSTRACT FROM AUTHOR]