Improved Otway Rees protocol and its formal verification

Authentication protocol is applied to implement the identity authentication of two communicating entities and build secure communication tunnel through exchanging keys. The paper analyzes the security properties of the original Otway Rees protocol and its existing improved version, it finds that the protocol cannot meet the authentication goals. The paper proposes a novel improved protocol, which eliminates redundancy in the Otway Rees protocol messages and removes the limitations that the Otway Rees protocol cannot resist impersonation attack by modifying message format and adding handshake message. The paper also verifies the security of the improved Otway Rees protocol by utilizing formal method. The analysis results show that the protocol satisfies the strong goals of identity authentication and key distribution.