Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis
Open Access
- 1 January 2008
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 163-176
- https://doi.org/10.1109/csf.2008.10
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 \cite{BH07}, 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 {\em data independent} policies can be expressed in our policy language.Keywords
This publication has 15 references indexed in Scilit:
- Defeasible security policy composition for web servicesPublished by Association for Computing Machinery (ACM) ,2006
- Verification and change-impact analysis of access-control policiesPublished by Association for Computing Machinery (ACM) ,2005
- A model-based approach to integrating security policies for embedded devicesPublished by Association for Computing Machinery (ACM) ,2004
- Using first-order logic to reason about policiesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- Proving security protocols with model checkers by data independence techniquesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- An algebra for composing access control policiesACM Transactions on Information and System Security, 2002
- Authorization in Distributed Systems: A New Approach1Journal of Computer Security, 1993
- Multivalued logics: a uniform approach to reasoning in artificial intelligenceComputational Intelligence, 1988
- A logic for default reasoningArtificial Intelligence, 1980
- A Useful Four-Valued LogicPublished by Springer Science and Business Media LLC ,1977