[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Analysis of security protocols based on challenge-response

  • Published:
Science in China Series F: Information Sciences Aims and scope Submit manuscript

Abstract

Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the existing analysis methods, which either adopt theorem proving techniques such as state exploration or logic reasoning techniques such as authentication logic, face the conflicts between analysis power and operability. To solve the problem, a new efficient method is proposed that provides SSM semantics-based definition of secrecy and authentication goals and applies authentication logic as fundamental analysis techniques, in which secrecy analysis is split into two parts: Explicit-Information-Leakage and Implicit-Information-Leakage, and correspondence analysis is concluded as the analysis of the existence relationship of Strands and the agreement of Strand parameters. This new method owns both the power of the Strand Space Model and concision of authentication logic.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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. Dolev D, Yao A. On the security of public key protocols. IEEE Trans Inf Theory, 1983, 29(2): 198–208

    Article  MATH  MathSciNet  Google Scholar 

  2. Burrows M, Abadi M. A logic of authentication. ACM Trans Comput Syst, 1990, 8(1): 18–36

    Article  Google Scholar 

  3. Meadows C. A model of computation for the NRL protocol analyzer. In: Proceedings of Computer Security Foundations Workshop VII, Franconia, NH, USA, June 1994, 84–89

  4. Paulson L C. The inductive approach to verifying cryptographic protocols. J Comput Security, 1998, 6(1): 85–128

    Google Scholar 

  5. Fàbrega F J T, Herzog J C, Guttman J D. Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symp. on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998. 160–171

    Google Scholar 

  6. Fàbrega F J T, Herzog J C, Guttman J D. Strand spaces: Proving security protocols correct. J Comput Security, 1999, 7(2, 3): 191–230

    Google Scholar 

  7. Song D. Athena: A new efficient automatic checker for security protocol analysis. In: Proceedings of the 12th Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999. 192–202

    Chapter  Google Scholar 

  8. Song D, Berezin S, Perrig A. Athena: a novel approach to efficient automatic security protocol analysis. J Comput Security, 2001, 9(1): 47–74

    Google Scholar 

  9. Guttman J D, Fàbrega F J T. Authentication tests. In: Proceedings of 2000 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 2000. 96–109

    Chapter  Google Scholar 

  10. Guttman J D, Fàbrega F J T. Authentication tests and the structure of bundles. Theor Comput Sci, 2002, 283(2): 333–380

    Article  MATH  Google Scholar 

  11. Guttman J D. Security protocol design via authentication tests. In: Proceedings of the 2002 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2002. 92–103

    Google Scholar 

  12. Ji Q G, Qing S H, Zhou Y B, et al. Study on strand space model theory. J Comput Sci Tech, 2003, 18(5): 553–570

    Article  MATH  MathSciNet  Google Scholar 

  13. Syverson P. Towards a Strand semantics for authentication logic. Electron Notes in Theor Comput Sci, 1999, 20: 143–157

    Article  MathSciNet  Google Scholar 

  14. Cervesato I, Durgin N, Kanovich M, et al. Interpreting strands in linear logic. In: Veith H, Heintze N, Clark E, eds. Proceedings of the 2000 Workshop on Formal Methods and Computer Security. Chicago, 2000

  15. Yang M, Luo J Z. On the analysis of security protocols based on authentication tests. J Software (in Chinese), 2006, 17(1): 148–156

    MATH  MathSciNet  Google Scholar 

  16. Yang M, Luo J Z. Analysis of correspondence property for security protocols. J Commun (in Chinese), 2006, 27(7): 39–45

    MathSciNet  Google Scholar 

  17. Woo T Y C, Lam S S. A semantic model for authentication protocols. In: Proceedings of the 1993 IEEE Computer Society Symp. on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1993. 178–194

    Chapter  Google Scholar 

  18. Qing S H. A new non-repudiation protocol. J Software (in Chinese), 2000, 11(10): 1338–1343

    Google Scholar 

  19. Li X X, Huai J P. A fair non-repudiation cryptographic protocol and its formal analysis and applications. J Software (in Chinese), 2000, 11(12): 1628–1634

    Google Scholar 

  20. Hu C J, Zhen Y, Shen C X. Proving secrecy property of cryptographic protocols. Chin J Comput (in Chinese), 2003, 26(3): 367–372

    Google Scholar 

  21. Lowe G. A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1997. 31–43

    Google Scholar 

  22. Lai X J. Security requirements on authentication protocols using challenge-response. J Grad School Chin Acad Sci, 2002, 19(3): 246–253

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, Southeast University, Nanjing, 210096, China

    Luo JunZhou & Yang Ming

Authors
  1. Luo JunZhou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yang Ming
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luo JunZhou.

Additional information

Supported by the National Natural Science Foundation of China (Grant Nos. 90412014 and 90604004), Jiangsu Provincial Key Laboratory of Network and Information Security (Grant No. BM2003201), and Jiangsu Provincial High-Tech Research Program (Grant No. BG2004036)

Rights and permissions

Reprints and permissions

About this article

Cite this article

Luo, J., Yang, M. Analysis of security protocols based on challenge-response. SCI CHINA SER F 50, 137–153 (2007). https://doi.org/10.1007/s11432-007-0015-8

Download citation

  • Received:

  • Accepted:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11432-007-0015-8

Keywords