Abstract
Every communication system is a safety-critical system, in which the communicating entities share the confidential data over the untrusted public network by using a set of cryptographic security protocols (CSPs). Many security protocols proved secure were cracked within a short span of time, and the best example is Needham–Schroeder authentication protocol. The quality assurance about the correctness of security protocols is one of the key challenges. In software testing, it is not possible to prove the correctness of security protocols, because testing has got major drawbacks and the tester cannot predict what knowledge an attacker may gain about the communication system by interacting with several runs of the protocol, and also testing shows the presence of bugs but can never show the absence of bugs. Formal verification has proved to be a reliable solution as the correctness of the CSP can be proved mathematically. In the proposed work, a new framework is proposed, which includes a library of functions to specify a security protocol in C++ by following a set of rules (syntax and semantics), a interpreter to interpret the C++ code to security protocol description language (SPDL), and finally a model checker Scyther backend verification engine. The proposed framework is successful in identifying the attacks on IKE version-1. Also the Skeme and Oakley versions were verified for their correctness.
Supported by Defence Research and Development Organisation (DRDO), SAG, New Delhi.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Needham RM, Schroeder MD (1978) Using encryption for authentication in large networks of computers. Commun ACM 21(12):993–999. https://doi.org/10.1145/359657.359659, http://doi.acm.org/10.1145/359657.359659
Lowe G (1996) Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria T, Steffen B (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 147–166
Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2014) FDR3—a modern refinement checker for CSP. In: Ábrahám E, Havelund K (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 187–201
Cremers C, Mauw S, de Vink E (2003) Formal methods for security protocols: three examples of the black-box approach. NVTI Newsl 7:21–32. Newsletter of the Dutch Association for Theoretical Computing Scientists
Roscoe AW (1994) Model-checking CSP. In: A classical mind. Prentice Hall International (UK) Ltd., Hertfordshire, UK, pp 353–378. http://dl.acm.org/citation.cfm?id=197600.197628
Herzog J (2005) A computational interpretation of Dolev-Yao adversaries. Theor Comput Sci 340(1):57–81
Clarke EM, Grumberg O (1987) Avoiding the state explosion problem in temporal logic model checking. In: Proceedings of the sixth annual ACM symposium on principles of distributed computing. ACM, pp 294–303
Cremers C, Mauw S (2012) Operational semantics and verification of security protocols. Springer
Carrel D, Harkins D (1998) The Internet Key Exchange (IKE). RFC 2409. https://doi.org/10.17487/RFC2409, https://rfc-editor.org/rfc/rfc2409.txt
Krawczyk H (1996) Skeme: a versatile secure key exchange mechanism for internet. In: Proceedings of the 1996 symposium on network and distributed system security (SNDSS ’96). SNDSS ’96, IEEE Computer Society, Washington, DC, USA, p 114.http://dl.acm.org/citation.cfm?id=525423.830460
Herzog J (2005) A computational interpretation of Dolev-Yao adversaries. Theor Comput Sci 340(1):57–81. https://doi.org/10.1016/j.tcs.2005.03.003, http://www.sciencedirect.com/science/article/pii/S0304397505001179. Theoretical Foundations of Security Analysis and Design II
Holzmann G (2003) The spin model checker: primer and reference manual, 1st edn. Addison-Wesley Professional
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Pradeep, R., Sunitha, N.R., Ravi, V., Verma, S. (2020). A Framework for Formal Verification of Security Protocols in C++. In: Ranganathan, G., Chen, J., Rocha, Á. (eds) Inventive Communication and Computational Technologies. Lecture Notes in Networks and Systems, vol 89. Springer, Singapore. https://doi.org/10.1007/978-981-15-0146-3_17
Download citation
DOI: https://doi.org/10.1007/978-981-15-0146-3_17
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-15-0145-6
Online ISBN: 978-981-15-0146-3
eBook Packages: EngineeringEngineering (R0)