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

Abstract

In recent years a lot of attention has been paid to the use of special logics to analyse cryptographic protocols, \u00a0foremost \u00a0among \u00a0these \u00a0being \u00a0the \u00a0BAN \u00a0logic. \u00a0These \u00a0logics \u00a0have \u00a0been \u00a0successful \u00a0in \u00a0finding weaknesses \u00a0in \u00a0various \u00a0cryptographic \u00a0protocols. \u00a0With \u00a0BAN \u00a0logic \u00a0analysis \u00a0on \u00a0a \u00a0Station-to-Station \u00a0(STS) protocol, the paper presents a limitation of BAN logic analysis on a Man-in-the-middle attack, which shows that \u00a0it \u00a0is \u00a0easy \u00a0for \u00a0the \u00a0BAN \u00a0logic \u00a0to \u00a0approve \u00a0protocols \u00a0that \u00a0are \u00a0in \u00a0practice \u00a0unsound \u00a0and \u00a0the \u00a0some 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.