CWI (THE NETHERLANDS)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
360 lines of muCRL
The Needham-Schroeder public key authentication protocol aims at
providing mutual authentication between an initiator agent A and a
responder agent B, both of which want to be assured of the others'
identity before starting a communication session. A simplified form
of the protocol consists of the following three steps:
Six properties concerning authentication and two properties concerning secrecy were formulated in regular alternation-free mu-calculus and checked on the LTS model of the protocol using the EVALUATOR 3.0 model-checker of CADP. The diagnostic sequences provided by the model-checker allowed to rediscover the error first pointed out by Gavin Lowe in 1996 (the responder B commits to a session with the initiator A even if A does not try to establish a session with B). After fixing the error as described by Lowe, all properties were successfully checked. An improved version of the protocol in presence of a rational intruder (which avoids sending useless messages) was also studied.
This case-study was the first attempt of using the muCRL language
to specify and study security protocols. It has shown that the
capabilities of the language (especially the data types) are well-adapted for describing this kind of protocols. Also, the CADP
toolbox provides analysis features which are helpful in detecting
and diagnosing errors.
[Pang-02] Jun Pang. "Analysis of a Security Protocol in muCRL".
In Chris George and Huaikou Miao, editors, Proceedings of the 4th
International Conference on Formal Engineering Methods ICFEM 2002
(Shanghai, China), Lecture Notes in Computer Science vol. 2495,
pp. 396-400, October 2002. Full version available as CWI Report
SEN-R0201, Amsterdam, The Netherlands, January 2002.
Available on-line at: http://www.cwi.nl/ftp/CWIreports/SEN/SEN-R0201.ps.Z
or from our FTP site in PDF or PostScript
CWI / Department of Software Engineering
SEN2 (Specification and Analysis of Embedded Systems)
Kruislaan 413, 1098 SJ Amsterdam, The Netherlands
Tel: +31 (0)20 592 4221
Fax: +31 (0)20 592 4199
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|