Algorithm

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 $\Sigma$ is a pair $(({\cal S},\leq),\Sigma)$ where $({\cal S},\leq)$ is a partially ordered set of sorts (type names) and $\Sigma$ is a set of function symbols. Each function symbol f is associated with an arity i.e. a finite word of the form $s_1\times\ldots\times s_n\rightarrow s_{n+1}$where $s_i$ ranges over the domain ${\cal S}$. The function f is said to be of arity n . The term $s_1\times\ldots\times s_n$ is called the domain of the function f while $s_{n+1}$ is called the codomain of f . Functions with arity are called constants.

In order to lighten the notation, we will use, in the sequel, $\Sigma$to denote a signature $(({\cal S},\leq),\Sigma)$.

Definition 4.2 ($\Sigma$-Algebra)

Let $(({\cal S},\leq),\Sigma)$ be an order-sorted signature. An order-sorted $\Sigma$-algebra is a pair ($\cal A$,$\cal F$) where $\cal A$ is an ${\cal S}$-indexed family of sets, say ${\cal A}=\bigcup_{s\in {\cal S}} {\cal A}_s$, and $\cal F$ is a $\Sigma$-indexed set of functions $\{f_{\cal A}\;\vert\; f\in\Sigma\}$,such that for all sorts s and s' , $s\leq s'$ implies ${\cal A}_s\subseteq {\cal A}_s'$. Moreover, if $f: s_1\times\ldots\times s_n\rightarrow s_{n+1}$ then $f_{\cal A}:{\cal A}_{s_1}\times\ldots\times {\cal A}_{s_n}\rightarrow {\cal A}_{s_{n+1}}$.

Definition 4.3 (Free Algebra)

Let $(({\cal S},\leq),\Sigma)$ be an order-sorted signature and X be an ${\cal S}$-indexed set of variable identifiers or merely variables i.e. $X = \bigcup_{s \in {\cal S} } X_s$ such that $X \cap \Sigma=\emptyset$. The free $\Sigma$-algebra over X is the pair $(T_\Sigma(X), F_\Sigma)$ where:

• The ${\cal S}$-indexed family $T_\Sigma(X)$ is defined as the least set that satisfies:
  • For all $x\in X_s$, $x\in (T_\Sigma(X))_s$.
  • For all $cte:\rightarrow s \in\Sigma$, $cte\in (T_\Sigma(X))_s$.
  • For all $f:s_1\times\ldots\times s_n\rightarrow s \in\Sigma$ and for all $(t_1,\ldots,t_n)\in ((T_\Sigma(X))_{s_1} \times\ldots\times (T_\Sigma(X))_{s_n})$, $f(t_1,\ldots,t_n)\in (T_\Sigma(X))_s$.
• The $\Sigma$-indexed set of functions $F_\Sigma$ is made of functions of the form $f_{T_\Sigma(X)}: ((T_\Sigma(X))_{s_1} \times\ldots\times (T_\Sigma(X))_{s_n})\rightarrow {T_\Sigma(X)}_{s}$ that take tuples of the form $(t_1,\ldots t_n)$ to $f(t_1,\ldots t_n)$.

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:

$$\begin{array} {lcll} 0 &:& & \rightarrow Nat\\ succ &:& N... ...ow Msg\\ key &:& Agt\times Agt & \rightarrow Key \end{array}$$

Definition 4.4 (Message Algebra)

Let ${\cal S}_M$ be the sort set $\{ Msg, Agt, Key, Nonce, Agt, Server, Nat \}$ and $\Sigma_M$ be the function symbol set $\{ e, c, key, nonce, agt, s, 0, succ\}$. Let $X_M$ be an ${\cal S}_M$-indexed family of message variables. We endow ${\cal S}_M$ with a partial order $\leq_M$ which stipulates that $Agt\leq_M Msg$, $Key\leq_M Msg$, $Nonce\leq_M Msg$, $Server\leq_M Agt$ and closed under reflexivity. We define the algebra of messages $T_{\Sigma_M}(X_M)$ as the free $\Sigma_M$-algebra over $X_M$. 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 $\mbox{$\langle {A,B,m} \rangle$}$ where A and B are principal identifiers, and m is a message. A triple $\mbox{$\langle {A,B,m} \rangle$}$ 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 $\mbox{$\langle {dir, m, P} \rangle$}$ where P is a principal identifier, m is a message and $dir\in\{!,?\}$. A triple $\mbox{$\langle {?,m,P} \rangle$}$ has to be read as: wait for receiving the message m from the principal P . A triple $\mbox{$\langle {!,m,P} \rangle$}$ 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, $Reduce(\{e(c(m,m_1),k_{as}), e(m_2,k_{ab}),k_{as}\})$ yields $\{m,m_1,e(m_2,k_{ab}),k_{as}\}$. 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, $Flat(\{e(c(m,m_1),k_{as}), e(m_2,k_{ab}),k_{as}\})$ yields $\{m,m_1,m_2,k_{as},k_{ab}\}$. 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 $\mbox{$\frac{\displaystyle {\{N_{a_1},X \}_{k_{as}}}}{\displaystyle {X} } $}$ and the set of fresh messages is $\{N_{a_1} , N_{a_2}, N_{a_3}\}$. Then, we compute $Flat(\{\{N_{a_1},X \}_{k_{as}},X\})\cap \{N_{a_1} , N_{a_2}, N_{a_3}\}=\{N_{a_1}, X\}\cap \{N_{a_1} , N_{a_2}, N_{a_3}\} =\{N_{a_1}\}$ and we put as side condition $Fresh(N_{a_1})$. Hence, the rule the complete rule is $\mbox{$\frac{\displaystyle {\{N_{a_1},X \}_{k_{as}}}}{\displaystyle {X} } $} Fresh(N_{a_1})$.

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 $B=\{(e(m,k),X)\}$, 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 Role1 which is initially $\mbox{$\langle {} \rangle$}$. Hence M=Glan(Role1) . 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 $Reduced(M \cup KI \cup Fresh)$. At this point, it is straightforward to see that those messages in $RM\backslash(KI \cup Fresh)$) 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 $KI(R)~ \cup~Fresh(R)$. 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