Skip to main content
Log in

Study on strand space model theory

  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

The growing interest in the application of formal methods of cryptographic protocol analysis has led to the development of a number 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 entity authentication protocol is secure in strand space model (SSM) with some small extensions. 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 of formal inference in strand space model, some deficiencies in original SSM are pointed out. In order to 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, oracle strands, 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 then be used to further analyze the entity authentication protocol. This analysis sheds light on why this protocol would be vulnerable while it illustrates that GSSM not only can prove security protocol correct, but also can be efficiently used to construct protocol attacks. It is also pointed out that using other protocol to attack some given protocol is essentially the same as the case of using the most of protocol itself.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Lowe G. Breaking and fixing Needham-Schroeder public-key protocol using FDR.Lecture Notes in Computer Science 1055, Springer Verlag, 1996, pp.147–166.

    Google Scholar 

  2. Roscoe A W. Intensional specifications of security protocols. InProc. The 9th Computer Security Foundation Workshop, Kenmare, County Kerry, Ireland, 1996, pp.28–38.

  3. Schneider S A. Verifying authentication protocol in CSP.IEEE Trans. Software Engineering, September, 1998, 24(9): 741–758.

    Article  Google Scholar 

  4. Paulson L C. The inductive approach to verifying cryptographic protocols.Journal of Computer Security, 1999, (7): 85–122.

    Google Scholar 

  5. Focardi R, Ghelli A, Gorrieri R. Using noninterference for the analysis of security protocol. InProc. The DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997, http://dimacs. rutegers.edu/workshops/security/.

  6. Butler M. On the use of data refinement in the development of secure communications system. Technical Report DSSE-TR-2001-1, Declarative Systems and Software Engineering Group, University of Southampton, January 2001.

  7. F J Thayer Fabrega, J C Herzog, J D Guttman. Strand speces: Proving security protocols correct.Journal of Computer Security, 1999, (7): 191–230

    Google Scholar 

  8. Zhang Y, Li J, Xiao G. An approach to the formal verification of the two-party cryptographic protocols.Operating Systems Review, 1999, 33(4): 48–51.

    Article  Google Scholar 

  9. Bai Shuoet al. The verification logic for secure protocols.Journal of Software, 2000, 11(2): 213–221. (in Chinese)

    Google Scholar 

  10. Debbabi M, Mejri M, Tawbi N, Yahmadi I. A new algorithm for the automatic verification of authentication protocols: From specifications to flaws and attack scenarios. InProc. The DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997, http://dimacs.rutegers.edu/ workshops/security/.

  11. Tzeng W G, Hu C M. Inter-protocol interleaving attacks on some authentication and key distribution protocols.Information Processing Letters, 1999, (69): 297–302.

    Article  MATH  Google Scholar 

  12. Kelsey J, Schneier B, Wagner D. Protocol interactions and the chosen protocol attack. InProc. Security Protocols, 5th International Workshop, Spriger Verlage LNCS 1361, 1997, pp.91–104.

  13. Perrig A, Song D. Looking for diamonds in the desert-extending automatic protocol generation to three-party authentication and key agreement protocols. InProc. The 13th Computer Security Foundation Workshop, IEEE Computer Society Press, 2000, pp.64–76.

  14. Paulson L C. Relations between secrets: Two formal analyses of the Yahalom protocol. Technical Report 432. Computer Laboratory, University of Cambridge, July 1997.

  15. Song D. Athena: A new efficient automatic checker for security protocol analysis. InProc. The 12th Computer Security Foundation Workshop, Mordano, Italy, 1999, pp.192–202.

  16. Alello L C, Massacci F. An executable specification language for planning attacks to security protocol. InProc. The 13th Computer Security Foundation Workshop, Cambridge, England, 2000, pp.88–102.

  17. Boyd C. Towards extensional goals in authentication protocols. InProc. The DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997, http://dimacs.rutegers.edu/workshops/security/.

  18. Marrero W, Clarke E, Jha S. A model checker for authentication protocols. InProc. The DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997, http://dimacs.rutegers.edu/ workshops/security/.

  19. J D Guttman, F J Thayer Fabrega. Authentication tests. InProc. 2000 IEEE Symp. Security and Privacy, IEEE Computer Society Press, Berkeley, California, May 2000, pp.96–109.

    Chapter  Google Scholar 

  20. Clark J, Jacob J. A survey of authentication protocol literature: Version 1.0. Available at http://dcpul. cs.york.ac.uk/~jeremy, 1997.

  21. Burrows M, Abadi M, Needham M R. A logic of authentication. InProc. The Royal Society of London, 1989, 426: 233–271.

  22. Steve M Bellovin. Problem areas for the IP security protocols. InProc. The Sixth Usenix UNIX Security Symposium, San Jose, California, July 1996, pp.22–25.

  23. Bird R, Gopal I, Herzberg Aet al. Systematic design of a family of attack-resistant authentication protocols.IEEE Journal on Selected Areas in Communications, June 1993, 11(5).

  24. Heather J, Lowe G, Schneider S. How to prevent type flaw attacks on security protocol. InProc. 13th Computer Security Foundation Workshop, MIEEE Computer Society Press, Cambridge, England, 2000, pp.269–284.

    Google Scholar 

  25. Syverson P. A taxonomy of reply attacks. InProc. The 7th IEEE Computer Security Foundations Workshop, Franconia, USA, 1994, pp.131–136.

  26. Cervesato I, Durgin N, Mitchell Jet al. Relating strands and multiset rewriting for security protocol analysis, Revised extended abstract. InProc. The 13th Computer Security Foundation Workshop, Cambridge, England, 2000, pp.35–51.

  27. Wu W, Saito T, Mizoguchi F. Security of public key certificate based authentication protocol. InThird International Workshop on Practice and Theory in Public Key Cryptosystems, PKC2000, LNCS 1759, pp.196–209.

  28. Meadows C. Open issues in formal methods for cryptographic analysis. Available at http://www.itd.nrl. navy.mil/ITD/5540/publications/.

  29. F J Thayer Fabrega, J C Herzog, J D Guttman. Mixing protocols. InProc. The 12th IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, Mordano, Italy, June 1999, pp.72–82.

    Chapter  Google Scholar 

  30. Lowe G. A heirarchy of authentication specifications. InProc. The 10th Computer Security Foundation Workshop, Rockport, Massachusetts, USA, 1997, pp.31–43.

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Ji QingGuang.

Additional information

This work was supported by the National Key Basic Research Program of China under Grant No.G1999035810 and Grant No.G1999035802, the National Natural Science Foundation of China under Grant No.60083007, and the National Outstanding Youth Foundation of China under Grant No.60025205.

Ji QingGuang was born in 1968. He is a Ph.D. candidate of the Engineering Research Center of Information Security Technology, the Institute of Software, the Chinese Academy of Sciences. His research interests are formal analysis and formal design of the secure operating system, formal analysis of security protocols, and public key cryptography.

QING SiHan was born in 1939. He is a chief researcher in Engineering Research Center for Information Security Technology, Institute of Software, the Chinese Academy of Sciences and a supervisor of Ph.D. candidates. His research interests include theory and technology of network and information security, secure operating system, design and analysis of cryptographic protocols, intrusion detection system and etc.

ZHOU YongBin was born in 1973. He received his M.S. degree in computer science from Shandong University. Now he is a Ph.D. candidate in Institute of Software, the Chinese Academy of Sciences in 2000. His research interests include applied cryptography, theory and technology of network and information security, PKI and related e-commerce protocols.

FENG DengGuo was born in 1965. He is a research member and doctoral supervisor of the Institute of Software, the Chinese Academy of Sciences. His current research areas include information security and computer network security.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Ji, Q., Qing, S., Zhou, Y. et al. Study on strand space model theory. J. Comput. Sci. & Technol. 18, 553–570 (2003). https://doi.org/10.1007/BF02947115

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02947115

Keywords

Navigation