Abstract: The security protocols are the basis of modern network communication, and the issue of proving the security of protocols is one of the current research hotspots. The logic of events theory (LoET) is a formal method for proving the security properties of protocols based on event system. Using the language of event orderings and event classes, and using a type of atoms to represent unguessable data, such as nonces, keys, etc., the protocol system is characterized effectively. Aimed at the security problem of the improved Helsinki protocol, predicate Fresh, FirstSend and their rules were extended in LoET, and the extended logic was used to analyze the protocol formally. Basic sequence of the protocol was constructed, and the authentication and secrecy of the protocol were formalized by LoET. The axiom system and rules were used to prove that the improved Helsinki protocol satisfied authentication and secrecy. The results show the effectiveness of LoET for proving the properties of authentication and secrecy.