Logic based analysis of security protocols in a unified verification framework

Security protocols are one of the imperative steps in creating and ensuring the secure communication and information processing. Also known as cryptographic protocols or encryption protocols, they are used for secure application-level data transport achieved by using a security function and applying cryptographic methods. A wide variety of different forms of security go beyond the traditional goals of secure authentication, integrity and data confidentiality. Modern applications require more subtle properties like blind signatures used for digital cash, non-repudiation, secure digital time-stamping, etc. However, these protocols are vulnerable to different kinds of attacks and their design in achieving data safety and confidentiality has proven to be challenging and error prone. Informal and intuitive techniques have been proposed to verify such protocols. Several methods such as modal logics and state space exploration were developed to ensure formal verification and validation of security protocols. This thesis presents the integration of a logic based verification technique into an existing verification framework. The existing framework unifies the verification of protocols through both state based techniques and modal logics. The integration is done through a translator that takes the input file specified in the language of the verification framework and translates it into the language of the logic-based verification technique. The validity of the proposed translation/integration is demonstrated in an empirical study in which a set of protocols are specified and their verification results are compared using the old logic based verification engine and the new verification framework. Comparison of both verification results establishes their equivalence. This proves validity of the translation process between the two verification engines.