The design of authentication protocols is notoriously error—prone．ISO has been working on a variety of authentication protocols standards for some years．This paper explores the approaches to formal analysis of authentication protocols using BAN logic and points out that the BAN logic analysis does not always lead to correct outcome．Finally，this paper discusses the design principles of authentication protocols and the future direc-tions for improvements of the BAN logic．