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.
- $A\rightarrow B:E_k^1(R)$
- $B\rightarrow A:E_A^2(S)$
- $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:
- Provide mutual authentication of both entities
- Provide a new secure shared key, unknown to any third party
- 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.