Dinesh, N., Joshi, J.K., Lee, I., and Sokolsky, O. (2009). Permission to Speak:
A Logic for Access Control and Conformance. In submission. A preliminary 
version appeared as an invited paper in the Workshop on Formal Languages for 
Contract-Oriented Software (FLACOS). 


Abstract: Formal languages for policy have been developed for access control 
and conformance checking. In this paper, we describe a formalism that combines 
features that have been developed for each application. From access control, 
we adopt the use of a saying operator. From conformance checking, we adopt the 
use of operators for obligation and permission. The operators are combined 
using an axiom that permits a principal to speak on behalf of another. The 
combination yields benefits to both applications. For access control, we 
overcome the problematic interaction with classical reasoning. For conformance,
our formalism accommodates nested obligations and permissions.

The axioms result in a decidable logic, and we characterize its complexity. We 
integrate the axioms into a logic programming approach, which lets us use 
quantification in policies while preserving decidability of access control 
decisions. Conformance checking, in the presence of nested obligations and 
permissions, is shown to be decidable. Non-interference is characterized using 
reachability via permitted statements.