Needham-Schroeder Public Key Authentication Protocol.

Organisation:	CWI (THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Cryptography.
Period:	2001-2002
Size:	360 lines of muCRL
Description:	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: Step 1: the initiator A selects a nonce Na and sends it along with its identity to B, both encrypted with B's public key Kb. Step 2: the responder B receives the message, decrypts it in order to obtain the nonce Na, and then it returns Na to A together with a new nonce Nb, both encrypted with A's public key Ka. Step 3: when A receives this message, it concludes that it is talking to B (since only B should be able to decrypt A's initial message containing nonce Na) and sends to B the nonce Nb encrypted with B's public key, which allows B to authenticate A in the same manner. In order to analyse the correctness of the protocol, a configuration containing an initiator, a responder, and an intruder agent was described in muCRL. The intruder has the capability of capturing any message exchanged among the other agents, to decrypt messages that are encoded with its own public key, to store parts of messages in its own knowledge database, to replay an old message it has seen before, and to generate new messages by combining the information contained in its database. 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.
Conclusions:	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.
Publications:	[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 the CADP Web site in PDF or PostScript
Contact:	Jun Pang CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam, The Netherlands Room: M325 Tel: +31 (0)20 592 4221 Fax: +31 (0)20 592 4199 E-mail: Jun.Pang@cwi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page