ASASP: Automated Symbolic Analysis of Security Policies

We describe asasp, a symbolic reachability procedure for the analysis of administrative access control policies. The tool represents access policies and their administrative actions as formulae of the BernaysSh¨onfinkel-Ramsey class and then uses a symbolic reachability procedure to solve security analysis problems. Checks for fix-point—reduced to satisfiability problems—are mechanized by Satisfiability Modulo Theories solving and Automated Theorem Proving. asasp has been successfully applied to the analysis of benchmark problems arising in (extensions of) the Role-Based Access Control model. Our tool shows better scalability than a state-of-the-art tool on a significant set of instances of these problems.

• Type: Journal
• Year: 2011
• Where: CADE
• Authors: Francesco Alberti, Alessandro Armando, Silvio Ranise
• Keywords: Benchmark Problems, CADE 2011, Control Policies, Logical Reasoning, Role Based Access Control