Information Technology Reference
In-Depth Information
3.1
Syntax
We start out by introducing a collection of principal expressions, ranged over by
P
and
Q
. Letting
A
range over a countable set of simple principal names, the
abstract syntax of principal expressions is given as follows:
P
::=
A
|
P
&
Q
|
P
|
Q
|
P
for
A
Q
The principal
P
&
Q
represents a compound principal who makes exactly those
statements made by both
P
and
Q
.
P
Q
represents an abstract principal cor-
responding to principal
P
quoting principal
Q
.
P
for
A
Q
represents a principal
P
acting on behalf of principal
Q
:
P
for
A
Q
is syntactic sugar for
P
|
Q
,
where
A
is a principal that vouches for
P
's authorization to make statements on
Q
's behalf [1].
For the logic itself, we let
p
range over a countable collection of primitive
propositions and define the abstract syntax for the logic as follows:
|
Q
&
A
|
ϕ
::=
p
|¬
ϕ
|
ϕ
1
∧
ϕ
2
|
ϕ
1
∨
ϕ
2
|
ϕ
1
⊃
ϕ
2
|
ϕ
1
≡
ϕ
2
|
P
says
ϕ
|
P
⇒
Q
P
serves
T
|
P
T
Q
|
Q
|
P
T
Q
Here,
T
ranges over sets of formulas that include only formulas of the forms
included on the first line (e.g., not involving
T
,
serves
T
,or
T
); the forms
involving
T
are our extensions.
Primitive propositions are used to represent requests and permissions, while
the formula
P
says
ϕ
represents principal
P
making the statement
ϕ
. In turn,
P
Q
represents a relationship between principals
P
and
Q
through which
statements of
P
can also be attributed to
Q
. The formula
P
⇒
T
Q
, pronounced
as “
P
is mimicked by
Q
on
T
,” is our extension to the logic, inspired by Howell
and Kotz's
restricted speaks for
relation
T
⇒
[9]. This
restricted mimics
formula
represents a weaker relation than
P
Q
, in part because only
P
's statements
from the set
T
can be attributed to
Q
. Finally,
P
serves
T
⇒
Q
(the
restricted serves
relation) and
P
T
Q
(the
restricted inherits
relation) are syntactic sugar for
P
|
Q
T
A
|
Q
and (
P
⇒
Q
)
∧
(
Q
T
P
), respectively.
3.2
Semantics
The semantics of the logic is based on Kripke structures. A Kripke structure is a
triple
,where
W
is a set of possible worlds,
I
is an interpretation
function that maps each primitive proposition to a set of worlds, and
J
is an
interpretation function that maps each primitive principal to a binary relation
over
W
.Weextend
J
to a function
J
over arbitrary principal expressions as
follows:
M
=
W, I, J
J
(
A
)=
J
(
A
)
J
(
P
&
Q
)=
J
(
P
)
J
(
Q
)
∪
J
(
P
Q
)=
J
(
P
)
J
(
Q
)
|
◦
J
(
P
)
J
(
Q
)
=
{
(
w
1
,w
3
)
|∃
w
2
.
(
w
1
,w
2
)
∈
∧
(
w
2
,w
3
)
∈
}
.
