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:
A process algebra, moslty inspired by CCS [Mil89] and CSP [Hoa85], with a
structured operational semantics. It describes the behaviour of processes and
their interactions. LOTOS has a rich set of operators (multiway synchronization
and abstraction like in CSP, disabling, ...), and an explicit internal action
like in CCS.
An abstract datatype language. ACT ONE [EM85], with an initial
semantics. A type is defined by its signature (sorts + operation on the sorts)
and by equations to give a meaning to the operations.
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
