next up previous
Next: Behaviour Up: Verification using LOTOS Previous: Introduction

LOTOS specification


The formal specification of a security protocol is written in LOTOS [BB87][ISO89] which is a standardized language suitable for the description of distributed systems. It is made up of two components:

The revision of the LOTOS standard is under study in ISO/IEC since 1991. The design of this enhanced version called E-LOTOS is based on the feedback obtained from practical applications of LOTOS and will certainly improve its expressive power.

A LOTOS specification is composed of two differents parts. The first one is dedicated to the description of the abstract data types and the cryptographic operations in particular. The second part describes the behaviour of the different entities involved in the protocol. We will firstly deal with this description