Confirming understanding of security protocol modelled in Scyther

hasin

1/11/24, 9:06 PM

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:

I is sending S the value of R
S is sending I the encryption of Kir, which is encrypted using a shared symmetric key between I and S
S is sending R the encryption of Kir, which is encrypted using a shared symmetric key between R and S
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
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.

1 + 0

symmetric

protocol-analysis

adversarial-model

Score:1

Crypto

Daniel S

1/11/24, 10:33 PM

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:

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.
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.
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.
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.
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).

+ 0

Elon Musk

I sit in a Tesla and translated this thread with Ai:

EN: Confirming understanding of security protocol modelled in Scyther

Post an answer

Most people don’t grasp that asking a lot of questions unlocks learning and improves interpersonal bonding. In Alison’s studies, for example, though people could accurately recall how many questions had been asked in their conversations, they didn’t intuit the link between questions and liking. Across four studies, in which participants were engaged in conversations themselves or read transcripts of others’ conversations, people tended not to realize that question asking would influence—or had influenced—the level of amity between the conversationalists.