Information Technology Reference
In-Depth Information
A Generic Model
for Analyzing Security Protocols
Yonggen Gu, Yuxi Fu, Farong Zhong, and Han Zhu
BASICS, Department of Computer Science and Engineering,
Shanghai Jiao Tong University, Shanghai 200030, China
{
gyg68, fu-yx, zhong-fr, zhu-h
}
@sjtu.edu.cn
Abstract.
Formal methods have proved useful in the analysis of secu-
rity protocols. The paper proposes a generic model for the analysis of
the security protocols (GSPM for short) that supports message passing
semantics and constructs for modelling the behavior of agents. GSPM is
simple, but it is expressive enough to express security protocols and prop-
erties in a precise and faithful manner. Using GSPM it is shown how se-
curity properties such as confidentiality, authentication, non-repudiation,
fairness, and anonymity can be described. Finally an example of formal
verification is illustrated.
1
Introduction
Security protocols are playing an increasingly important role and have become
an essential ingredient of communication infrastructures. They are designed to
provide properties such as confidentiality, authentication, non-repudiation, fair-
ness, and anonymity for users who wish to exchange messages through a medium
over which they have little control. However the design of a security protocol is a
di
cult and error-prone task. Many popular and widely used security protocols
have been shown to have flaws. For this reason, the use of formal methods for
the verification of security protocols has received increasing attention.
Since the security protocols themselves often contain a great deal of com-
binatorial complexity, it is extremely dicult to model them and verify their
properties. Over the past few years various modelling languages, for instance
logics and process algebras, have been proposed for the systematic and tool-
supported analysis of the security protocols. Formal methods have proved useful
in the analysis of the security protocols. A popular approach is to model a proto-
col as a system of concurrent processes, described using an appropriate language
like CSP [9]. In [10] Lowe found a new attack to Needham-Schroeder public-
key protocol [13] by encoding and analysing it in CSP. Following this initial
work, numerous other calculi have been studied for the purpose of modelling
and analyzing security protocols. For example, VSPA [8] is a value passing vari-
ant of CCS [11] extended to incorporate two security levels; The spi calculus [2]
The work is supported by The Young Scientist Research Fund (60225012),The Nat-
ural Science Fund (60473006) and The National 973 Project (2003CB316905).
