Study on Strand Space Model Theory

The growing interest in the application of formal methodsof cryptographic protocol analysis has led to the development of anumber of different ways for analyzing protocol. In this paper,it is strictly proved that if for any strand,there exists at least one bundle containing it, then an entityauthentication protocol is secure in strand space model (SSM) with somesmall extensions. Unfortunately, the results of attack scenariodemonstrate that this protocol and the Yahalom protocol and itsmodification are de facto insecure. By analyzing the reasons of failureof formal inference in strand space model, some deficiencies in originalSSM are pointed out. In order to break through these limitations ofanalytic capability of SSM, the generalized strand spacemodel (GSSM) induced by some protocol is proposed. In thismodel, some new classes of strands, oracle strands, high orderoracle strands etc., are developed, and some notions areformalized strictly in GSSM, such as protocol attacks, validprotocol run and successful protocol run. GSSM can then be used tofurther analyze the entity authentication protocol. Thisanalysis sheds light on why this protocol would be vulnerablewhile it illustrates that GSSM not only can prove securityprotocol correct, but also can be efficiently used to constructprotocol attacks. It is also pointed out that using otherprotocol to attack some given protocol is essentially the same asthe case of using the most of protocol itself.