Abstract: Investigations into the problem how to implement safe communication in the network and also into the problem emerged from symmetric key algorithm were made. And two kinds of practical authentication protocols, Point to Point Simple Authentication Protocol and Trusted Third Party Simple Authentication Protocol, were designed based on the characteristics of the network security. And we also have analysed the security of the two protocols to make sure that both of them have achieved the purpose of keyoriented, key affirmation and the aim of trusting the key of its peer via the formal analysis method (the mode logic method based on knowledge and belief consequence--SVO logic).

Key words: authentication protocol, formal analysis, SVO logic