Information Technology Reference
In-Depth Information
Notice that, implicitly, the banking server believes that the only way WB would
have Bob's pwd is if Bob provided it to allow WB to make requests on Bob's
behalf.
The server passes the username-password pair on to the password server,
which confirms the validity of that pair. Thus, from the perspective of the online-
banking server,
says
Bob, pwd
speaks for
PS
(
Bob
)
(4)
Combining the pieces of information (2) and (4), S determines that
(
WB
∧ PS
)
says
(
Bob, pwd
speaks for
Bob
)
.
Therefore, using Rule (3), the banking server deduces that
WB
|Bob
speaks for
S|Bob.
Because
speaks for
is a monotonic operator, this fact yields
WB
|Bob
speaks for
(
WB
|Bob ∧ S|Bob
)
,
and hence
for
S
Bob
)
.
Combining this result with the original request (1), the banking server can de-
duce that
(
WB
|Bob
)
speaks for
(
WB
WB
for
S
Bob
says
r.
In accordance with its access-control policy, the online banking server then grants
the request.
We return to this example in Section 6, where we discuss how it can be
verified in higher-order logic and HOL. However, we first describe how the logic
itself can be embedded into HOL.
5
Implementing the Logic in HOL
In the previous sections, we have described the logic for access control and showed
how it can be used to reason about brokered requests. Furthermore, this logic
played an important role in the development of the CSIv2 standard, by providing
a way to consider how to interpret requests and the SAS data structure.
To provide mechanized support for reasoning about the standard and its
applications, we have embedded a subset of the logic into the Cambridge HOL
(Higher Order Logic) theorem prover [4]. HOL supports a predicate calculus
that is typed and allows variables to range over predicates and functions. HOL
is implemented using the meta-language ML [6] and, at the lowest level, is a
collection of ML functions that operate on sequences. The benefits of using
HOL (or any open theorem prover) are at least threefold: (1) our results are
formally verified and checked, (2) our results are easily reused by others and can
