The difficulty of designing and analyzing security protocols
has long been recognized. It appeared that a large portion of
the protocols described in academic literature is subject to
attacks [1]. Formal analysis is one of the approaches that help
to detect and correct found vulnerabilities.
There are a numbers of publications in which the process
algebra CSP language and the FDR model checker were used for
protocol analysis [2, 3]. However, FDR tool is a commercial
product and even evaluation and academic licenses are not
free. The purpose of this project is to show the feasibility
of using the SMV tool [4], which is free and available for
the number of platforms. The tool uses state-machine based
SMV language.
As a case study, a Needham-Schroeder public-key authentication
protocol [5] was chosen. A flaw was discovered in it 17 years
after original paper was published [2]. I'm going to describe
the protocol and intruder behaviors in SMV language and using
the SMV tool rediscover the flaw or prove that the flaw doesn't
exist after applying the Lowe's fix [2] for two instances
of the protocol. It is well known that one of the weaknesses
of this approach is that it can be applied only for a limited
number of instances of the protocol.
Proving that there is no flaw exists for some number of instances
does not necessary guarantee that there is no attack involving
more instances (although it is not the case with the Needham-Schroeder
protocol as it was shown in [2]). I'm going to find out what
is the practical number of instances of the mentioned protocol
SMV tool can handle and how the time and memory demand varies
with the number of protocol instances involved.
Final presentation: on-line,
PDF
SMV models and trace:
prot.smv (protocol
and intruder models), description
(PDF)
prot_wo_intruder.smv (protocol
model, no intruder)
attack.tra (attack trace, can be
viewed in SMV tool)
Literature
[1] G. Lowe. Some new attacks upon security protocols. Oct.
1996.
[2] G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key
Protocol using FDR. In proceedings of TACAS, volume 1055,
1996.
[3] P. Y. A. Ryan, S. A. Schneider. The Modeling and Analysis
of Security Protocols: the CSP Approach. Addison-Wesley, 2001.
[4] SMV home page, http://www-cad.eecs.berkeley.edu/~kenmcmil/
[5] R. Needham, M. Schroeder. Using Encryption for Authentication
in Large Networks of Computers. Communications of the ACM,
1978.
|