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 and
and suppose that the principal
wishes to prove his identity to
, in this case the
principal
has to play the role A and the principal
has to play the role B . However, if, later, the
principal
wishes to prove his identity to
,
must play the A 's role and
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
from B . Third, he sends the message
to B . Hence, the role associated to A could
be written as the following sequence of actions:
An action is a triple of the form 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
, and sends it to the agent A . Third, he receives from
A the message
. Fourth, he sends to the
server the message
. Fifth, he receives from the server the message
. Accordingly, the corresponding role is:
The principal playing the role of the server S participates
in the protocol through two actions. First, he receives from
B the message . Second,
he sends to B the message
. Hence, the
role of S is given by:
At that point, we are ready to present the second step of our algorithm i.e. the proof system generation.