TY - GEN
T1 - Process Algebra Can Save Lives
T2 - 42nd IFIPWG6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022
AU - Arshad, Hamed
AU - Horne, Ross
AU - Johansen, Christian
AU - Owe, Olaf
AU - Willemse, Tim A.C.
PY - 2022/6/12
Y1 - 2022/6/12
N2 - This paper proposes an approach to formally verify XACML policies using the process algebra mCRL2. XACML (eXtensible Access Control Markup Language) is an OASIS standard for access control systems that is much used in health care due to its fine-grained, attribute-based policy definitions, useful in dynamic environments such as emergency wards. A notorious problem in XACML is the detection of conflicts, which arise especially when combining policies, such as when health institutions merge. Our formal translation of XACML policies into mCRL2, using our automated tool XACML2mCRL2, enables us to verify the above property, called consistency, as well as other policy properties such as completeness and obligation enforcement. Verifying policy properties statically allows us to resolve inconsistencies in advance, thus avoiding situations where an access request is denied in a critical situation (e.g., in an ambulance, when lives may be put in danger) just because of incomplete or inconsistent policies. The mCRL2 toolset is especially useful for modeling behaviors of interactive systems, where XACML would be only one part. Therefore, we verify an access control system together with the intended health care system that it is supposed to protect. For this, we exemplify how to verify safety and liveness properties of an assisted living and community care system.
AB - This paper proposes an approach to formally verify XACML policies using the process algebra mCRL2. XACML (eXtensible Access Control Markup Language) is an OASIS standard for access control systems that is much used in health care due to its fine-grained, attribute-based policy definitions, useful in dynamic environments such as emergency wards. A notorious problem in XACML is the detection of conflicts, which arise especially when combining policies, such as when health institutions merge. Our formal translation of XACML policies into mCRL2, using our automated tool XACML2mCRL2, enables us to verify the above property, called consistency, as well as other policy properties such as completeness and obligation enforcement. Verifying policy properties statically allows us to resolve inconsistencies in advance, thus avoiding situations where an access request is denied in a critical situation (e.g., in an ambulance, when lives may be put in danger) just because of incomplete or inconsistent policies. The mCRL2 toolset is especially useful for modeling behaviors of interactive systems, where XACML would be only one part. Therefore, we verify an access control system together with the intended health care system that it is supposed to protect. For this, we exemplify how to verify safety and liveness properties of an assisted living and community care system.
KW - Access control
KW - mCRL2
KW - Process algebra
KW - XACML
UR - https://www.scopus.com/pages/publications/85133025805
U2 - 10.1007/978-3-031-08679-3_2
DO - 10.1007/978-3-031-08679-3_2
M3 - Conference contribution
AN - SCOPUS:85133025805
SN - 978-3-031-08678-6
T3 - Lecture Notes in Computer Science (LNCS)
SP - 11
EP - 30
BT - Formal Techniques for Distributed Objects, Components, and Systems
A2 - Mousavi, Mohammad Reza
A2 - Philippou, Anna
PB - Springer
CY - Cham
Y2 - 13 June 2022 through 17 June 2022
ER -