Advertisement

Annales Des Télécommunications

, Volume 55, Issue 1–2, pp 20–30 | Cite as

Verification of two versions of the challenge handshake authentication protocol (chap)

  • Guy Leduc
Article

Abstract

The challenge handshake authentication protocol, chap, is an authentication protocol intended for use primarily by hosts and routers that connect to a network server via switched circuits or dial-up lines, but might be applied to dedicated links as well. In this paper, we specify two versions of the protocol, using the formal language Lotos, and apply the Eucalyptus model-based verification tools to prove that the first version has a flaw, whereas the second one is robust to passive and active attacks. The paper is written in a tutorial fashion with a strong emphasis on the methodology used. The relative simplicity of the chap protocol allows one to include complete Lotos specifications and definitions of properties, so that the experiment can be reproduced easily.

Key words

Communication protocol Authentication Validation Formal description technique Description language Crytography Security Signal interception 

Vérification de deux versions du protocole d’authentification mutuelle chap

Résumé

Le protocole chap (challenge handshake authentication protocol) est un protocole d’authentification utilisé principalement par des ordinateurs ou des routeurs qui s’interconnectent via des circuits commutés ou des lignes téléphoniques, mais il peut aussi être utilisé sur des liaisons spécialisées. Cet article spécifie deux versions du protocole en Lotos, et prouve à l’aide de la boîte à outils Eucalyptus que la première a une faille, mais que la seconde résiste à des attaques passives et actives. Cet article est écrit sous forme didactique en insistant sur la méthodologie utilisée. La simplicité relative du protocole chap permet d’inclure les spécifications Lotos complètes et les définitions des propriétés, de façon à rendre l’étude de cas reproductible.

Mots clés

Protocole communication Authentification Validation Technique description formelle Langage description Crytographie Sécurité Interception signal 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AG97]
    Abadi (M.),Gordon (A. D.). A calculus for cryptographic protocols : The Spi calculus.Proceedings of the 4th ACM Conference on Computer and Communication Security, (1997).Google Scholar
  2. [BFG+91]
    Bouajjani (A.), Fernandez (J.-C), Graf (S.), Rodriguez (C), Sifakis. (J.). Safety for branching time semantics.In: 18th icalp, Berlin,Springer-Verlag, (July 1991).Google Scholar
  3. [BoB87]
    Bolognesi (T.), Brinksma (E.). Introduction to the ISO specification language Lotos.Computer Networks and ISDN Systems,14, n° 1, pp. 25–59, (1987).CrossRefGoogle Scholar
  4. [Bol96]
    Bolignano (D.). Formal verification of cryptographic protocols.In : Proc. of the 3rd ACM Conference on Computer and Communication Security, (1996).Google Scholar
  5. [CG90]
    Chen (P.),Gligob (V.). On the formal specification and verification of a multiparty session protocol.In : Proc. of the IEEE Symposium on Research in Security and Privacy, (1990).Google Scholar
  6. [DEK82]
    Dolev (D.),Even (S.),Karp (R.). On the security of ping-pong protocols.Information and Control, pp. 57-68, (1982).Google Scholar
  7. [DNV90]
    Nicola (R.), Vaandrager (F.W.). Actions versus state based logics for transition systems.Proc. Ecole de Printemps on Semantics of Concurrency, lncs 469, Springer-Verlag, Berlin, pp. 407–419, (1990).Google Scholar
  8. [DoY83]
    Dolev (D.),ad Yao (A.),ieee Transactions on Information Theory, 29(2): 198–208, (March 1983).zbMATHCrossRefGoogle Scholar
  9. [EM85]
    Ehrig (H.),Mahr (B.). Fundamentals on the security of public key protocols of algebraic specification 1, equations and initial semantics.In : W. Brauer, B. Rozenberg, A. Salomaa, eds., EATCS , Monographs on Theoretical Computer Science, Springer-Verlag, (1985).Google Scholar
  10. [FGK+96]
    Fernandez (J.-C), Garavel (H.), Kerbrat (A.), Mateescu (R.), Mounier (L.), Sighireanu (M.). cadp (Caesar/Aldebaran development package): a protocol validation and verification toolbox. In :R. Alur andT. Henzinger, eds, Proc. of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA), (Aug. 1996).Google Scholar
  11. [Gar96]
    Garavel (H.). An overview of the Eucalyptus toolbox.In : Proc. of the COST247 workshop (Maribor, Slovenia), (June 1996).Google Scholar
  12. [Gar98]
    Garavel (H.). Open/Caesar: an open software architecture for verification, simulation and testing.Proc. of TACAS’98, LNCS 1384, Springer-Verlag, Berlin, pp. 68–84, (1998).Google Scholar
  13. [GL97a]
    Germeau (F.), Leduc (G.). Model-based design and verification of security protocols using Lotos.Proc. of the Dimacs Workshop on Design and Formal Verification of Security Protocols, Rutgers University, NJ, USA, 22 p, (Sept. 97).Google Scholar
  14. [GL97B]
    Germeau (F.), Leduc (G.). A computer-aided design of a secure registration protocol.Formal Description Techniques and Protocol Specification, Testing and Verification, forte/pstv’ 97, Chapman & Hall, London, pp. 145–160, (1997).Google Scholar
  15. [Hoa 85]
    Hoare (C. A. R.). Communicating sequential processes.Prentice-Hall International, (1985).Google Scholar
  16. [ISO8807]
    iso/iec. Information processing systems - open systems interconnection - Lotos, a formal description technique based on the temporal ordering of observational behaviour.IS 8807, (February 1989).Google Scholar
  17. [Kem89]
    Kemmerer (R.). Using formal methods to analyse encryption protocols,ieee Journal on Selected Areas in Communications,7, n° 4, p. 448–457, (1989).CrossRefGoogle Scholar
  18. [KMM94]
    Kemmerer (R.), Meadows (C), Millen (J.). Three systems for cryptographic protocol analysis.Journal of Cryptology,7, n° 2, pp. 14–18, (1989).Google Scholar
  19. [LBK+96]
    Leduc (G.),Bonaventure (O.),Koerner (E.),Léonard (L.),Pécheur (C),Zanetti (D.). Specification and verification of a ttp protocol for the conditional access to services.In : Proc. of 12th J. Cartier Workshop on “Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control System ”, Montreal, Canada, (2-4 Oct. 96).Google Scholar
  20. [LBL+99]
    Leduc (G.), Bonaventure (O.), Léonard (L.), Koerner (E.), Pécheur (C). Model-based verification of a security protocol for conditional access to services.Formal Methods in System Design,14, n° 2, pp. 171–191, (March 1999).CrossRefGoogle Scholar
  21. [LG99]
    Leduc (G.),Germeau (F.). Verification of security protocols using Lotos - method and application.To appear in Computer Communications, special issue on “Formal Description Techniques in Practice”.Google Scholar
  22. [Low96]
    Lowe (G.). Breaking and fixing the Needham- Schroeder public-key protocol using fdr.In : T. Margaria and B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1055, Springer-Verlag, (1996).Google Scholar
  23. [LR97]
    Lowe (G.), Roscoe (B.). Using csp to detect errors in the tmn protocol,ieee Transactions on Software Engineering,23, n° 10, pp.659–669, (Oct. 1997).CrossRefGoogle Scholar
  24. [MCF87]
    Millen (J.), Clark (S.), Freedman (S.). The interrogator : protocol security analysis.IEEE Transactions on Software Engineering,13, n° 2, (1987).Google Scholar
  25. [MCJ97]
    Marrero (W.),Clarke (E.),Jha (S.). A model checker for authentication protocols.Proc. of the Dimacs Workshop on Design and Formal Verification of Security Protocols, Rutgers University, (Sept. 1997).Google Scholar
  26. [Mea94]
    Meadows (C). The nrl protocol analyser: an overview.Journal of Logic Programming,19, n° 20, pp. 1–679, (1994).Google Scholar
  27. [Mil 89]
    Milner (R.). Communication and concurrency.Prentice-Hall Intern., London, (1989).Google Scholar
  28. [MSS97]
    Mitchell (J.),Shmatikov (V.),Stern (U.). Finite- state analysis of ssl 3.0 and related protocols.Proc. of the Dimacs Workshop on Design and Formal Verification of Security Protocols, Rutgers University, (Sept. 1997).Google Scholar
  29. [NFG+91]
    de Nicola (R.),Fantechi (A.),Gnesi (S.),Ristori (G.). An action based framework for verifying logical and behavioural properties of concurrent systems,University of La Sapienza, Roma.Google Scholar
  30. [Par81]
    Park (D.). Concurrency and automata on infinite sequences.In P. Deussen ed., Theoretical Computer Science, lncs 104, Springer-Verlag, pp. 167-183, (March 1981).Google Scholar
  31. [Pec96]
    Pécheur (C). Improving the specification of data types in Lotos.Doctoral Dissertation, University of Liège, (July 1996).Google Scholar
  32. [RFC 1994]
    Simpson (W.). ppp challenge handshake authentication protocol (chap),rfc 1994, (August 1996).Google Scholar
  33. [Sch98]
    Schneider (S.). Verifying authentication protocols in CSP.ieee Transactions on Software Engineering,24, n° 9, pp. 751–758, (Sept. 1998).CrossRefGoogle Scholar
  34. [Sta99]
    Stallings (W.) Cryptography and network security -Second Edition. Prentice-Hall, (1999).Google Scholar
  35. [STS94]
    Stepien (B.),Tourrilhes (J.),Sincennes (J.). Eludo: The University of Ottawa Toolkit. Technical Report, Univesity of Ottawa, (1994).Google Scholar
  36. [VGW89]
    van Glabeek (R.),Weijland (W.). Branching-time and abstraction in bisimulation semantics.Proc. of the 11th World Computer Congress, San Francisco, (1989).Google Scholar
  37. [WL93]
    Woo Lam (A.). A semantic model for authentication protocols.In: Proc. of ieee Symposium on Research in Security and Privacy, (1993).Google Scholar

Copyright information

© Springer-Verlag 2000

Authors and Affiliations

  1. 1.Research Unit in Networking (RUN)Université de Liège, Institut MontefioreLiège

Personalised recommendations