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:

• 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

 
• Behaviour
• Abstract data types
  • Principles
  • Public-key encryption and signature
• The intruder
  • Model
  • Specification of the intruder
• Finite model