Is this hypothetical key-exchange secure?

I've thought about the following (generic) key-agreement protocol.
The only weaknesses I could have found are missing freshness guaranteees.

As for the notions:
$E^1_K(P)$ is the symmetric encryption of plaintext $P$ using key $K$. This is AES-GCM for example.
$E^2_A(P)$ can either denote symmetric encryption (e.g. AES-GCM) of $P$ using the (pre-shared) key of $A$ or it can denote asymmetric encryption of $P$ using the public key of $A$, the scheme is for example ECIES or RSA-OAEP. Certificates must be provided in the first two steps if asymmetric encryption is used.
$k$ is a random 128/256 bit AES key which is chosen by A prior to the first message and not disclosed until message 3.

1. $A\rightarrow B:E_k^1(R)$
2. $B\rightarrow A:E_A^2(S)$
3. $A\rightarrow B:E_B^2(k)$

The derived key is $MS=H(R||S)$ with $H$ being a KBKDF. $R$ and $S$ are 128 to 256 bit secure random values, generated by a CSPRNG.

Now for the aims of the protocol:

1. Provide mutual authentication of both entities
2. Provide a new secure shared key, unknown to any third party
3. Disable any party to manipulate the derived key to have some special property

A quick design rationale:
The first message ensures that assumption (3) is hold, B can't choose his random value dependant on As and A can't change it. The symmetric / asymmetric encryption should ensure (2). The usage of IND-CCA2 / AEAD primitives should ensure (3) as well. The usage of the PSK / certificates should ensure (1), as only they can successfully authenticate the messages.

I know, nothing is secure without a formal proof.

So my question:
Is the above protocol likely to be secure?

By the way: The protocol won't be deployed. This is a question about (general) protocol design.

• What is small k? Is it a pre-shared key between A and B? Jul 15 '15 at 8:23
• In the message flow, you use small k in the first message, where I would think it might mean a pre-shared key. In the third message, you encrypt k, which suggests it is something else. Jul 15 '15 at 8:39
• @user4621 $k$ is a random 256-bit AES key chosen by A prior to the first message.
– SEJPM
Jul 15 '15 at 11:13
• You are assuming that it's not possible to come up with a ciphertext $C$ and find pairs $(M_1,K_1)$, $(M_2,K_2)$, and so on such that $E_{K_1}(M_1)=E_{K_2}(M_2)=C$. This actually typically is possible, and this therefore means that (3) does not hold. What you actually want in step 1 instead is a secure commitment to $R$. Jul 15 '15 at 17:39
• @YehudaLindell, so if such a pair was found this would enable an active attacker to alter the agreed keys? Because this should be detected by decryption failure after message 3 (authenticated encryption is used). Or do you mean this would enable A to choose arbitrary Rs (which he always can...)? Or did you mean that this would enable A to send a fraudelent k decrypting to something completely else? This would be caught by authenticated encryption as well.
– SEJPM
Jul 15 '15 at 21:02

This is exactly where automatic protocol analysis tools can help you. For example, using the Scyther tool, the protocol description using symmetric encryption is:

/*
* Protocol description for Scyther
*
* Note we use 'K' to model 'k' since Scyther assumes 'k(.,.)' refers
* to pre-shared keys between two agents.
*/

// The protocol description with E^2 instantiated as symmetric
// encryption

hashfunction H;

macro msg1 = { R }K ;
macro msg2 = { S }k(A,B) ;
macro msg3 = { K }k(A,B) ;
macro sessionkey = H(R,S);

protocol testSymmetric(A,B)
{
role A
{
fresh R: Nonce;
fresh K: Nonce;
var S: Nonce;

send_1(A,B, msg1 );
recv_2(B,A, msg2 );
claim(A,Running,B,R,S);
send_3(A,B, msg3 );

claim(A,Secret,sessionkey);
claim(A,Alive);
claim(A,Weakagree);
claim(A,Commit,B,R,S);
claim(A,Niagree);
}

role B
{
var R: Nonce;
var K: Nonce;
fresh S: Nonce;

recv_1(A,B, msg1 );
claim(B,Running,A,R,S);
send_2(B,A, msg2 );
recv_3(A,B, msg3 );

claim(B,Secret,sessionkey);
claim(B,Alive);
claim(B,Weakagree);
claim(B,Commit,A,R,S);
claim(B,Niagree);
}
}

If you run this through the Scyther tool, you will find the key is secret, but agreement fails: an attacker can, for example, replace the random value in the first message by anything, causing B never to compute the key, but A still finishes and might think B now agrees on the values. Thus, the protocol does not give you any decent authentication, but the partner is supposedly alive. This is what Scyther shows you: If you modify the message macros for the asymmetric version, i.e.,

macro msg1 = { R }K ;
macro msg2 = { S }pk(A) ;
macro msg3 = { K }pk(B) ;

then the situation is much worse. Although the key is still secret, even the most basic authentication notion fails: along the lines of the previous attack, the attacker can complete a run with B without A ever being present. A slightly more interesting attack is one on the A role (where the intended partner Bob is never alive): In this case, the attacker just reroutes the messages and A thinks B is alive but completed the protocol with Charlie.

If you use the compromising adversaries version of Scyther you can also analyse KCI, UKS, and (w)PFS attacks, which will probably yield interesting results.

• That why one should never roll their own protocols :) The issues could be mitigated by introducting some sort of key confirmation? (in both cases)
– SEJPM
Jul 16 '15 at 16:21