Implementing a Calculus for Distributed Access Control in Higher Order Logic and HOL - Computer Network Security - page 41

be independently checked, and (3) future modifications and extensions to HOL
theories can be easily verified for correctness.
There are multiple ways to embed a logic in HOL. The simplest way is to
perform an axiomatic extension of the HOL logic: all of the desired theorems
of the embedded logic (e.g., the axioms and inference rules in Figure 1) are
defined as unproved axioms in HOL. This method is easy, but it may result in
an inconsistent theory, thereby defeating the point of theorem proving.
The other possibility is to perform a conservative extension of the HOL logic:
the desired logic is introduced as a series of definitional extensions in HOL, and
all desired axioms and theorems are proved within the HOL system. Although
this method requires much more work than an axiomatic extension, any resulting
theories are guaranteed to be sound.
We therefore choose this latter approach, which requires the following steps:

1. Creating HOL datatypes for principals, formulas, and Kripke structures,
along with their type constructors
2. Defining in HOL the models operator (

=)
3. Proving the soundness of the desired axioms and inference rules

|

We consider these steps in turn, as we give a flavor of the embedding.
The first step is to introduce new HOL datatypes for principal expressions,
logical formulas, and so on. To do this, we use the Hol datatype command, as
in the following example:

Hol datatype principal = name of string
| meet of principal → principal
| quoting of principal → principal

| forp of principal → principal → principal;

Recall that, for any structure M = W, w 0 ,I,J and world w ∈ W , the prop-

erty = ϕ is true if and only if w ∈E M [[ ϕ ]]. Therefore, one way of defining

the models predicate in HOL is first to define the meaning function

M,w |

E M [[ − ]] ,

J .

which in turn requires a definition for the extended interpretation function

We have defined these functions in HOL as follows:

val JextDef =
def ( Jext ( World,w0,Ifn,Jfn) ( name A) = Jfn World ( name A)) ∧
( Jext ( World,w0,Ifn,Jfn) ( P meet Q) =
Jext ( World,w0,Ifn,Jfn) P UNION Jext ( World,w0,Ifn,Jfn) Q) ∧
( Jext ( World,w0,Ifn,Jfn) ( P quoting Q) =
Jext ( World,w0,Ifn,Jfn) Q O Jext ( World,w0,Ifn,Jfn) P) ∧
( Jext ( World,w0,Ifn,Jfn) ( P forp D) Q =
( Jext ( World,w0,Ifn,Jfn) Q O Jext ( World,w0,Ifn,Jfn) P) UNION
( Jext ( World,w0,Ifn,Jfn) Q O Jext ( World,w0,Ifn,Jfn) D)) : thm