Information Technology Reference
In-Depth Information
Because delegated authority must be carefully controlled and limited to pre-
vent fraud, reasoning about delegation must be done precisely, accurately, and
consistently. To meet these needs we use a specialized calculus and modal logic
for reasoning about brokered requests and delegations. In the next section, we
give an overview of this logic; we then revisit the banking scenario in Section 4.
3 Calculus for Reasoning about Brokered Requests
In a series of papers [5,3,8], Abadi and colleagues introduced a logic for au-
thentication and access control for distributed systems. This logic incorporates
a calculus of principals into a standard multi-agent modal logic: the calculus of
principals provides a mechanism to describe ordering relationships among princi-
pals, while the modal logic provides a mechanism for reasoning about principals'
credentials and the statements they make. The result is a logic that supports
reasoning about access control, delegation, and trust.
3.1 Calculus of Principals
Syntactically, the calculus of principals is very simple. We assume the existence
of a countable set containing
simple principal names
and ranged over by the
meta-variable
A
. The set of
principal expressions
(ranged over by
P
and
Q
) has
an abstract syntax given by the following grammar:
P
::=
A
|
P ∧ Q
|
P |Q
|
P
for
Q
Intuitively,
P ∧ Q
denotes a principal whose statements correspond precisely
to those statements that
P
and
Q
jointly make.
P |Q
denotes a principal whose
statements correspond to those that
P
attributes to
Q
. Finally,
P
for
Q
denotes a
principal whose statements correspond to those that
P
is authorized to attribute
to
Q
. We consider
P ∧ Q
to be a stronger (i.e., more trustworthy) principal than
either
P
or
Q
because of the consensus. Likewise, we consider
P
for
Q
to be a
stronger principal than
P |Q
because of the authorization.
Semantically, we interpret principal expressions over a multiplicative semi-
lattice semigroup (MSS). An MSS (
S,
,
)isaset
S
equipped with two binary
operations (
and
):
is idempotent, commutative and associative, while
is
associative and distributes over
in both arguments. For
S
-elements
x
and
y
,
the element
x
y
is the
meet
of
x
and
y
. Thus the operator
induces an ordering
≤
on
S
as follows:
x ≤ y
if and only if
x
=
x
y
.
As a common (and useful) example of a MSS, consider any set
T
, and let
T
R
be a set of binary relations over
T
that is closed under union (
∪
) and relational
composition (
◦
). It is straightforward to verify that (
T
R
, ∪, ◦
) satisfies the MSS
amounts to the superset relation:
r
1
≤ r
2
if
and only if
r
1
=
r
1
∪ r
2
, which is true precisely when
r
1
⊇ r
2
.
Every MSS can be used to provide an interpretation for principal expressions.
Specifically, consider any structure
≤
axioms. In this case, the ordering
is an MSS and
J
is a
total function that maps each simple principal name to an element of the MSS
M
=
P,J
, where
P
