String Space Method For Analysis Of Security Protocols

With the ceaselessly development of network, the security of network information becomes more and more important; as the foundation of the security of network information, the security of cryptographic protocols becomes the key of this problem. Security scientists have exploited many methods and theories of formal method for this difficult problem in past 20 years. This paper makes a summary of seurity of protocols and formal method in chapter 2.Strand Space, brought forward by Fabrega, Herzog and Guttman, is a applied, intuitionistic and strict formal method for security protocols analysis. Strand Space including a partial order describing causal structure and a analog recursion method, brought forward the boundary of the attacker's capacity which does not depend on idiographic protocols.This paper makes an extension to the model of Strand Space in theorem. whereas the HASH function in key agreement protocol, using the honest function, we expansion the capacity of the eavesdropper and the correlative theories in Strand Space. Given the strand space of WTLS from the simplified model in§4.2.2, combining the concept of Ideal and Honest function, we analysed the security and authentication of WTLS, and pointed out a limitation of the mend of Paulson's weaker theorem about TLS's main secret.Modeling Yahalom protocol-creating and putting out share secret bases on symmetry cryptography- in strand space, the security of this protocol is proved by a convenient method which founds on strand space theory. Finally, herein this authentication method, we give some advices in cryptographic protocols design.