The Specification

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 $X \hookrightarrow Y$ 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: $$S \rightarrow SxSy \vert \epsilon$$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 $X \hookrightarrow Y$ 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.