Seve: Automatic tool for verification of security protocols

Abstract

Security protocols play more and more important role with widely use in many applications nowadays. They are designed to provide security properties for users who want to exchange messages over unsecured medium. Currently, there are many tools for specifying and verifying security protocols such as Casper/FDR, ProVerif or AVISPA. In these tools, the knowledge of participants, which is useful to reason about some security properties, is not included in the model. The intruder?s ability, which is either needed to be specified explicitly or set by default, is not flexible in some circumstances. Moreover, whereas most of the existing tools focus on secrecy and authentication properties, few supports privacy properties like anonymity, receipt freeness and coercion resistance, which are crucial in many applications such as in electronic voting systems or anonymous online transactions. To the best of our knowledge, there is still no automatic tool using formal methods to verify security protocols related to receipt freeness and coercion resistance properties. In this thesis, we introduce a framework for specifying security protocols in the Labeled Transition System (LTS) semantics model, which embeds the knowledge of the participants and parameterizes the ability of attacker. Using this model, we give the formal definitions for three types of privacy properties based on trace equivalence and knowledge reasoning. The formal definitions for some other security properties such as secrecy and authentication are introduced under this framework, and the verification algorithms are given as well. The results of this thesis are embodied in the implementation of a SeVe module in PAT model checker, which supports specifying, simulating and verifying security protocols. The tool is built towards supporting automatic verification: the users only need to specify the security protocols using SeVe language (which is introduced to ease the user from specifying security protocols), the tool will automatically generate the system behaviors and the verification results are given by just one click. The experimental results show that SeVe module is capable of verifying many types of security protocols and complements the state-of-the-art security verifiers in several aspects. Moreover, it also proves the ability in building an automatic verifier for security protocols related to privacy type, which are mostly verified by hand now.