Skip to main content
SpringerLink
Log in

A Dictionary Sequence Model to Analyze the Security of Protocol Implementations at the Source Code Level

  • Conference paper
  • First Online:
Trusted Computing and Information Security (CTCIS 2017)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 704))

Included in the following conference series:

  • 651 Accesses

Abstract

It is one of most important parts in the field of information security to set up models for the security analysis of cryptographic protocols, especially for the security analysis of cryptographic protocol implementations at the source code level. On the base of the dictionary sequence, a model is set up in this paper, aimed at the security analysis of cryptographic protocol implementations at the source code level. It is a new way to evaluate whether protocols are secure or not through the change of the sequences of function returning values in the process of the implementation at the source code level. Based on the new model, an experiment is carried out. It is shown in the experiment that our new model has advantage over previous models. Our new model will be helpful for designing and evaluating cryptographic protocol implementations at the source code level.

This work is supported by the State Key Program of National Natural Science of China (No. 61332019), and the National Basic Research Program (973 Program) of China (No. 2014CB340601).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Zhang, H.G., Han, W.B., Lai, X.J., et al.: Survey on cyberspace security. Sci. China Inf. Sci. 58(11), 1–43 (2015)

    MathSciNet  Google Scholar 

  2. Zheng, H., Qin, J., Jiankun, H., Qianhong, W.: Threshold attribute-based signcryption and its application to authenticated key agreement. Secur. Commun. Netw. 9, 4914–4923 (2016)

    Article  Google Scholar 

  3. Zhao, S., Xi, L., Zhang, Q., Qin, Y., Feng, D.: Security analysis of SM2 key exchange protocol in TPM2.0. Secur. Commun. Netw. 8, 383–395 (2015)

    Article  Google Scholar 

  4. Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Sci. Comput. Progr. 58(1–2), 3–27 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  5. Blanchet, B.: A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, Oakland, California, pp. 140–154, May 2006

    Google Scholar 

  6. Bhargavan, K., Fournet, C., Corin, R.J., Zalinescu, E.: Cryptographically verified implementations for TLS. In: Ning, P., Syverson, P.F., Jha, S. (eds.) 15th ACM Conference on Computer and Communications Security (ACM CCS 2008), Alexandria, USA, pp. 459–468. ACM, New York (2008)

    Google Scholar 

  7. Bhargavan, K., Fournet, C., Gordon, A.D.: Modular verification of security protocol code by typing. In: Hermenegildo, M.V., Palsberg, J. (eds.) 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), Madrid, Spain, pp. 445–456. ACM, New York (2010)

    Google Scholar 

  8. Aizatulin, M., Gordon, A.D., Jürjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: Chen, Y., Danezis, G., Shmatikov, V. (eds.) 18th ACM Conference on Computer and Communications Security (ACM CCS 2011), Chicago, USA, pp. 331–340. ACM, New York (2011)

    Google Scholar 

  9. Sprenger, C., Basin, D.A.: Refining key establishment. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium (CSF 2012), Cambridge, USA, pp. 230–246 (2012)

    Google Scholar 

  10. Backes, M., Maffei, M., Unruh, D.: Computationally sound verification of source code. In: CCS 2010, 4–8 October 2010

    Google Scholar 

  11. Avalle, M., Pironti, A., Sisto, R.: Formal verification of security protocol implementations: a survey. Formal Aspects Comput. 26(1), 99–123 (2014)

    Article  Google Scholar 

  12. Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363–379. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_24

    Chapter  Google Scholar 

  13. Dupressoir, F., Gordon, A.D., Jürjens, J., Naumann, D.A.: Guiding a general-purpose C verifier to prove cryptographic protocols. J. Comput. Secur. 22(5), 823–866 (2014)

    Article  Google Scholar 

  14. Tang, C., Lu, Z., Feng, C.: A verification logic for security protocols based on computational semantics. Acta Electronica Sinica, 42(6) (2014)

    Google Scholar 

  15. Xiao, M., Ma, C., Deng, C., Zhu, K.: A novel approach to automatic security protocol analysis based on authentication event logic. Chin. J. Electron. 24(1), 187–192 (2015)

    Article  Google Scholar 

  16. Chaki, S., Datta, A.: ASPIER: an automated framework for verifying security protocol implementations. In: 2009 22nd IEEE Computer Security Foundations Symposium

    Google Scholar 

  17. Aizatulin, M., Gordon, A.D., Jürjens, J.: Computational verification of C protocol implementations by symbolic execution. In: CCS 2012, Raleigh, North Carolina, 16–18 October 2012

    Google Scholar 

  18. Hasabnis, N., Sekar, R.: Extracting instruction semantics via symbolic execution of code generators. In: FSE 2016, Seattle, WA, USA, 13–18 November 2016

    Google Scholar 

  19. Milner, R.: Communication and Mobile Systems: The π - Calculus. Cambridge University Press, Cambridge (1999)

    Google Scholar 

  20. Jürjens, J.: Automated security verification for crypto protocol implementations: verifying the JESSIE project. Electron. Notes Theor. Comput. Sci. 250(1), 123–136 (2009)

    Article  Google Scholar 

  21. Backes, M., Busenius, A., Hriţcu, C.: On the development and formalization of an extensible code generator for real life security protocols. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 371–387. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_34

    Chapter  Google Scholar 

  22. Narendra Kumar, N.V., Shyamasundar, R.K.: POSTER: dynamic labelling for analyzing security protocols. In: CCS 2015, Denver, Colorado, USA, 12–16 October 2015

    Google Scholar 

  23. ITU-TS: Recommendation Z.120: Message Sequence Chart (MSC) ITU-TS, Geneva (1999)

    Google Scholar 

  24. Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Spring, Heidelberg (2012)

    Book  MATH  Google Scholar 

  25. Yao, A.C.-C., Yung, M., Zhao, Y.: Concurrent knowledge extraction in public-key models. J. Cryptol. 2, 156–219 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  26. Wang, J., Shi, Y., Peng, G., Zhang, H., et al.: Survey on key technology development and application in trusted computing. China Commun. 13(11), 70–90 (2016)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer School, Wuhan University, Wuhan, 430072, China

    Fu-Sheng Wu & Huan-Guo Zhang

  2. Key Laboratory of Aerospace Information Security and Trusted Computing of Ministry of Education, Wuhan University, Wuhan, 430072, China

    Fu-Sheng Wu & Huan-Guo Zhang

Authors
  1. Fu-Sheng Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Huan-Guo Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Huan-Guo Zhang .

Editor information

Editors and Affiliations

  1. National University of Defense Technology, Changsha, China

    Ming Xu

  2. Hunan University, Changsha, Hunan, China

    Zheng Qin

  3. Wuhan University, Wuhan, China

    Fei Yan

  4. National University of Defense Technology, Changsha, Hunan, China

    Shaojing Fu

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer Nature Singapore Pte Ltd.

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Wu, FS., Zhang, HG. (2017). A Dictionary Sequence Model to Analyze the Security of Protocol Implementations at the Source Code Level. In: Xu, M., Qin, Z., Yan, F., Fu, S. (eds) Trusted Computing and Information Security. CTCIS 2017. Communications in Computer and Information Science, vol 704. Springer, Singapore. https://doi.org/10.1007/978-981-10-7080-8_11

Download citation

  • DOI: https://doi.org/10.1007/978-981-10-7080-8_11

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-10-7079-2

  • Online ISBN: 978-981-10-7080-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation