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.


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