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.
Keywords
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.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Zhang, H.G., Han, W.B., Lai, X.J., et al.: Survey on cyberspace security. Sci. China Inf. Sci. 58(11), 1–43 (2015)
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)
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)
Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Sci. Comput. Progr. 58(1–2), 3–27 (2005)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, Oakland, California, pp. 140–154, May 2006
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)
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)
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)
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)
Backes, M., Maffei, M., Unruh, D.: Computationally sound verification of source code. In: CCS 2010, 4–8 October 2010
Avalle, M., Pironti, A., Sisto, R.: Formal verification of security protocol implementations: a survey. Formal Aspects Comput. 26(1), 99–123 (2014)
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
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)
Tang, C., Lu, Z., Feng, C.: A verification logic for security protocols based on computational semantics. Acta Electronica Sinica, 42(6) (2014)
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)
Chaki, S., Datta, A.: ASPIER: an automated framework for verifying security protocol implementations. In: 2009 22nd IEEE Computer Security Foundations Symposium
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
Hasabnis, N., Sekar, R.: Extracting instruction semantics via symbolic execution of code generators. In: FSE 2016, Seattle, WA, USA, 13–18 November 2016
Milner, R.: Communication and Mobile Systems: The π - Calculus. Cambridge University Press, Cambridge (1999)
Jürjens, J.: Automated security verification for crypto protocol implementations: verifying the JESSIE project. Electron. Notes Theor. Comput. Sci. 250(1), 123–136 (2009)
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
Narendra Kumar, N.V., Shyamasundar, R.K.: POSTER: dynamic labelling for analyzing security protocols. In: CCS 2015, Denver, Colorado, USA, 12–16 October 2015
ITU-TS: Recommendation Z.120: Message Sequence Chart (MSC) ITU-TS, Geneva (1999)
Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Spring, Heidelberg (2012)
Yao, A.C.-C., Yung, M., Zhao, Y.: Concurrent knowledge extraction in public-key models. J. Cryptol. 2, 156–219 (2016)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer Nature Singapore Pte Ltd.
About this paper
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)