Formal Analysis And Verification Of Composition Protocol Based On Model Checking

The security protocol is a highly interoperable protocol based on cryptography and is one of the important means to solve network security problems.Traditional informal method cannot comprehensively and accurately detect vulnerabilities in security protocol,while formal method,relying on the rigor of mathematics,can effectively analyze and verify protocol.In recent years,many formal analysis methods for security protocol have been proposed and applied,but most of them are based on the assumption of a single protocol for security analysis.However,in complex network communication,it is usually difficult to meet the assumption of a single protocol.Therefore,there is an urgent need for more methods to formally analyze the security of composition protocol.Model checking technology,as a formal method,has been used to verify the security of composition protocol in multi-protocol environments,but there are still disadvantages such as state explosion,high technical requirements,and limited application protocol scope.To address the above issues,this paper uses the model checker SPIN to verify the security of composition protocol.First,a formal analysis and verification method for composition protocol based on SPIN is proposed.Then a message specification strategy is proposed to alleviate the state explosion problem in protocol verification.Finally,SPIN is used to formally verify the NSB+NSL and APG3+ZF3 composition protocols.The main work and innovation points of this paper are as follows:(1)A formal analysis and verification method for composition protocol based on SPIN is proposed.The method abstracts protocol security properties as principal declaration events to characterize the properties of composition protocol and constructs a composition protocol semantic model suitable for SPIN modeling accordingly.The automated verification of the composition protocol is achieved by converting the semantic model and the attacker model into the Promela modeling language.This method provides important theoretical guidance for the formal verification of composition protocol based on SPIN.(2)A message specification strategy is proposed to alleviate the state explosion problem.Various methods for constructing intrusion messages in the Promela modeling process are analyzed,and considering the complex interaction of composition protocol,a hierarchical intrusion message construction strategy and a field detection and component recognition method are proposed.The objective is to mitigate the state explosion problem and enhance the generality of the model by optimizing the intruders’ message template selection strategy and message construction methods.(3)Formally define the intruder model based on the message specification strategy.The intruder model is formally defined based on the proposed message specification method,and the behavioral framework of the intruder is described in detail,including four behavioral algorithms and behavioral patterns.Through verification of a series of classical protocols,the results show that the model can effectively guide intruder modeling and improve protocol verification efficiency.(4)Verify the security of the NSL+NSB and APG3+ZF3 composition protocols using SPIN.The specific Promela modeling process of the composition protocol is described,and two known cross-protocol attacks are successfully discovered.The results show that the proposed method is effective for the formal verification of both simple composition protocol without multi-stage encryption and complex composition protocol with multi-stage encryption,and can provide reference for the verification of similar composition protocol using SPIN.