Role Extraction

Roles are protocol abstractions where the emphasis is put, for a specific role, on a particular principal. A role reflects the way some principal perceives the protocol messages. To understand the difference between roles and principals, let us take the following simple example: suppose that we have two principals $A_1$ and $A_2$ and suppose that the principal $A_1$ wishes to prove his identity to $A_2$, in this case the principal $A_1$ has to play the role A and the principal $A_2$ has to play the role B . However, if, later, the principal $A_2$ wishes to prove his identity to $A_1$, $A_2$ must play the A 's role and $A_1$ the B 's one. The reader should notice that throughout the rest of this paper roles and principals will be confused as far as ambiguity could be avoided.

For instance, in the case of the Woo and Lam protocol of Table 1, three roles could be extracted: A , B and S . The principal, playing the role A , participates in the protocol through three main steps: First, A sends his identity to the principal B . Second, he receives a nonce $N_b$ from B . Third, he sends the message $\{N_b\}_{k_{as}}$ to B . Hence, the role associated to A could be written as the following sequence of actions:

$$Role(A) = \mbox{$\langle {!, A, B} \rangle$} \mbox{$\langle... ... \rangle$} \mbox{$\langle {!, \{N_b\}_{k_{as}},B} \rangle$}$$

An action is a triple of the form $\mbox{$\langle {dir, m, P} \rangle$}$ where dir is a direction symbol (either ? meaning input or ! meaning output), m is a message and P is a principal identifier.

The principal playing role B participates in the protocol of Table 1 through five actions. First, he receives a principal identifier, say A . Second, he generates a fresh nonce, say $N_b$, and sends it to the agent A . Third, he receives from A the message $\{N_b\}_{k_{as}}$. Fourth, he sends to the server the message $\{ A, \{N_b\}_{k_{as}} \}_{k_{bs}}$. Fifth, he receives from the server the message $\{N_b\}_{k_{bs}}$. Accordingly, the corresponding role is:

$$\begin{array} {lcl} Role(B) & = & \mbox{$\langle {?, A, A} ... ...ox{$\langle {?, \{ N_b \}_{k_{bs}} , S} \rangle$} \end{array}$$

The principal playing the role of the server S participates in the protocol through two actions. First, he receives from B the message $\{ A, \{N_b\}_{k_{as}} \}_{k_{bs}}$. Second, he sends to B the message $\{N_b\}_{k_{bs}}$. Hence, the role of S is given by:

$$Role(S) = \mbox{$\langle {?, \{ A, \{N_b\}_{k_{as}} \}_{k_{b... ...angle$} \mbox{$\langle {!, \{ N_b \}_{k_{bs}} , B} \rangle$}$$

At that point, we are ready to present the second step of our algorithm i.e. the proof system generation.