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:
A user can make a connection request to through action
To inform users that the connection is established, the
Initiator and the Responder give as output
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),
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.