# Confirming understanding of security protocol modelled in Scyther

In university, I'm currently learning how to use Scyther to model security protocols. Currently I am trying to understand what is happening in an example protocol given to me which is:

# Key Establishment Protocol
#

usertype SessionKey;

protocol ke11(I,R,S)
{
role I
{
var Kir: SessionKey;

send_1(I,S, R);
recv_2(S,I,{Kir}k(I,S));

claim_I1(I,Running,R,Kir);

send_4(I,R,{I}Kir);
recv_5(R,I,{R}Kir);

claim_I3(I,Commit,R,Kir);
claim_I1(I,Secret,Kir);
}

role R
{
var Kir: SessionKey;

recv_3(S,R, (I,{Kir}k(R,S)));
recv_4(I,R,{I}Kir);

claim_R3(R,Running,I,Kir);

send_5(R,I,{R}Kir);

claim_R2(R,Commit,I,Kir);

claim_R1(R,Secret,Kir);
}

role S
{
fresh Kir : SessionKey;

recv_1(I,S, R);
send_2(S,I, {Kir}k(I,S));
send_3(S,R, I,{Kir}k(R,S));
}
}


This has also been given to me:

1. I → S : R
2. S → I : {Kir}k(I,S)
3. S → R : I,{Kir}k(R,S)
4. R → I : {I}Kir
5. I → R : {R}Kir


From my understanding:

1. I is sending S the value of R
2. S is sending I the encryption of Kir, which is encrypted using a shared symmetric key between I and S
3. S is sending R the encryption of Kir, which is encrypted using a shared symmetric key between R and S
4. I is sending R the value of I encrypted using Kir which it got from decrypting the value in 2 using the shared symmetric key
5. R is sending I the value of R encrypted using Kir which it got from decrypting the value in 3 using the shared symmetric key.

I'm not really sure if this is correct so could someone please comment on if my understanding is correct or not. Specifically, I don't really understand what is being sent when I have written that the value of I or R is being sent (I -> S:R).

Any comments would greatly be appreciated. Many thanks.

It looks mostly correct, but note that in step 3 that S is sending R the value I in plaintext, as well as the encryption of Kir.

It may help to think of I, R and S as Initiator, Responder and Server respectively. When the values I, R and S are transmitted, these are user identifiers that might be email addresses or IP addresses.

The protocol could then be described in English as:

1. Initiator contacts the server, asking the server to help set up a connection with the responder. To do this they provide Server with the responder’s ID.
2. Server generates a fresh session key called Kir, encrypts it with a pre-shared key known to both server and initiator, then sends it to initiator.
3. Server contacts the responder and provides responder with initiators ID and an encryption of the session key Kir using a pre-shared key known to both responder and server.
4. Responder recovers Kir from the information sent by the server. Responder then contacts initiator and authenticates themselves by sending an encryption of the initiator’s ID using Kir.
5. Initiator sends responder an encryption of responder’s ID using Kir.

The idea is that both responder and initiator know kir, but an adversary does not. They should also be confident that they are communicating with the user associated with the corresponding ID (assuming that the server behaves honestly).