There are two kinds of properties that we currently are interested in. The first is a kind of secrecy property. We provide the model checker with a set of terms which the intruder is not allowed to obtain. During the verification, we simply check that the intruder does not have possession of any of the terms in this set. This is not as straightforward as it might seem because the information known to the intruder is typically infinite. For example, if the intruder knows a piece of data and a key, it can repeatedly encrypt this data to produce an infinite number of new terms.
The second property is a temporal property that Woo and Lam call
correspondence [23]. In particular, we are interested in
checking that ``if principal A believes it has finished a protocol
run with principal B , then principal B must have begun a protocol
run with principal A .'' This can be generalized to ``if event X
occurs, then event Y must have occurred in the past.'' (We will use
Woo and Lam's notation to denote this.)
However, there is more to this property than a simple temporal
relationship. The relation between Y events and X events must be
a one-to-one mapping. More formally, the projection of any trace onto
X events and Y events must be derivable from the following
grammar:
where the terminal symbols x and y represent the events X and Y .
In particular, if principal A believes it has completed two protocol
runs with principal B , then principal B must have at least begun
two protocol runs with principal A . Each end of a protocol run on
A 's part must be mapped to a separate beginning of a protocol run on
B 's part.
In order to check for this kind of property, we will augment the
global state with counters. For each correspondence property we will maintain a separate counter which will keep
track of the difference between the number of Y events and X
events. If this counter ever turns negative (i.e. there are more X
events than Y events) then the correspondence property will be
violated at that point (there will be no one-to-one mapping from X
events to Y events). Conversely, as long as the counter never goes
negative there is always a one-to-one mapping from X events to Y
events.