Automated Certification of Authorisation Policy Resistance
Andreas Griesmayer, Charles Morisset

TL;DR
This paper introduces a formal method and tool for automatically verifying the resistance of attribute-based access control policies against attribute hiding attacks, enhancing security assurance in distributed systems.
Contribution
It presents ATRAP, a novel automated tool that combines Maude and Isabelle to verify policy resistance in ABAC, based on the PTaCL language.
Findings
ATRAP successfully finds resistance counter-examples.
ATRAP can automatically prove policy resistance.
Performance evaluation shows ATRAP's efficiency.
Abstract
Attribute-based Access Control (ABAC) extends traditional Access Control by considering an access request as a set of pairs attribute name-value, making it particularly useful in the context of open and distributed systems, where security relevant information can be collected from different sources. However, ABAC enables attribute hiding attacks, allowing an attacker to gain some access by withholding information. In this paper, we first introduce the notion of policy resistance to attribute hiding attacks. We then propose the tool ATRAP (Automatic Term Rewriting for Authorisation Policies), based on the recent formal ABAC language PTaCL, which first automatically searches for resistance counter-examples using Maude, and then automatically searches for an Isabelle proof of resistance. We illustrate our approach with two simple examples of policies and propose an evaluation of ATRAP…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAccess Control and Trust · Security and Verification in Computing · Cryptography and Data Security
