Access control via belnap logic: intuitive, expressive, and analyzable policy composition
File(s)
Published version
Author(s)
Bruns, Glenn
Huth, Michael
Type
Report
Abstract
Access control to IT systems increasingly relies on the ability to compose policies. There
is thus bene t in any framework for policy composition that is intuitive, formal (and so \an-
alyzable" and \implementable"), expressive, independent of speci c application domains, and
yet able to be extended to create domain-speci c instances. Here we develop such a framework
based on Belnap logic. An access-control policy is interpreted as a four-valued predicate that
maps access requests to either grant, deny, con
ict, or unspeci ed { the four values of the Bel-
nap bilattice. We de ne an expressive access-control policy language PBel, having composition
operators based on the operators of Belnap logic. Natural orderings on policies are obtained by
lifting the truth and information orderings of the Belnap bilattice. These orderings lead to a
query language in which policy analyses, e.g. con
ict freedom, can be speci ed. Policy analysis
is supported through a reduction of the validity of policy queries to the validity of propositional
formulas on predicates over access requests. We evaluate our approach through rewall policy
and RBAC policy examples, and discuss domain-speci c and generic extensions of our policy
language.
is thus bene t in any framework for policy composition that is intuitive, formal (and so \an-
alyzable" and \implementable"), expressive, independent of speci c application domains, and
yet able to be extended to create domain-speci c instances. Here we develop such a framework
based on Belnap logic. An access-control policy is interpreted as a four-valued predicate that
maps access requests to either grant, deny, con
ict, or unspeci ed { the four values of the Bel-
nap bilattice. We de ne an expressive access-control policy language PBel, having composition
operators based on the operators of Belnap logic. Natural orderings on policies are obtained by
lifting the truth and information orderings of the Belnap bilattice. These orderings lead to a
query language in which policy analyses, e.g. con
ict freedom, can be speci ed. Policy analysis
is supported through a reduction of the validity of policy queries to the validity of propositional
formulas on predicates over access requests. We evaluate our approach through rewall policy
and RBAC policy examples, and discuss domain-speci c and generic extensions of our policy
language.
Date Issued
2011-01-01
Citation
Departmental Technical Report: 11/6, 2011, pp.1-39
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
39
Journal / Book Title
Departmental Technical Report: 11/6
Copyright Statement
© 2011 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
11/6