An Improved NSSK Authentication Protocol and Its Formal Analysis

In order to ensure that the message is fresh, both the identity of the communication and the shared key in the session are reliable, while avoiding the defects of the old message retransmission attack and identity posing in the native NS protocol, the optimized protocol adopts the means by which the receiver communicates with the key distribution center, and add the sender's identity and the temporary values sent by the parties to the messages returned by the key distribution center. By using the modal logic BAN logic, this paper models the improved protocol, and defines the initial hypothesis set and the security target set. Based on this, the reasoning rule is used to prove that the improved protocol can ensure the authentication protocol is safe.