Information Technology Reference
In-Depth Information
. We can extend
J
to a meaning function
J
that provides an interpretation for
all
principal expressions, as follows:
P
J
(
A
)=
J
(
A
)
,
J
(
P ∧ Q
)=
J
(
P
)
J
(
Q
)
,
J
(
P |Q
)=
J
(
P
)
J
(
Q
)
Abadi and colleagues suggest that the principal
P
for
Q
can be viewed as syn-
tactic sugar for (
P |Q
)
(
D|Q
), where
D
is a (fictional) distinguished principal
that validates
P
's authorization to make statements on
Q
's behalf.
∧
3.2 Modal Logic
The calculus of principals provides a mechanism to describe ordering relation-
ships among principals. To reason about principals' credentials and access con-
trol, we turn to modal logic.
Syntax.
We assume the existence of a countable set of
propositional variables
,
ranged over by the meta-variables
p
and
q
. This set, along with formulas of form
“
P
speaks for
Q
” and “
P
says
ϕ
” that relate principals and statements, forms
the basis for a set
LogExp
of
logical formulas
. The abstract syntax for logical
formulas, ranged over by
ϕ
is given by the following grammar:
ϕ
::=
p
|¬ϕ
|
ϕ
1
&
ϕ
2
|
ϕ
1
or
ϕ
2
|
ϕ
1
⊃
ϕ
2
|
ϕ
1
⇐⇒
ϕ
2
|
P
says
ϕ
|
P
speaks for
Q
We will see that, semantically, the formula
P
speaks for
Q
holds when
P
≤ Q
is true in the underlying calculus of principals. It follows that
speaks for
is
monotonic with respect to both
∧
and
|
.
Logical Rules.
Having identified the syntax of logical expressions, we now intro-
duce a collection of logical rules for manipulating them. In particular, we define
a derivability predicate
ϕ
provided that the
formula
ϕ
is derivable from the collection of rules. This collection of rules can
be split into two groups: those standard for all modal logics and those relating
the modal logic to the calculus of principals. These rules appear in Figure 1.
over logical formulas: we write
Semantics.
The logical rules are useful for deducing relationships among princi-
pals and for reasoning about issues of delegation and trust. However, as given,
they merely provide rules for manipulating syntactic expressions: there is no
a
priori
reason to trust in their consistency. We therefore must introduce a seman-
tic framework in which to prove their
soundness
.
We have already seen that MSSs can provide suitable interpretations for the
calculus of principals. For simplicity of exposition, in the following discussion we
restrict ourselves to algebras of binary relations; however, arbitrary MSSs can
be used as the underlying model for principals with some additional overhead
(for example, see [3]).
We use
Kripke structures
to provide interpretations for logical formulas. A
Kripke structure
M
=
W, w
0
,I,J
comprises a set
W
of
possible worlds
;a
