The Formal Modeling Of Network Protocols And Discovery Of Attacks Based On Model Checking

With the gradual progress of the era of information, communication services areundergoing rapid changed. As the key factor in the communication services, thesecurity and reliability of network protocols can directly impact the whole networktremendously. And the vulnerabilities and flaws provide a potential opportunity formalicious users or attackers to attack the network. In order to systematically analyzethe security of network protocols, provide the guarantee of security in the primaryphase of network protocols development and reduce the risk of attacks, The paperpropose a systematical methodology of modeling network protocols using formalmethod and detecting attacks by model checking.Formal methods and model checking technique is very popular in the field ofsecurity analysis. The paper mainly focus on security properties, which networkprotocols should satisfy, and propose an approach to model network protocols thenfinally use model checking to verify these properties. We firstly extends the CSP#language and model in respects of messages encapsulation, process broadcast,system clock and security library. Then we build the basic model for networkprotocols; Then build the adversary model for network protocols and define theknowledge set and behaviors of the adversary; Specify the security objectives anduse Linear Temporal Logic, etc. to express the security properties; Summarizediscovered attack cases and build the attacker model for generating the adversaryprocesses automatically; The security properties will be verifies by model checkingtechnique, afterwards find the existing flaws in network protocols and increasesecurity-coefficient of network products.The paper details the whole process of security analysis in case study andanalyzes experiment results carefully. At last the result show our method is usefuland efficient in the security analysis of network protocols and it can detect potentialattacks and improve security of whole network.