Study On Formal Analysis Of Security Protocol Based On Strand Space Model

With the popularization of network and Internet applications, security issues are becoming more and more important. Accordingly, security protocol, the most effective way to solve security issues, is of the same importance. But it is not an easy work to ensure the validity of security protocol in the sophisticated network environment, which has become an important research subject. Great efforts have been made by scientists to meet this challenge during the past 20 years, which in a sense shows the difficulty of security protocols analysis. Among all existing theories and methods, formal analysis is an outstanding one.The updated research fruit--Strand Space Model (SSM) brought forward by Fabrega, Herzog and Guttman is of the best prospect among varieties of formal analysis methods at large. It fully absorbs former researching results and uses a kind of order graph between its nodes existing casual relationship to demonstrate the action sequence of main body and intruder of the protocol and deduce the validity of the protocol by means of certification. It can prevent the bursting of status space and is practical, intuitive and strict for formal analysis of security protocol.This paper does a further study on the SSM, and then analyses numbers of security protocols based on it as follows:1. Yahalom protocolEstablish the SSM of Yahalom protocol and conduct the further discussion;2. A kind of authentication protocol based on a transmission modelWith SSM, we find out its dropper and create a new attack on this protocol and make some improvement;3. ISI payment protocolWe apply the SSM to the analysis of fairness of E-business protocol. Additionally, we study on proxy multi-signature scheme in basic theory and present a strengthened proxy multi-signature scheme.