The study of canonically complete attribute-based access control (ABAC) languages is relatively new. A canonically complete language is useful as it is functionally complete and provides a "normal form" for policies. However, previous work on canonically complete ABAC languages requires that the set of authorization decisions is totally ordered, which does not accurately reflect the intuition behind the use of the allow, deny and not-applicable decisions in access control. A number of recent ABAC languages use a fourth value and the set of authorization decisions is partially ordered. In this paper, we show how canonical completeness in multi-valued logics can be extended to the case where the set of truth values forms a lattice. This enables us to investigate the canonical completeness of logics having a partially ordered set of truth values, such as Belnap logic, and show that ABAC languages based on Belnap logic, such as PBel, are not canonically complete. We then construct a canonically complete four-valued logic using connections between the generators of the symmetric group (defined over the set of decisions) and unary operators in a canonically suitable logic. Finally, we propose a new authorization language @math , an extension of , which incorporates a lattice-ordered decision set and is canonically complete. We then discuss how the advantages of @math can be leveraged within the framework of XACML.
Jobe defined a canonically complete @math -valued logic @cite_8 . The operators and the construction of the unary selection operators using these operators are given in Appendix . The expression for @math above could be expressed in normal form, providing we could find suitable unary operators for a @math -valued logic. In we explain how to produce a suitable set of unary operators for an @math -valued logic.
@cite_8
2086979258
This paper examines the questions of functional completeness and canonical completeness in many-valued logics, offering proofs for several theorems on these topics. A skelet al description of the domain for these theorems is as follows. We are concerned with a proper logic L , containing a denumerably infinite class of propositional symbols, P, Q, R, …, a finite set of unary operations, U 1 , U 2 ,…, U b , and a finite set of binary operations, B 1 , B 2 , …, B c . Well-formed formulas in L are recursively defined by the conventional set of rules. With L there is associated an integer, M ≧ 2, and the integers m , where (1 ≦ m ≦M), are the truth values of L .