Formal description techniques gain increased consideration due to significant advances and results recently obtained. A lot of computer systems achieve mission-critical tasks and thus require an absolute proof that they are working without any errors. Such a proof can be deduced with formal verifications. The ever growing power of computers and the increasing knowledge of verification techniques allow one to perform validations on real problems. With the development of the Internet and specially with the birth of the electronic commerce, the security of communications between computers becomes a crucial point. All these new applications require reliable protocols able to perform secure transactions. The environment of these operations is very hostile because no transmission channel can be considered safe. Formal descriptions and verifications can be used to obtain the assurance that a protocol cannot be threatened by an intruder.
Special modal logics have been designed to verify authentication protocols. The most well-known such logic is the BAN logic [BAN90], but some others have been proposed to overcome some of its limitations. Such logics have been used successfully to verify several protocols, but have not proved very effective in some other circumstances. Another approach consists of using general purpose formal methods usually applied to more conventional protocols. They are supported by verification tools, such as theorem provers or model-checkers, which makes it possible to automate the proof process. Approaches based on theorem proving applicable to a large class of protocols and to general authentication properties have been proposed [Mea92][Bol96].
Until recently among the different formal methods, the model-checking approach was not felt adequate to tackle the verification of security protocols. Recent results prove the contrary, this approach can in fact be very efficient to achieve a real computer aided design of security protocols. To our knowledge, its first application to the verification of security protocols was achieved in [Low96] where the Needham-Schroeder protocol [Sch96] was specified in CSP [Hoa85] and model-checked by the FDR tool. Independently of this work, we specified the Equicrypt protocol [LBQ96] in LOTOS and used the Eucalyptus toolbox [Gar96] to verify it [LBK96][GL97]. The present paper will focus on the method we used to model and verify a security protocol using LOTOS.
The paper is organized as follow. In section 2, we will show that the LOTOS language is a very good performer to handle the specification of security protocols. With its flexibility, a wide range of cryptographic operations can be modelled. We will describe the establishment of security properties and the associated verification process in section 3. The verification is quite automatic and allows one to certify that an intruder cannot break a cryptographic protocol with different kinds of attacks. An application of our method on a concrete protocol will be presented in section 4. We will also point out that it is possible to tune a protocol in order to obtain new properties and improve its behaviour.