Challenge Handshake Authentication Protocol (CHAP).

Organisation:	Research Unit in Networking (RUN), Université de Liège (BELGIUM)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Cryptography.
Period:	1999.
Size:	about 190 lines of LOTOS
Description:	The Challenge Handshake Authentication Protocol (CHAP) is a protocol used to authenticate both ends of a communication link. It is intended for use primarily by hosts and routers that connect to a PPP (Point-to-Point Protocol) network server via switched circuits or dial-up lines, but might be applied to dedicated links as well. CHAP uses a a challenge response mechanism based on a nonce (a sort of random number used only once) and a shared secret, which is only known to the entities that want to authenticate each other. Mutual authentication can be achieved by running the protocol in both directions. In this case the shared secret can be the same for both directions, but the RFC highly recommends to use two different secrets. This case-study deals with the verification of two versions (with one resp. two shared secrets) of the CHAP protocol. Using LOTOS and the CADP verification tools, the author has been able to prove that the first version has a flaw, whereas the second one is robust to passive and active attacks. The methodology used is based on the following principle. The service of CHAP (i.e., the suitable orderings of service primitives) is derived when no intruder is present and shown to satisfy the authentication properties. Then an intruder process is inserted, which behaves as an insecure full-duplex communication link. The intruder can interrupt, intercept, modify or insert messages in the channels but cannot directly access the secret shared by the two entities of the protocol. To check that the protocol is robust, the authentication properties must be satisfied by the service of CHAP derived in the presence of an intruder. Firstly, the verification of CHAP without any intruder is performed. The LTS model has been generated with CAESAR and minimized with ALDEBARAN. The authentication property (i.e., when initiating a connection, the other party is indeed the one it claims to be) has been expressed as a regular sequence of transitions and checked on the LTS using the EXHIBITOR tool. In the presence of an intruder, the two versions of the CHAP protocol have been specified and checked against the authentication properties. The first one (with a single secret) appeared to be erroneous: EXHIBITOR produced the scenario of an attack in which the intruder is able to substitute himself to one of the CHAP entities. The second version of the protocol (with two secrets) proved to be robust against intruder attacks.
Conclusions:	This case-study illustrates a model-based methodology for verifying security protocols by using the specification language LOTOS and the CADP verification toolset. Intrusion can be taken into account by adding an intruder process replacing the communication channels. This allows to model in a simple and powerful way the real-world, non-cryptographic and non-repetitive attacks on the behaviour of the protocol. Moreover, model-checking tools such as CADP allow to explicitly exhibit the scenarios of attacks, thus providing valuable information for the debugging of security protocols.
Publications:	[RFC1994] W. Simpson. "PPP Challenge Handshake Authentication Protocol (CHAP)". Available online at: http://www.faqs.org/rfcs/rfc1994.html [Leduc-99] Guy Leduc. "Verification of two versions of the Challenge Handshake Authentication Protocol (CHAP)". Annals of Telecommunications 55(1-2):18-30, January-February 1999. Available on-line at: ftp://ftp.run.montefiore.ulg.ac.be/pub/RUN-PP00-01.ps or from the CADP Web site in PDF or PostScript
Contact:	Prof. Guy Leduc Université de Liège Institut d'Electricité Montefiore Bât. B28 B-4000 Liège 1 Belgium Tel: +32 4 366 26 98 Fax: +32 4 366 29 89 E-mail: [email protected]
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