The function of formal analysis in the design of the authentication protocols is discussed ; Based on Needham-Schroeder protocol with shared key and Otw ay-Rees protocol, an improvement is presented and then analyze it using BAN logic, according to the result of fo rmal analysis, an attack mode to the protocol is show and point out that formal analysis is helpful for the desig n of protocol ;at the end besides the actions of the logical analysis, the limi tatio ns and the directions fo r further improvement are discussed .