The protocol can be specified as follows in security protocol notation, where Alice is authenticating herself to Bob using a server S (M is a session-identifier, NA and NB are nonces): Note: The above steps do not authenticate B to A.
This is one of the protocols analysed by Burrows, Abadi and Needham in the paper[2] that introduced an early version of Burrows–Abadi–Needham logic.
These attacks leave the intruder with the session key and may exclude one of the parties from the conversation.
Boyd and Mao[4] observe that the original description does not require that S check the plaintext A and B to be the same as the A and B in the two ciphertexts.
In the absence of any check to prevent it, M (or perhaps M,A,B) becomes the session key between A and B and is known to the intruder.
One problem with this protocol is that a malicious intruder can arrange for A and B to end up with different keys.