The intent hereafter is to present the verification algorithm. First of all, we would like to present an algebraic formalization of the message domain. The latter is defined in terms of a many sorted ordered algebra.

**Definition 4.1** **(Signature) **

An order-sorted signature is a pair
where is a partially
ordered set of sorts (type names) and is a set of function
symbols. Each function symbol *f* is associated with an arity i.e. a
finite word of the form where ranges over the domain . The function *f* is said
to be of arity *n* . The term is called the
domain of the function *f* while is called the codomain of
*f* . Functions with arity are called constants.

In order to lighten the notation, we will use, in the sequel, to denote a signature .

**Definition 4.2** **(-Algebra) **

Let be an order-sorted signature. An
order-sorted -algebra is a pair (,) where
is an -indexed family of sets, say , and is a
-indexed set of functions ,such that for all sorts *s* and *s*' , implies . Moreover, if then .

**Definition 4.3** **(Free Algebra) **

Let be
an order-sorted signature and *X* be an -indexed set of
variable identifiers or merely variables i.e. such that . The free -algebra over *X* is the pair
where:

- The -indexed family is defined as the least set that
satisfies:
- For all , .
- For all , .
- For all and for all , .

- The -indexed set of functions is made of functions of the form that take tuples of the form to .

The next definition introduces formally the algebra of
messages used within this work. First of all, we consider the
following sorts: *Msg* , *Key* , *Nonce* , *Agt* , *Nat* and
*Server* that classify respectively messages, keys, nonces,
agents, naturals and the server. We consider these function
symbols: *e* , *c* , *key* , *nonce* , *agt* that correspond
respectively to encryption, catenation, key generation, nonce
generation and agent generation. In addition, we assume the
existence of a constant *s* denoting the server. Let, and
*succ* be the usual natural constructors. The arities of these
functions are given below:

**Definition 4.4** **(Message Algebra) **

Let be the sort set and be the function symbol set . Let be an -indexed family of message variables. We endow with a partial order which stipulates that , , , and closed under reflexivity. We define the algebra of messages as the free -algebra over . The free terms of the latter algebra are called messages.

In what follows, we present formal definitions of roles and protocols.

**Definition 4.5** **(Protocol) **

A protocol is a sequence of communication steps. Each step is
a triple of the form where *A* and *B* are
principal identifiers, and *m* is a message. A triple
has to be read as: *A* sends the message *m* to
*B* .

**Definition 4.6** **(Role) **

A role is a sequence of communication steps. Each step is a
triple of the form where *P* is a principal
identifier, *m* is a message and . A triple
has to be read as: wait for receiving the
message *m* from the principal *P* . A triple has to be read as: send the message *m* to the principal *P* .

From the protocol definition, it is straightforward how we can
extract roles. A role *P* , for instance, is extracted from the
protocol by looking at all the steps (in the same order) in
which the character *P* is used to point out the sender or
the receiver.

**Table 5:**
The Verification Algorithm: Part I

The verification algorithm is reported in Tables 5
and 6. We assume that each principal comes with the
specification of two sets *KI*(*R*) and *Fresh*(*R*) . The set
*KI*(*R*) corresponds to the initial knowledge of the principal
*R* . Generally, the set *KI*(*R*) includes the identity of the
role *R* , the server identity (if it exists), the identities of
the other roles and all the keys that he shares with
other principals. The set *Fresh*(*R*) includes all those fresh
messages generated by the role *R* .

In Tables 5 and 6, we present the main functions invoked by the verification algorithm. The functions reported in Table 5 operate on messages while the functions reported in Table 6 operate on roles.

First of all, let us explain the functions operating on
messages. The Function *Glan* : takes as parameter a role, say
*R* , and yields a message set, say *M* . The latter embodies
all those messages received by *R* during all the protocol
steps. Given a message set *M* , the Function *Reduce* computes
a reduced message set by recursively decomposing and
decrypting (with known keys) those messages in *M* . For
instance, yields
. The function *Reduce* is
used essentially to perform role abstraction, therefore to
generate rules of the inference system. Given a message set
*M* , the function *Flat* computes a flattened message set by
recursively decomposing and decrypting non-elementary messages
in *M* . For instance, yields
. The function *Flat* is used to
generate the side conditions of the inference rules. After the
computation of the premise and the conclusion parts, the side
condition is generated. For example, if we want to know the
side condition of the rule and the set of fresh messages is . Then, we compute and we
put as side condition . Hence, the rule the
complete rule is .

The Function *Bind* takes as parameter a message set *M* and
yields a set of bindings. A binding is a pair (*m*,*X*) where
the first component is a message and the second component is a
message variable. The *Bind* function aims to bind all the
messages in *M* to newly allocated message
variables. Actually, in the verification algorithm, the *Bind*
function will be invoked with the set of unknown messages to
some role and hence replacing (or binding) these messages by
(or to) variables. The Function *Gen* takes as parameter a
message *m* together with a binding set *B* and yields the
argument message *m* in which we replace all the messages
occurring in *B* by their corresponding variables. Indeed, the
function *Gen* rewrites a message according to a binding. For
instance, given the binding , the message
*m*=*e*(*e*(*m*,*k*),*k*') will be rewritten into *m*'=*e*(*X*,*k*') . The
message *m*' denotes the interpretation of the message *m* by
a role for which the key *k* is unknown.

Now, we would like to explain the functions that generate the
rules and the constraint set. Recall that, the constraint set
tells us which messages the intruder has to find in order to
attack the protocol. The Function *GenRole* takes as
parameters a role *R* , an initial knowledge (message set) *KI*
and a set of fresh messages (those messages created by the
protocol specifically for a particular session) *Fresh* . The
computation is done step by step along the protocol steps. The
function *GenRole* gives as outcome the generalized version of
the role *R* . The computation of such a generalized role
involves the computation of the corresponding binding and
rewriting the role accordingly. Indeed, at first we collect
*M* , the set of messages received by *R* before the current
analyzed step. This is captured in the function *GenRoleStep*
by *Role*1 which is initially . Hence
*M*=*Glan*(*Role*1) . To obtain the reduced set associated with
*M* , say *RM* , and taking into account that we have an initial
knowledge (message set) *KI* and a set of fresh messages
*Fresh* , we compute . At this
point, it is straightforward to see that those messages in
) are unknown to the role
*R* . Those messages are then used to compute the binding *B*
according to which the transmitted message in the current step
will be generalized. The inference rules are computed so as to
associate one rule per protocol step. In other words, we
associate one inference rule per output communication made by
a particular role. The function *RoleRules*(*GRole*,*KI*,*Fresh*)
takes as input the generalized role *GRole* , the initial
knowledge *KI* and the fresh informations *Fresh* associated
with one role. If in the current step the role sends a
message, then the rule premises set includes all the
generalized messages received by this role before this current
step and the conclusion is the message sent at that step. The
rule side condition is pointed out by looking if the premises
set contains a fresh information vis-à-vis this
role. However, if at the current step the role receives a
message, we have only to update the premises set by adding
this message. To generate the complete inference system, we
have to apply the function *RoleRules*(*GRole*,*KI*,*Fresh*) to all
generalized roles in the protocol. For instance, we remark
that we associate to each step in the protocol an inference
rule, since whenever one role receives a message there is
necessary another which has sent it. Furthermore, since there
is one message sent per protocol step, we generate one rule
for each protocol step.

The Function *Collect* is devoted to the collection of those
constraints needed to perform a masquerade on a role *R* . The
function *Collect* takes as parameter the generalized role *R*
and the set of messages *K* , and returns the set of
constraints. Initially, the message set *K* is set to . Whenever the role *R* sends (output
communication) a message, the intruder adds it to his
knowledge *K* . When the role is waiting for some message, say
*m* , the algorithm generates a constraint of the form
(*K*,*Rules*,*m*) which should be read as follows: the intruder
has to synthesize the message *m* thanks to the proof system
*Rules* (inference rules) and also by using his knowledge *K* .

**Table 6:**
The Verification Algorithm: Part II