A framework for formal verification of security protocols in C++

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.