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 Bernays-Shönfinkel-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.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: SMT-based verification of data-aware processes: a model-theoretic approach (2020)
- Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: From model completeness to verification of data aware processes (2019)
- Ranise, Silvio: Symbolic backward reachability with effectively propositional logic. Application to security policy analysis (2013)
- Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei: EPR-based bounded model checking at word level (2012)
- Alberti, Francesco; Armando, Alessandro; Ranise, Silvio: ASASP: automated symbolic analysis of security policies (2011) ioport
Further publications can be found at: http://st.fbk.eu/en/node/153