The Verification Of Security Protocol Based On GSPM And The Inplementation Of The Tool

It is a key problem whether a security protocol reaches the designed security criteria since network technologies develop rapidly. Formal methods and automated tools are very important techniques to guarantee the security properties and the application requirements. GSPM (Generic Security Protocol Model) is such a method. This dissertation investigates the properties of security protocol based upon GSPM.Firstly, as type attack flaws affect the types of the messages; the type pattern rule designed in GSPM is too strict to solve type attack flaws. So a new semantic type attack has been added into the model, which makes GSPM strong enough to detect this flaw.Secondly, we design some algorithms to analyze the security protocol based on GSPM, including message deducing algorithm, message match algorithm and state-search algorithm. LTL (Linear Temporal Logic) is introduced to denote the property of security protocol, like confidentiality and authentication. A verification algorithm is designed due to the characteristic of LTL.Finally, this dissertation presents the implementation of an automatic verification tool based on GSPM and the algorithms mentioned above. The tool receives protocols and security objectives as input and automatically translates them into GSPM syntax to apply specific checking rules. This dissertation gives an analysis of the result and performance. It also shows the using flow of the tool.