Validating the Use of BAN LOGIC

Most attacks against security protocols are due to their vulnerable designs. These type of protocols are usually the base which many other protocols and applications are built upon, so proving the correctness of such protocols has become a very important issue in recent years. At the same time, the complexity of security protocols has increased considerably, making it harder to perform an exhaustive analysis of the different situations they are able to deal with. BAN logic was created to assist in the validation of authentication protocols. Although there are other validation logics, we have chosen BAN because we believe its formal process is very simple and robust and therefore facilitates its application to validate old protocols such as Otway-Rees and more complex new ones such as IKE (standard Internet Key Exchange protocol). This paper is based on BAN logic. We will give a brief description of validating procedures and we will demonstrate the validity of BAN foundations, refuting some weaknesses detected by other authors.