Security analysis and improvement of Yahalom protocol

Logic-based formal analysis methods are the efficient methods for analyzing the security of cryptography protocols. The paper analyzes the security of the Yahalom protocol by employing the formal method SVO logic and finds that the protocol does not achieve the authentication goals. By modifying message format and adding handshake message, the paper also proposes a novel improved Yahalom protocol, which removes the limitations that the original Yahalom protocol cannot against the reply attack and the BAN-Yahalom protocol cannot resist impersonation attack. The analysis results of the improved Yahalom protocol reveal that the protocol completes the strong goals of identity authentication and key negotiation.