Please use this identifier to cite or link to this item: https://doi.org/10.1007/s11704-012-2903-3
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
privacy
process analysis toolkit (PAT)
secrecy
security protocols
Issue Date: 2012
Source: 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. https://doi.org/10.1007/s11704-012-2903-3
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
URI: http://scholarbank.nus.edu.sg/handle/10635/43023
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.

SCOPUSTM   
Citations

7
checked on Dec 7, 2017

WEB OF SCIENCETM
Citations

4
checked on Nov 23, 2017

Page view(s)

56
checked on Dec 11, 2017

Google ScholarTM

Check

Altmetric


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