(1) Alice → Bob : g^x (2) Alice ← Bob : g^y, E_K(S_B(g^y, g^x)) (3) Alice → Bob : E_K(S_A(g^x, g^y))
I know there should be something I'm missing, but I cannot think of why E_K(...) is used. Isn't the signature sufficient? Even if there was a MITM, having S_B(...) or S_A(...) isn't very useful. What am I missing here?