Deontic STIT logic, from logical paradox to security policy

Our ultimate goal in this article is to develop a logic to formalize security policies, especially for intrude detection in pervasive computing environments. Security is a high priority requirement for lots of information systems, and it is considered in practice as a more and more significant issue. In most systems, security requirements may already exist but usually remain informal, and starting from these requirements it is of growing interest to be able to define a rigorous security policy.

In pervasive computing environments, resources like information and services are accessible anywhere and anytime via any devices (Barolli and Takizawa 2010; Marcelloni et al. 2014; Ogiela et al. 2014; Ramos et al. 2014; Choi et al. 2014). There are different sorts of users and services, and some of them may be unknown or not predefined (Kagal et al. 2001). The distribution of resources in these environments forces us to leverage decentralized security management. In this setting, the environment is divided into a number of domains based on different factors. For each domain, there is a security agent with an administrator (we call it authority) who is responsible for preserving the security of resources that are under their protection.

Several authors have used deontic logic to specify security policies (Glasgow et al. 1992; Jones and Sergot 1992; Demolombe and Jones 1996; Cuppens-Boulahia and Cuppens 2008; Cuppens et al. 2013). These authors outlined the main features of this formalism to analyze further various aspects of security, to formalize previously informal security requirements and to provide a flexible and expressive language for specifying security properties. Deontic logic is a formal study of norms and deontic modalities (such as permission, forbidden and obligation). In 1951, the publication of von Wright (1951) indicates the birth of deontic logic. With the work of Meyer (1988), deontic logic became a part of computer science. Deontic logic has been a valuable tool in the specification and reasoning of security policies because key notions in security such as permission, authorization, prohibition and obligation are exactly the subjects of deontic logic. To apply deontic logic in the specification of security policies in pervasive computing environments, we need a deontic logic in which different authorities are explicitly modeled. Deontic STIT logic offers one option for this purpose. Deontic STIT logic (Horty 2001; Kooi and Tamminga 2008; Sun 2011; Broersen 2011), grounded on STIT (see to it that) theory (Belnap et al. 2001), is a branch of deontic logic developed by philosophers, logicians and computer scientists in recent years. In Kooi and Tamminga (2008) and Sun (2011), the authors develop deontic logics which are capable of models commands from different authorities.

Another reason for choosing deontic STIT logic comes from the motivation of the specification of policies of intrusion detection. Cuppens-Boulahia and Cuppens (2008) investigate the specification of intrusion detection policies. They argue that it is appropriate to use the bring it about modality for specification. Since the difference between bring it about and see to it that is negligible, deontic STIT logic can be an appropriate tool to specify policies of intrusion detection.

From a logical perspective, one limitation of the existing deontic STIT logic is that they are suffered from some logical paradoxes. This paper develops a new multi-authority deontic STIT logic (MADL) to overcome this problem such that our logic is more suitable for the application to security than the existing deontic STIT logics.

In the rest of this paper, we recap the miners paradox in Sect. 2 as a trigger of our further study. We then present our deontic STIT logic in Sect. 3. In Sect. 4 we discuss some related work. Section 5 summarizes this article with future work.

In recent years, many deontic logicians get interested in the miners paradox (Gabbay et al. 2014). The miners paradox presented in Kolodny and MacFarlane (2010) is described like this:

There are 10 miners trapped in either shaft A or shaft B, but we don’t know which one. Water threatens to flood the shafts. We have sandbags to block only one shaft. If one shaft is blocked, all water will flood into the other shaft, killing all miners inside. If we block neither shaft, both will be flooded partially, killing 1 miner.

Since we don’t know the miners’ location, it seems plausible that:Which contradicts to (1).

The deontic STIT logic proposed in Horty (2001), Kooi and Tamminga (2008), Sun (2011) cannot solve this paradox: Although the inference from (2)–(4) to (5) is not valid in the logic introduced in Sun (2011), both Horty (2001) and Sun (2011) are not capable of predicting (1). In this paper, we develop MADL, which is able to block the inference from (2)–(4) to (5) meanwhile predicts (1)–(4).

In deontic STIT logic, the semantics of deontic operator is interpreted by best choices, which are defined via a preference relation over sets of possible worlds. Such a relation is characterized by a preference relation over possible worlds through lifting. In the literature, there are many methods of lifting preference, which are summarized by Lang and van der Torre (2008) as follows:In utilitarian deontic logic (UDL) of Horty (2001), Kooi and Tamminga (2008), Sun (2011), strong lifting is used. According to strong lifting, the best choices in the miners paradox are \({\textit{block}}\_ A\), \({\textit{block}}\_ B\) and \({\textit{block}}\_{\textit{neither}}\). Therefore, “we ought to block neither” is false. To have a more precise understanding of such reasoning, we now formally review the UDL introduced in Sun (2011).

The language of utilitarian deontic logic, \(\mathfrak {L}_{udl}\), is defined by the following BNF: Let \({\varPsi }=\{p,q,r,\ldots \}\) be a set of propositional atoms and \(Agent=\{1,\ldots ,n\}\) be a set of agents,where \(p\in {\varPsi }, G\subseteq Agent\). Intuitively, \([G]\psi \) says that “group G sees to it that \(\psi \).” \(\bigcirc _{G}\psi \) says that “G ought to see to it that \(\psi \).” \(\bigcirc _{G}(\psi /\phi )\) says that “G ought to see to it that \(\psi \) under the condition \(\phi \).” The semantics of UDL is defined via the notion of utilitarian models.

We use \(w\preceq v\) to represent that w is no better than v and \(w\approx v\) as an abbreviation of \(w\preceq v\) and \(v\preceq w\).

\(X\prec ^s Y\) is used to denote \(X\preceq ^s Y\) meanwhile \(Y\not \preceq ^s X\).

\(T\preceq ^s_{H} T'\) means that “\(T'\) weakly dominates T.” From a perspective of decision theory, \(T\preceq ^s_{H} T'\) says that whatever other agents do, the result obtained by choosing \(T'\) is no worse than that of choosing T. \(T\prec ^s_{H}T'\) is short for \(T\preceq ^s_{H} T'\) and \(T' \not \preceq ^s_{H} T\). If \(T\prec ^s_{H} T'\), then we say \(T'\) strongly dominates T.

Intuitively, Choice(H / Y) are those choices made by group H which are consistent with Y.

\(T\preceq ^s_{H/Y}T'\) means that “\(T'\) weakly dominates T under the condition of Y.” \(T\prec ^s_{H/Y}T'\), read as “\(T'\) strongly dominates T under the condition of Y,” is short for \(T\preceq ^s_{H/Y}T'\) and \(T'\not \preceq ^s_{H/Y}T\).

Here \(\Vert \psi \Vert =\{v\in W: M,v\vDash \psi \}\).

The miners paradox is characterized by a model \(Miners= (W, V ,Choice, \preceq )\), \(W=\{v_1,\ldots , v_6\}\), \(Choice(H)=\{\{v_1,v_2\},\) \(\{v_3,v_4\},\{v_5,v_6\}\}\), \(Choice(Agent-H)=\{W\}\), \(v_3\approx v_6\preceq v_1\approx v_2 \preceq v_4 \approx v_5\), \(V({\textit{in}}\_ A) =\{v_1,v_3,v_5\}\), \(V({\textit{in}}\_ B) =\{v_2,v_4,v_6\}\), \(V({\textit{block}}\_ A) =\{v_5, v_6\}\), \(V({\textit{block}}\_ B) =\{v_3, v_4\}\), \(V({\textit{block}}\_{\textit{neither}}) =\{v_1, v_2\}\) (Fig. 1).

Group H can choose \({\textit{block}}\_A\), \({\textit{block}}\_B\) or \({\textit{block}}\_{\textit{neither}}\), while other agents can only choose W. All the three choices of group H are optimal by the strong lifting. Therefore, \(Miners, v_1\not \vDash \bigcirc _H ({\textit{block}}\_{\textit{neither}})\). Therefore, UDL cannot solve the miners paradox.

Using logics to handle the problems of specifying and reasoning about the security of information systems started from 1988 by Glasgow and MacEwen (1988). Since then, various types of logic have been used to model inference abilities and specification of security policies. Van Hertum et al. (2016) have recently proposed a multi-agent variant of autoepistemic logic, called Distributed Autoepistemic Logic with Inductive Definitions (dAEL(ID)), to be used as a says-based access control logic. By applying the semantic principles of autoepistemic logic to characterize the says-modality, dAEL(ID) allows us to derive a statement of the form \(says_{\lnot k} \psi \) on the basis of the observation that k has not issued statements implying \(\psi \). Supporting reasoning about such negated says-statements allows dAEL(ID) to straightforwardly model access denials, which can hardly be modeled by previous says-based access control logics.

In this article, we have developed a deontic STIT logic with the possible application to the specification of security policy for intrude detection in the pervasive computing environment. Compared to the existing deontic STIT logics, an advantage of our logic is that it is capable of solving the miners paradox, a logical paradox which recently grabs attentions of logicians, philosophers, linguistists and computer scientists. A complete and sound axiomatization for our logic was developed. Concerning future works, we will study the computational complexity of our logic and perform some case study for the application of our logic to security policies.