Popis: |
With the wide application of digital control technology in the nuclear safety control system, cyber security has gradually become an important part of system operation security. Replay attacks are a common form of cyber attack, this attack can bypass software encryption, signatures and other safeguards against information leaks to disguise identity or inject information. This paper describes a formal method to verify the ability of the protocol to resist replay attacks. This method need analyze the network protocol communication process, determine the elements to resist replay attack in the protocol, use formal language to establish the model of attack for the protocol, traverse all states by formal tools, check whether there is a design flaw in the protocol and demonstrate the process and path of replay attack so that protocol designers identify the weaknesses of defensive measures. |