Please use this identifier to cite or link to this item:
Title: SeVe: Automatic tool for verification of security protocols
Authors: Luu, A.T.
Sun, J.
Liu, Y. 
Dong, J.S. 
Li, X.
Quan, T.T.
Keywords: authentication
model checking
process analysis toolkit (PAT)
security protocols
Issue Date: 2012
Citation: Luu, A.T., Sun, J., Liu, Y., Dong, J.S., Li, X., Quan, T.T. (2012). SeVe: Automatic tool for verification of security protocols. Frontiers of Computer Science in China 6 (1) : 57-75. ScholarBank@NUS Repository.
Abstract: Security protocols play more and more important roles with wide use in many applications nowadays. Currently, there are many tools for specifying and verifying security protocols such as Casper/FDR, ProVerif, or AVISPA. In these tools, the intruder's ability, which either needs 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. In this paper, 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 an 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 also given. The results of this paper are embodied in the implementation of a SeVe module in a process analysis toolkit (PAT) model checker, which supports specifying, simulating, and verifying security protocols. The experimental results show that a 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. © 2012 Higher Education Press and Springer-Verlag Berlin Heidelberg.
Source Title: Frontiers of Computer Science in China
ISSN: 16737350
DOI: 10.1007/s11704-012-2903-3
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Aug 12, 2020


checked on Aug 12, 2020

Page view(s)

checked on Aug 3, 2020

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.