A Modal Logic for Role-Based Access Control - Computer Network Security - page 185

E M [[ p ]] = I ( p )
E M [[ ¬ϕ ]] = W −E M [[ ϕ ]]
E M [[ ϕ 1 ∧ ϕ 2 ]] =

E M [[ ϕ 1 ]] ∩E M [[ ϕ 2 ]]

E M [[ ϕ 1 ∨ ϕ 2 ]] = E M [[ ϕ 1 ]] ∪E M [[ ϕ 2 ]]

E M [[ ϕ 1 ⊃ ϕ 2 ]] = E M [[ ¬ϕ 1 ]] ∪E M [[ ϕ 2 ]]

E M [[ ϕ 1 ≡ ϕ 2 ]] = E M [[ ϕ 1 ⊃ ϕ 2 ]] ∩E M [[ ϕ 2 ⊃ ϕ 1 ]]

J ( P )( w ) ⊆E M [[ ϕ ]] }
= {w |{w | ( w, w ) ∈

E M [[ P says ϕ ]] = {w |

J ( P ) }⊆E M [[ ϕ ]] }

W

if J ( Q ) ⊆

J ( P )

E M [[ P ⇒ Q ]] =

∅ otherwise

W

if ∀s ∈ T. P says s ⊃ Q says s,

E M [[ P T Q ]] =

∅ otherwise

E M [[ P serves T Q ]] = E M [[ P |Q T A|Q ]]

E M [[ P T Q ]] = E M [[ ( P ⇒ Q ) ∧ ( Q T P )]] .

Fig. 2. The meaning functions E M [[ − ]]

We then define a family (indexed by Kripke structures M ) of extended mean-

ing functions ]], which map arbitrary formulas to the sets of worlds in which

they are considered true. The definition of

E M [[ −

E M [[ − ]] appears in Figure 2. We write

( M,w ) | = ϕ if and only if w ∈E M [[ ϕ ]], and we say that M satisfies ϕ provided

that ( M ,w ) | = ϕ for all w ∈ W .Wesaythat ϕ is valid if every Kripke structure

M satisfies ϕ .

3.3 Logical Rules

The Kripke structures provide a precise semantics for the logic, but it is not
convenient to reason at that level. Thus, we introduce a collection of logical rules
for manipulating logical expressions. These rules, given in Figure 3, are sound
with respect to the Kripke semantics: for every formula ϕ ,if ϕ is derivable (i.e.,

ϕ ), then ϕ is valid (i.e., satisfied in all Kripke structures).

3.4 Our Extensions to the Access-Control Logic

The original Abadi logic is unable to adequately describe RBAC for two reasons:
its notion of roles conflicts with the RBAC concept, and it provides no way to
express the role-permission associations. Specifically, the Abadi logic includes a
special class of principals called roles , and arbitrary principals can adopt roles to
make requests (e.g., “( Alice as Fac ) says ϕ ”). However, adopting roles is at the
principal's discretion, and the effect is a reduction of privileges (e.g., Alice as Fac
has fewer privileges than Alice does). In contrast, an RBAC user is granted
privileges purely through the adoption of roles, and only when the user has been
authorized to adopt a given role. Thus, reasoning about RBAC requires us to