Information Technology Reference
In-Depth Information
6 Banking Example in HOL Theorem Prover
Having described our HOL implementation, we can now return to the online-
banking example introduced in Section 4. In that scenario, an online-banking
server (
SD
) receives a request from a web browser (
WB
) purportedly working
as a broker on behalf of a bank client Bob. Determining whether or not that
request should be honored required a chain of reasoning based on statements
regarding who spoke for whom, delegation relationships, and requests. That
chain of reasoning is captured by the following theorem:
∀WB Bob BobPwd PS SD req World w0 Ifn Jfn w1.
((
World,w0,Ifn,Jfn),w1) MD
(
WB says BobPwd speaks for Bob) imps
(
PS says BobPwd speaks for Bob) imps
(((
WB meet PS) says BobPwd speaks for Bob) imps
(
WB quoting Bob) speaks for
(
SD quoting Bob)) imps
(
WB says Bob says req) imps
((
WB forp SD) Bob says req)
This goal can be proved by applying a series of HOL tactics to the logical
rules given in Figure 1. As mentioned previously, we cannot use the first rule of
Figure 1 directly. Instead, we must introduce particular instances of this rule,
which we can then verify in HOL. To prove the desired theorem, we need four
specific instances, one of which is shown below:
(
ϕ
1
imps
(
ϕ
2
imps
(
ϕ
3
imps
(
ϕ
4
imps
ϕ
5
))))
imps
((
ϕ
5
imps
(
ϕ
4
imps
ϕ
6
))
imps
(
ϕ
1
imps
(
ϕ
2
imps
(
ϕ
3
imps
(
ϕ
4
imps
ϕ
6
)))))
To verify the soundness of these new rules in HOL system, we must show that
they are satisfied by all Kripke models. Thus, for example, we must prove the
following theorem in HOL:
∀
s1 s2 s3 s4 s5 s6 World w0 Ifn Jfn w1.
((
World,w0,Ifn,Jfn),w1) MD
((
s1 imps
(
s2 imps
(
s3 imps
(
s4 imps s5)))) imps
((
s5 imps
(
s4 imps s6)) imps
(
s1 imps
(
s2 imps
(
s3 imps
(
s4 imps s6)))))) : thm
Proving the soundness of these rules is time consuming but straightforward.
However, having to prove them significantly increases the burden for proving the
desired theorem about the banking scenario.
7 Conclusions
Our original objective was to implement an access-control logic in HOL in order
to reason about the CSIv2 protocol in ways that are assured and independently
