The Model

We now define the model formally by describing how the overall global state and the individual principal local states are defined as well as by describing how actions update the state. The model consists of the asynchronous composition of a set of named, communicating processes, each augmented with a local store in which to keep track of the current information it ``knows'', and with a set of bindings for the variables appearing in the process. Each principal involved in the protocol is modelled as one of these processes and is described by a sequence of actions it is to perform and by the initial state of its local store. The initial state of the bindings is assumed to be empty. One process, the intruder, is not completely specified. Only the initial state of its local store is given and it is allowed to perform any ``realistic'' actions. For example, the intruder is not allowed to decrypt messages with a key it does not possess and it is not allowed to send messages that it cannot create with the information in its local store. But it is allowed to receive and send messages arbitrarily, possibly intercepting messages intended for other principals or possibly impersonating a trusted principal.

More formally, each principal is modelled as a 4-tuple $\langle N, p, I, B \rangle$, where:

• $N \in \mbox{ {\em names}}$ is the name of the principal.
• p is a process (similar in style to CSP) given as a sequence of actions to be performed.
• $I \subseteq {\cal M}$ is a set of all messages known (which can be produced) by the principal. ${\cal M}$ is the set of all possible messages. Typically I will be infinite and in particular, it is closed under encryption, decryption, pairing (concatenation), and projection. For example, if $m, k \in I$ then $\{ m \}_{k} \in I$.For some set of messages J , we will use $\overline{J}$ to denote the closure of J under these operations.
• $B : \mbox{ {\em vars}}(p) \rightarrow I$, where vars(p) is the set of variables appearing in the process p , is a set of bindings.

The global state is then maintained as the composition of the participating principals, along with the intruder process, a list of permanent secrets, a list of temporary secrets, and a set of counters indexed by the pairs of principals participating in protocol runs. More formally, the global state is a 5-tuple $\langle \Pi, C_{i}, C_{r}, S_{s}, S_{t} \rangle$, where:

• $\Pi$ is the product of the the individual principals and the intruder process. This product is asynchronous, yielding an interleaving semantics, with the restriction that processes synchronize on messages.
• $C_{i} : \mbox{ {\em names} } \times \mbox{ {\em names} } \rightarrow {\Bbb N}$ gives the difference between the number of times some principal with name A has begun initiating a protocol with some other principal with name B and the number of times B has finished responding to principal A . If a counter ever gets a negative value this means that B has finished responding in a protocol with A (i.e. believes A has participated in the protocol) without A having taken part in the protocol.
• $C_{r} : \mbox{ {\em names} } \times \mbox{ {\em names} } \rightarrow {\Bbb N}$ gives the difference between the number of times some principal named A has begun responding to some other principal named B and the number of times B has finished initiating a protocol with A . If a counter ever gets a negative value this means that B has finished initiating a protocol with A (i.e. believes A has participated in the protocol) without A having taken part in the protocol.
• $S_{s} \subseteq {\cal M}$ is a set of messages that are are considered safe secrets. These are the set of words that the intruder is never allowed to know. This set remains constant and usually includes things like the private keys that principals use to communicate with a server.
• $S_{t} \subseteq {\cal M}$ is a set of messages that are are considered temporary secrets. This is the set of new secrets generated during the run of the protocol. These are secrets which we assume the intruder may be able to discover by some outside means, but which the protocol should not reveal, such as session keys.

The specific actions that a principal may perform can be divided into internal actions and communication actions. The internal actions are performed asynchronously. Any principal is allowed to perform an internal action and interleaving is used to model all possible behaviors when multiple principals can make a transition. We define a transition relation $\rightarrow$ between principals such that A $\rightarrow$ B if and only if principal A can take an action and become a principal that behaves like B.

Communication actions consist of send and receive actions. Each receive action can potentially change the principal's local store, reflecting any new information it has ``learned.'' Communication actions can only occur in pairs and both principals make a transition simultaneously. These communication actions are also interleaved with the possible actions of other automata.

In order for a communication action to take place, the message being sent must unify with the message being received. A message s-msg from principal $\mbox{\bf A} = \langle A, p, I_{A}, B_{A} \rangle$ unifies with a message r-msg from principal $\mbox{\bf B} = \langle B, q, I_{B}, B_{B} \rangle$, if there exist a substitution $\sigma_{B} : \mbox{\em vars}(q) \rightarrow I_{A}$extending $B_{B}$ $(B_{B} \subseteq \sigma_{B})$, such that $B_{A}$(s-msg) = $\sigma_{B}$(r-msg). If the messages unify, then the following transitions can be taken:

$$\begin{eqnarray*} \langle A, \mbox{ {\sc send}({\em s-msg})}.p', I_{A}, B_{A} \r... ...ngle & \rightarrow & \langle B, q', I_{B}', \sigma_{B} \rangle\ \end{eqnarray*}$$

where $I_{B}' = \overline{I_{B} \cup \sigma_{B}(\mbox{\em r-msg})}$.Because we require that s-msg unify with r-msg, if there is already a pair (var, val) in B for some var appearing in r-msg, then the corresponding value in s-msg must be val. Thus the updates to B only add new bindings and never change previous bindings.

For the most part internal actions are used to create or discover new information. For example, NEWNONCE is used to create a nonce. Nonces are globally distinct, and each NEWNONCE action creates a nonce that has not appeared up to that point in the protocol. The new nonce is added to the principal's local store. NEWSECRET works similarly, except that this is supposed to model generating a new session key which can then be used to encrypt messages. More formally:

$$\begin{eqnarray*} \langle A, \mbox{{\sc newnonce}({\em var})}.p', I, B \rangle &... ...p', I, B \rangle & \rightarrow & \langle A, p', I', B' \rangle\ \end{eqnarray*}$$

where in both cases, if val is the new value generated by the action, then $I' = \overline{I \cup \mbox{{\em val}}}$ and $B' = B[\mbox{{\em var} $\leftarrow$\space {\em val}}]$. If the action was a NEWSECRET action, then $S_{t}$ is updated in the global state as well to $S_{t}' = S_{t} \cup \mbox{\em val}$.

Additionally, the intruder is allowed to perform a GETSECRET action which it can use to acquire a secret previously generated by a principal using NEWSECRET. This models the possibility of session keys being compromised. It allows us to have two classes of secrets, those which we assume to be ``permanent'' like a private key between a server and a trusted principal, and those secrets which are ``temporary'' such as session keys. We need to allow the intruder to obtain session keys in order to allow for the possibility of replay attacks which would allow the intruder to establish an old compromised key as a session key. However, we also need to restrict the the usage of GETSECRET or else the intruder would be allowed to compromise a session key immediately after it is generated and before it is ever used. For this reason, we only allow the intruder to perform a GETSECRET action to compromise a key which has already been established or used in a protocol. Formally,

$$\begin{eqnarray*} \langle Z, \mbox{\sc getsecret}.p', I, B \rangle & \rightarrow & \langle Z, p', I', B \rangle\ \end{eqnarray*}$$

where for some val $\in S_{t}, I' = \overline{I \cup \mbox{{\em val}}} \mbox{ and in the global state } S_{t}$ is updated to $S_{t}' = S_{t} -${val}.

Finally, we have four special actions BEGINIT, ENDINIT, BEGRESPOND, and ENDRESPOND. These are used to mark the beginning and the end of a principal's participation in a protocol. We use them to guarantee that if the principal named A finishes the protocol (performs ENDINIT(B)) then the principal named B has participated in the protocol (performed BEGRESPOND(A)). We do this by maintaining counters for each pair of principals participating in a protocol. More formally,

$$\begin{eqnarray*} \langle A, \mbox{{\sc beginit}($B$)}.p', I_{A}, B_{A} \rangle & \rightarrow & \langle A, p', I_{A}, B_{A} \rangle\ \end{eqnarray*}$$

and we update the global state by setting the new value of $C_{i}(A,B)$:$$C_{i}'(A,B) = \left\{ \begin{array} {ll} C_{i}(A,B) + 1 & \... ...space is defined}\ 1 & \mbox{otherwise} \end{array} \right.$$

Similarly,

$$\begin{eqnarray*} \langle B, \mbox{{\sc endrespond}($A$)}.p', I_{B}, B_{B} \rangle & \rightarrow & \langle B, p', I_{B}, B_{B} \rangle\ \end{eqnarray*}$$

and we update the global state by setting the new value of $C_{i}(A,B)$:$$C_{i}'(A,B) = \left\{ \begin{array} {ll} C_{i}(A,B) - 1 & \... ... 0\ \mbox{\em error} & \mbox{otherwise} \end{array} \right.$$

The definitions for BEGRESPOND and ENDINIT are identical except that $C_{r}$ is updated in the global state instead of $C_{i}$.

The GETSECRET action may only be performed by the intruder, while the rest of the actions may be performed by any principal. The actions a particular honest principal may make are restricted to the sequence of actions p that represent its role in the protocol. The intruder has no such restriction and is allowed to make any action at any time, provided that if it performs a SEND action with message m , it must be the case that $m \in \overline{I_{Z}}$.

Recall that a trace is an alternating sequence of global states and actions and that we are interested in checking all possible traces. Clearly, there are a finite number of next states for each of the participants. In addition, while the intruder can generate an infinite number of messages, it is only allowed to send a finite number because each SEND much match with a RECEIVE. Since the there are a finite number of possible next states, we only consider a finite number of runs, we can perform a depth first search of the state space to generate all possible traces. We then check that no reachable state violates the security specification. Pseudocode for this algorithm can be found in figure 1.

   Figure 1: Model-checking algorithm

The remaining detail is how to maintain the local stores for the principals. The local store is accessed in three places. First, if principal $\langle A, p, I_{A}, B_{A} \rangle$ sends a message m , then we must insure that $m \in I_{A}$. Second, if the principal receives message m , then we must update $I_{A}$ to $I_{A}' = \overline{I_{A} \cup m}$. Finally, we check every global state to see if $s \in I_{Z}$ for some $s \in S_{s} \cup S_{t}$, where $I_{Z}$ is the intruder's local store. It turns that these local stores are infinite because of the closure operation. However, we never really need to compute the entire closure; we need only determine if a particular message is in the closure. So it suffices to represent the infinite set with a finite set of ``generators.'' This is the topic of the next section.