Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis

File Description SizeFormat 
access-policies-analysis-belnap.pdfPublished version523.63 kBAdobe PDFDownload
Title: Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis
Author(s): Bruns, G
Huth, M
Item Type: Conference Paper
Abstract: It is difficult to develop and manage large, multi-author access control policies without a means to compose larger policies from smaller ones. Ideally, an access-control policy language will have a small set of simple policy combinators that allow for all desired policy compositions. In [5], a policy language was presented having policy combinators based on Belnap logic, a four-valued logic in which truth values correspond to policy results of grant , deny , conflict , and undefined . We show here how policies in this language can be analyzed, and study the expressiveness of the language. To support policy analysis, we define a query language in which policy analysis questions can be phrased. Queries can be translated into a fragment of first-order logic for which satisfiability and validity checks are computable by SAT solvers or BDDs. We show how policy analysis can then be carried out through model checking, validity checking, and assume-guarantee reasoning over such translated queries. We also present static analysis methods for the particular questions of whether policies contain gaps or conflicts. Finally, we establish expressiveness results showing that all data independent policies can be expressed in our policy language. © 2008 IEEE.
Publication Date: 19-Sep-2008
URI: http://hdl.handle.net/10044/1/5659
Publisher Link: http://doi.ieeecomputersociety.org/10.1109/CSF.2008.10
ISBN: 978-0-7695-3182-3
Publisher: IEEE Computer Society Press
Presented At: 21st IEEE Computer Security Foundations Symposium
Start Page: 163
End Page: 176
Copyright Statement: © 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
Conference Location: Pittsburgh, USA
Appears in Collections:Quantitative Analysis and Decision Science



Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons