Matrix Model For Strand Space Theory

With the popularity of network applications, security protocols are used in every corner of production and life. Security protocols ensure that communication is safe enough in the open network environment by applying the cryptographic techniques. So the security attributes of security protocol itself, get more and more people’s attention. With the continuous expansion of the field of security, the security protocol gradually spread to various levels, which result in the structure of security protocol becoming increasingly complex. These require the formal analysis techniques must keep up with the pace of the times. So how to design a security protocol and how to test its security attribute, has become one of the most important topics in the research areas of security protocols.In the past20years, formal analysis of security protocols has provided a relatively perfect methods and systems, but still extensive analysis completed by the artificial, which makes analysis inefficient and prone to defects. The strand space model theory converts each state and the overall steps of the security protocol into the form of set and directed graphs. And define protocol running properties as various states in the partial order relation set. So we can determine whether exist the attack nodes by defining and proving the least element in the collection. But so far, the previous theoretical models of the string space still apply only to analysis by human and they are unsuitable done automatically by a computer.Fully absorbed the results of previous studies, this paper selected the strand space model for the study and proposed the concept of security protocols strand space matrix model. First, the paper describes the security protocols and basic theory of protocol formal analysis, basic concepts and progress in research. And then do a more detailed exposition of strand space model theory. At last the paper fully elaborate the strand space matrix model by strictly giving the relevant concepts, theories and methods.The strand space matrix model this paper proposed is more intuitive and simple than any other security protocol analysis model. It turns the process of security protocols analysis into the generation, transformation, and judgment of the matrix. So it is easily done automatically by a computer.