Based On Strand Space Model Of Security Protocol Analysis And Design Methods

Due to its open protocol, the Internet has revolutionized computer networks, but this revolution brings new risks and threats. The best way to protect computer networks is to prevent attackers from intruding, using fast automated procedures.This problem can be solved by using active security management, based on sharing information about attacks and cooperation between organizations. Secure Zone Cooperation, a framework that establishes mutual collaboration and cooperation between trusted zones, can protect systems and networks from potential attacks. In this powerful security architecture ,we need to establish security communication system to protect security information exchanged among each zone. Cipher algorithm and security protocol are its core. But it need much great price to attack a mature cipher algorithm than a defective security protocol. So the analysis and design for efficient security protocol is more important research problem in the field of computer communication.The fundament of many kinds of distributed system is security protocol,whose roles are distributing of key and Authentication.Once some flaws are found in it,the security of communication will be threatened seriously.There are a lot of security flaws in the design of many existed protocols. The technology of analyzing and checking for security protocols becomes the hot spot of research at present. But the present methods are mainly used to analyze security of some specific security protocol,not ensure the security just at the beginning of designing. So the usage of formal methods for design for security protocol has magnificent meaning ,especially for the requirement of some complex cipher protocol.In formal methods,security protocol analysis based on Strand Space Model can make use of exact causal relation information to make the prove of security properties very concise. Thayer has developed a method-called the "authentication test"method-that can be used by hand to verify cryptographic protocols.It can achieve authentication and recency by encryption and random number.At the same time,strand space and authentication can also be used to guide the protocol development process.Thayer said leading to new protocols by them is also possible.Through studying the approach of protocol analysis based on Strand Space Model,in the paper we put forward how to construct special-purpose protocols forspecific situations in secure communication or electronic commerce using authentication. And the process of design is the proved process for trusted subjects by strand space and authentication.We describe a protocol design process,and illustrate its use by creating ATSP(an Authentication Test-based Secure Protocol) . First,our exact design goals for ATSP are to provide authentication and pairwise confidentiality for certain values in a three-way protocol exchange.ATSP must also provide non-reprdiation guarantees.However,we give no attention to fairness. The design process is organized around the authentication tests,a method for protocol verification based on the strand space theory. The authentication tests dictate how randomly generated values such as nounces may be combined with encryption to achieve authentication and freshness. ATSP offers functionality and four kinds of security guarantees.To sum up,on the basis of strand space theory,by analyzing process towards special goals and design of outgoing authentication test,incoming authentication test and unsolicited authentication test,we achieve expected security goals.The process is concise.Meanwhile,the design process of protocol is also verification by strand space model.whether ATSP has done anything unnecessary can be seen by analysis of formal method.Thus the redundancy of protocol is decreased and the efficiency of communication is increased.