The reduced protocol is composed by the following three steps:
The protocol is modeled through two VSPA agents: the Initiator and the Responder. The Initiator accepts a user connection request, then starts the messages exchange with the Responder.
Protocol messages are all of the form:
where:
A user can make a connection request to
through action
request(a_id,b_id).
To inform users that the connection is established, the
Initiator and the Responder give as output
connection(a_id,b_id,ok) and
r_connection(b_id,a_id,ok), respectively. In the case of a protocol
failure the messages become:
connection(a_id,b_id,no) and r_connection(b_id,a_id,no),
respectively.
Another action is executed by Responder to inform users that someone
has made a connection request: r_running(a_id,b_id).
Initiator is defined using VSPA by:
Initiator receives, through action , a request from user a_id for a connection with
user dest_id; then it starts a run of the
protocol. It sends message 1 containing the sender identifier and its
nonce, both encrypted with receiver's public key. When it receives message 2
containing the two nonces
,dest_nonce encrypted
with the Initiator public key, it checks
if
is equal to the nonce sent in the first message
(
). If this is the case, it sends
the other nonce
to user
and informs the user
that the connection with
is established
(action connection(a_id,dest_id,ok)).
If the nonce
is different from
, the protocol
fails and this is notified through action
.
Similarly to Initiator, the Responder is defined in VSPA as follows:
Responder receives message 1, containing sender's nonce and identity
(send_nonce,).
It checks if the identifier contained
in the plaintext part of the message (send_id) is equal to that
contained in the ciphertext part. If it is so, it sends message 2 containing
the nonce received and its own nonce, encrypted with the sender public key.
It receives message 3 and checks if the nonce received is equal to its own;
if the check is successful it informs, through the action
, the user that the
connection is established, otherwise it gives
as output
which represent an
unsuccessful termination of the protocol. The complete protocol
specification is defined as parallel composition of the agents described
above:
where is the set of messages sent during the protocol.