Abstract:The paper first introduces the main ideas of the algorithm Gastin.P proposes,and then gives an informal analysis on the well-known Needham-Schroeder public-key authentication protocol,whose result demonstrates that it is very effective for using the algor