Research Unit in Networking (RUN), Université de Liège (BELGIUM)
CADP (Construction and Analysis of Distributed Processes)
about 190 lines of LOTOS
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.
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.
"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
Prof. Guy Leduc
Université de Liège
Institut d'Electricité Montefiore
B-4000 Liège 1
Tel: +32 4 366 26 98
Fax: +32 4 366 29 89
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|