The growing interest in the application of formal methods of cryptographic pro-tocol analysis has led to the development of a number of different ways for analyzing protocol. Inthis paper, it is strictly proved that i...The growing interest in the application of formal methods of cryptographic pro-tocol analysis has led to the development of a number of different ways for analyzing protocol. Inthis paper, it is strictly proved that if for any strand, there exists at least one bundle containingit, then an entity authentication protocol is secure in strand space model (SSM) with some smallextensions. Unfortunately, the results of attack scenario demonstrate that this protocol and the Yahalom protocol and its modification are de facto insecure. By analyzing the reasons of failure offormal inference in strand space model, some deficiencies in original SSM are pointed out. In orderto break through these limitations of analytic capability of SSM, the generalized strand space model(GSSM) induced by some protocol is proposed. In this model, some new classes of strands, oraclestrands, high order oracle strands etc., are developed, and some notions are formalized strictly in GSSM, such as protocol attacks, valid protocol run and successful protocol run. GSSM can thenbe used to further analyze the entity authentication protocol. This analysis sheds light on why thisprotocol would be vulnerable while it illustrates that GSSM not only can prove security protocolcorrect, but also can be efficiently used to construct protocol attacks. It is also pointed out thatusing other protocol to attack some given protocol is essentially the same as the case of using themost of protocol itself.展开更多
基金National Key Basic Research Program of China under，国家自然科学基金，国家杰出青年科学基金
文摘The growing interest in the application of formal methods of cryptographic pro-tocol analysis has led to the development of a number of different ways for analyzing protocol. Inthis paper, it is strictly proved that if for any strand, there exists at least one bundle containingit, then an entity authentication protocol is secure in strand space model (SSM) with some smallextensions. Unfortunately, the results of attack scenario demonstrate that this protocol and the Yahalom protocol and its modification are de facto insecure. By analyzing the reasons of failure offormal inference in strand space model, some deficiencies in original SSM are pointed out. In orderto break through these limitations of analytic capability of SSM, the generalized strand space model(GSSM) induced by some protocol is proposed. In this model, some new classes of strands, oraclestrands, high order oracle strands etc., are developed, and some notions are formalized strictly in GSSM, such as protocol attacks, valid protocol run and successful protocol run. GSSM can thenbe used to further analyze the entity authentication protocol. This analysis sheds light on why thisprotocol would be vulnerable while it illustrates that GSSM not only can prove security protocolcorrect, but also can be efficiently used to construct protocol attacks. It is also pointed out thatusing other protocol to attack some given protocol is essentially the same as the case of using themost of protocol itself.
