"Equicrypt" Trusted Third Party Protocol

Organisation:	University of Liege (Belgium) - Research Unit in Networking (RUN)
Method:	LOTOS
Tools used:	Eucalyptus toolset, including APERO CADP (Construction and Analysis of Distributed Processes) XELUDO
Domain:	Security protocols.
Period:	1996-1997
Size:	+/- 2000 lines, including the intruder process and comments.
Description:	Equicrypt is a Trusted Third Party (TTP) protocol considered in the European ACTS project number 051 (OKAPI) dealing with security, cryptography and authentication in computer networks. The Equicrypt protocol is meant to be a third party betwen video-on-demand service providers and customers. The formal language LOTOS was used to specify the Equicrypt protocol and verify its robustness to attacks by an intruder. We describe how this security protocol can be modelled in LOTOS at an appropriate abstraction level, and how security properties can be expressed and verified automatically. We describe a generic intruder process and its modelling. We have used the model-based CADP verification tools from the Eucalyptus toolbox to discover some successful attacks against this protocol. More precisely, all properties are fulfilled without the intruder, but some of them are falsified when the intruder is added. The diagnostic sequences can be used almost directly to exhibit the scenarios of possible attacks on the protocol. Two of them have been presented.
Conclusions:	Until very recently, the model-checking approach was not felt adequate to tackle the verification of security protocols, but our recent results prove the contrary and open new avenues for model-checking. The asset of this approach lies in the capability of finding the attacks as diagnostic sequences of unsatisfied properties. For a typical configuration, the generated model was composed of 786,681 states and 4,161,795 transitions. It took 20 hours of CPU time on a Sun Ultra-2 workstation running Solaris 2.5 with 800 Mbytes of RAM. After minimization with the strong bisimulation, the LTS had still 69,754 states and 520,633 transitions. The minimization was carried out in 20 minutes of CPU time on the same workstation.
Publications:	G. Leduc, O. Bonaventure, E. Koerner, L. Léonard, C. Pecheur, D. Zanetti. "Specification and verification of a TTP protocol for the conditional access to services". In: Proceedings of the 12th J. Cartier Workshop on Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control System. Montreal, Canada, 2-4 oct, 1996. Available on-line at: http://www-run.montefiore.ulg.ac.be/publications/papers/papers-list.html or from the CADP Web site in PDF or PostScript F. Germeau and G. Leduc. "Model-based Design and Verification of Security Protocols using LOTOS". In: Hilarie Orman and Catherine Meadows, eds, Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols (Rutgers University, New Jersey, USA), September 1997. Available on-line at: http://www-run.montefiore.ulg.ac.be/publications/papers/papers-list.html or also at: http://dimacs.rutgers.edu/Workshops/Security/program2/gl97-2/gl97-2.html or from the CADP Web site in PDF or PostScript F. Germeau and G. Leduc. "A Computer Aided Design of a Secure Registration Protocol". In: Teruo Higashino and Atsushi Togashi, eds, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification {FORTE/PSTV}'97 (Osaka, Japan), November 1997. Available on-line at: http://www-run.montefiore.ulg.ac.be/publications/papers/papers-list.html or from the CADP Web site in PDF or PostScript G. Leduc, O. Bonaventure, L. Léonard, E. Koerner, C. Pecheur. "Model-Based Verification of a Security Protocol for the Conditional Access to Services". Formal Methods in System Design, 14(2):171-191, March 1999. Available on-line at: http://www-run.montefiore.ulg.ac.be/publications/papers/abstract-PP99-01.html G. Leduc and F. Germeau. "Verification of Security Protocols using LOTOS - Method and Application". Computer Communications, 23(12):1089-1103, July 2000. Available on-line at: http://www-run.montefiore.ulg.ac.be/publications/papers/abstract-PP00-02.html or from the CADP Web site in PDF or PostScript See also: http://dimacs.rutgers.edu/Workshops/Security/program2/gl97-2/node14.html
Contact:	Guy Leduc Maitre de recherches F.N.R.S (Senior Research Associate) Universite de Liege Systemes et Automatique Institut d'Electricite Montefiore, B 28, B-4000 LIEGE 1 (BELGIUM) Tel : +32 4 366 26 98 Secr : +32 4 366 26 91 Fax : +32 4 366 29 89 URL: http://www-run.montefiore.ulg.ac.be/users/leduc.html Email: leduc@montefiore.ulg.ac.be
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