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 Bernays-Shonfinkel-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.
ASASP: Automated Symbolic Analysis of Security Policies / Alberti, F; Armando, A; Ranise, S. - 6803:(2011), pp. 26-+. (Intervento presentato al convegno 23rd International Conference on Automated Deduction tenutosi a Polonia nel 21/07-05/08/2011).
ASASP: Automated Symbolic Analysis of Security Policies
Ranise, S
2011-01-01
Abstract
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 Bernays-Shonfinkel-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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
