Research On The Techniques Based On Multi-set Rewriting For Analyzing The Secure Properties Of Cryptographic Protocols

Cryptographic protocols are the base of accomplishing sharing resources over the network which is a distributed system. Intruder can make use of the flaws brought by the protocol itself to attacking the distributed system. These attacks destroy the security of the network. So the security of cryptographic protocols is the key of security of network. The design and analysis of cryptographic protocols are notoriously complex and error prone. Cryptographic protocols may have potential flaws which are difficulty to detect, though they are designed cautiously. So the design and analysis of cryptographic protocols are the troubles of information security. Informal techniques were used to analyze cryptographic protocols previously, and they have been replaced by formal techniques nowadays. The main formal techniques can be classified into belief logic, model checking, and theorem proving.This paper studies a new kind of formal method for cryptographic protocols analysis, called MSR (Multiset rewriting) model. The model uses strongly typed multiset rewriting over firs order atomic formulas to express protocol actions and relies on a form of existential quantification to symbolically model the generation of fresh data. It is a precise and flexible framework for the specification of complex cryptographic protocols. The main works in this paper are listed as follows:1) MSR model based on MSR and some related theories are studied.2) Under the MSR framework, the definitions about secrecy and authentication are proposed3) Protocol model and intruder model is improved to solve the infinite state of intruder model.4) The analysis of NS protocol and Zhou-Gollmann protocol using the improved model is introduced. And these works proved the rationality of improved model.5) Maude is learned, and the MSR prototype is studied and the improvements of it are proposed.