ASASP

Automated symbolic analysis of security policies

Francesco Alberti, Alessandro Armando, Silvio Ranise

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Citations (Scopus)

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-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.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages26-33
Number of pages8
Volume6803 LNAI
DOIs
Publication statusPublished - 2011
Event23rd International Conference on Automated Deduction, CADE 23 - Wroclaw, Poland
Duration: Jul 31 2011Aug 5 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6803 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other23rd International Conference on Automated Deduction, CADE 23
CountryPoland
CityWroclaw
Period7/31/118/5/11

Fingerprint

Symbolic Analysis
Security Policy
Reachability
Access control
Automated Theorem Proving
Theorem proving
Role-based Access Control
Fixpoint
Security Analysis
Satisfiability Problem
Control Policy
Access Control
Scalability
Modulo
Benchmark
Model

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Alberti, F., Armando, A., & Ranise, S. (2011). ASASP: Automated symbolic analysis of security policies. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6803 LNAI, pp. 26-33). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6803 LNAI). https://doi.org/10.1007/978-3-642-22438-6_4

ASASP : Automated symbolic analysis of security policies. / Alberti, Francesco; Armando, Alessandro; Ranise, Silvio.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6803 LNAI 2011. p. 26-33 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6803 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Alberti, F, Armando, A & Ranise, S 2011, ASASP: Automated symbolic analysis of security policies. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 6803 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6803 LNAI, pp. 26-33, 23rd International Conference on Automated Deduction, CADE 23, Wroclaw, Poland, 7/31/11. https://doi.org/10.1007/978-3-642-22438-6_4
Alberti F, Armando A, Ranise S. ASASP: Automated symbolic analysis of security policies. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6803 LNAI. 2011. p. 26-33. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-22438-6_4
Alberti, Francesco ; Armando, Alessandro ; Ranise, Silvio. / ASASP : Automated symbolic analysis of security policies. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6803 LNAI 2011. pp. 26-33 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5e88691110f94d9f9dd5bbeb4fde08a3,
title = "ASASP: Automated symbolic analysis of security policies",
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-Sh{\"o}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.",
author = "Francesco Alberti and Alessandro Armando and Silvio Ranise",
year = "2011",
doi = "10.1007/978-3-642-22438-6_4",
language = "English",
isbn = "9783642224379",
volume = "6803 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "26--33",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - ASASP

T2 - Automated symbolic analysis of security policies

AU - Alberti, Francesco

AU - Armando, Alessandro

AU - Ranise, Silvio

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=80051694398&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80051694398&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22438-6_4

DO - 10.1007/978-3-642-22438-6_4

M3 - Conference contribution

SN - 9783642224379

VL - 6803 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 26

EP - 33

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -