The Formal Analysis Of Security Protocols Based On Maude

Networks provide a variety of convenience for people, but it brings about some serious security problems at the same time. The security protocols can assure people engage in various online transaction activities. Security protocols usually contains several flows due to the complication of the distributed networks system. In this thesis, the analysis of security of security protocols using the formal method based Maude has been proposed.According to the message form of security protocols and Dolev-Yao intruder model, all the elements of security protocols can be defined by the Maude functional Modules, the implementation of protocols and the ability of the intruder can be represented by the Maude rewriting rules. The Maude engine will explore the state space from the initial state until it reaches the final state or satisfies the given conditions. By the facility of the reachability analysis in Maude(implemented as search), each property of the protocols can be checked simultaneously when a model is generated. The result of searching will give a counterexample in the event that the protocol has defects, otherwise return no solutions.The main contributions of this thesis are as follows:·Introduce the basic knowledge of the Maude engine, detailedly describe the functional modules and system modules in Core Maude and rewriting rules in Maude.·The formal analysis of IKEv2 protocol which is designed to perform key exchange and mutual authentication and SHARE protocol are modeled and analyzed in Maude. The secrecy and authentication of security protocol are checked with the Maude search command. The attacking paths of the flawed protocols are listed and analyzed.