Article Preview
TopIntroduction
Traditional security policy systems provided a simple yes/no answer to access requests. However, it was recognized that access often depends on some user-actions being performed before access is granted. For instance, an access rule may specify that users are allowed to download music files provided that they pay 1$ first. In this case, if a user requests to download, for example, the latest single of Muse, s\he is asked to pay 1$. If the payment is made successfully, the user is allowed to download the requested file. Such requirements are called pre-obligations. Neither traditional access control models such as DAC (NCSC, 1987) and RBAC (Ferraiolo & Kuhn, 1992) nor more recent contextual security models such as ASL (Jajodia, Samarati, & Subrahmanian, 1997) and OrBAC (Abou El Kalam et al., 2003) support preobligations: In these models, an access request is only allowed if the conditions associated with a permission authorizing the access are true when the access request is made.
There are several advantages of supporting pre-obligations in the policy language. First, this provides additional expressiveness since it enables policy administrators to specify that subjects may fulfill some of the access requirements after the access request. Furthermore, it separates the expression of requirements from the functional specification (the code) of the application. Thus, the analysis of policy requirements is simplified and administrators are able to modify the behavior of the system by updating policy rules without recoding the application.
To support pre-obligations, a number of works (Bettini, Jajodia, Wang, & Wijesekera, 2002, 2003 ; Ni, Bertino, & Lobo, 2008) subordinate obligations to access control rules. This approach has some limitations. For instance, obligations are only activated after access requests and general obligations are not supported. In addition, this approach generally produces intricate access control policies since permissions and obligations are often specified within the same rule. This is the approach used in (Ni et al., 2008) to specify permissions and their associated pre-obligations. The main limitation of previous works on pre-obligations is however that none formalized the effects of supporting pre-obligations on the evolution of the authorization and obligation policy states. This is essential to provide a deeper understanding of pre-obligations and their enforcement in information systems. In addition, this formal approach allows the study and the analysis of change in the authorization and obligation policy states in the presence of pre-obligations. Therefore, it enables, for instance, to derive plans to reach some particular authorization states (Becker & Nanz, 2008 ; Craven et al., 2009) or to explain the deactivation of pre-obligations after permission activation.
In this paper, we study the specification and the enforcement of pre-obligations. In our approach, we formalize the enforcement of pre-obligations using an extension of the language Lactive (Baral & Lobo, 1996). Lactive enables the description of change in state using concepts from action specification languages (Gelfond & Lifschitz, 1993).Thus, it enables reasoning about state evolution and the study of interactions between pre-obligations and the authorization and obligation policy states. Lactive also supports the specification of reactive behavior using active rules. This feature enables us to provide formal operational semantics for the enforcement of pre-obligations.