A Limitation of BAN Logic Analysis on a Man-in-the-middle Attack

In recent years a lot of attention has been paid to the use of special logics to analyse cryptographic protocols, foremost among these being the BAN logic. These logics have been successful in finding weaknesses in various cryptographic protocols. With BAN logic analysis on a Station-to-Station (STS) protocol, the paper presents a limitation of BAN logic analysis on a Man-in-the-middle attack, which shows that it is easy for the BAN logic to approve protocols that are in practice unsound and the some enhancements of the BAN logic should be made or in some cases, the informal method will be required in some security protocol analysis like STS. An improved STS protocol against a man-in-the-middle attack is given in the paper.