On The Formal Description And Analysis Of Security Protocols Using Colored Petri Nets

With the continuous development of wireless sensor network(WSN)and industrial control network(ICN),emerging areas in cyberspace are produced with a more complex communication mechanism.As one of the key technologies for the protection of data and service resources in various emerging fields,security protocols have received widespread attention in recent years.The explosion in the number of security protocols,the differences in the operating environments of the protocols,the increase in the complexity of the protocols,and the closeness of subjective design and analysis with involved analysts have made the specification and verification of security protocols a challenging task.The formal analysis method of security protocols has made great progress in recent years.Some influential representation methods have arisen in several major branches including modal logic,theorem proving and model checking.Correspondingly,methods based on computational complexity of computing models are also developing simultaneously.This method has rigorous mathematical theory as a support,which makes it a demanding work for the researchers to use.Moreover,different results may obtained due to the different understanding of analysts when analyzing the same protocol.Compared with the computational complexity method,thanks to its symbolic and discrete nature,the formal analysis method based on the symbolic model has a simpler and clearer structure and has an inherent advantage in combination with the field of distributed computer engineering.Nowadays,with the growing of the number of security protocols in the industry,the automatic analysis of the protocol is bound to be an inevitable trend in the specification and verification of security protocols.Colored Petri Net is one of the most important tools in the analysis of distributed and asynchronous concurrent systems with both a clear structure and a rigorous mathematical foundation by the characteristics of duality,graph,and algebraic representation.Besides,its assistant computer tool integrates the functions of automated state space analysis,which can be utilized to analyze security protocols with additional modifications.This thesis makes use of its advantages in system modeling,and proposes a security protocol analysis method combining temporal logic and Dolev-Yao model.This method starts with the construction of the attacker model,introduces message inference rules and finally formsthe theory of using the colored petri net modeling to analyze the protocol security under the Dolev-Yao model.In addition,a security protocol analysis prototype system is also implemented based on CPN Tools combining the above theoretical method.By comparison with AVISPA,the leading security protocol automation analysis tool,the practicability of the proposed method is proved,and most security protocols can be analyzed with extended attacker models.