Research On Analysis And Design Of Cryptographic Protocols Based On Generalized Strand Space Model

This dissertation mainly studies attacker of Dolev-Yao model,constructing attack based on generalized strand space model and design of cryptographic protocols,and together, our research focuses on three parts.The first part is extensions to Dolev-Yao model and its applications;The second part is generalization to constructing attack based on generalized strand space model;The third part is to apply generalized constructing attack method to guide design of cryptographic protocols.Reseach results of the first part is as follows:It is very necessary to extend original theory of strand spaces so that it can be applied to ananlyze real world protocols;The penetrator's strands are extended through adding initiative signature,initiative signature verfication,HMAC(keyed-hashing for message authentication code) and generating fresh random value traces to Dolev-Yao model;A new notion of ideal is defined and the relevant propositions or theorems are therefore modified and proved;Taking TLS protocol for example, strand space model and theory extended are used to find an attack.In order to avoid the kind of attack, a piece of strategy to be paid attention to is put forward when cryptographic protocols are designed.Reseach results of the second part is as follows:Taking Needham-Schroeder protocol for example, usage of constructing attack is illuminated based on generalized strand space model;During ananlyzing Needham-Schroeder protocol using this method, though the known middle-in-man attack is found, the hidden type-flaw attack can not be found;So, flaws lie in constructing attack based on generalized strand space model.After this method is ananlyzed carefully, the flaws are found out, and corresponding amendatory measures are brought forward;In order to verify amendatory constructing attack based on generalized strand space model effective,an artificial protocol is put forward,which is similar to "ffgg" protocol constructed by Millen,that is to say, the two protocols have cryptographic property in common(After "ffgg" protocol is ananlyzed by Millen using Pulson's inductive approach, it is secure); Amendatory constructing attack is more effective than Pulson's inductive approach in finding flaws of cryptographic protocols.In fact,it is not secure, after "ffgg~" protocol is analyzed by using the amendatory constructing attack method based on generalized strand space model,and there is a parallel attack in "ffgg~" protocol.Moreover, it is easily proved that "ffgg" protocol is not secure by using he amendatory constructing attack method.Reseach results of the third part is as follows:Fundamental principle is summarized which is followed when we design cryptographic protocols.Taking Needham-Schroeder-Lowe for example,this dissertation explains to how to apply amendatory constructing attack based on generalized strand space model to guide design of cryptographic protocols,and put forward general course we should follow when cryptographic protocols are designed according to this amendatory method.