The specification of the behaviour only describes the exchange of messages. It does not consider the data transferred by these messages. Abstract data types define the elements that are handled by the behavioural part. They define which kind of data are used by the protocol but also which operations are allowed on these data. Only the defined operations are permitted. With this restriction, complex cryptographic operations can be abstracted away from mathematical details. We will see that only a simple description of their characteristics is needed.
With LOTOS, abstract data types are written in ACT ONE. Each LOTOS variable can only have values of a particular sort defined during the declaration. A LOTOS type is a module composed of one or several sorts, operations and equations. A sort is the name given to a set of values that belong to the same domain. Specific operations are defined on the values of each sort and the semantics of these operations is provided by specific equations. This structure allows for a great flexibility in the handling of data in LOTOS.
A lot of mechanisms exist in modern cryptography [Sch96], but only a few of them are actually used in security protocols. We do not intend to make an exhaustive translation of cryptographic operations in ACT ONE. We just want to show the level of abstraction provided by LOTOS and the relative simplicity in the definition. Thus we will focus on two examples that represent the most widely used operations: encryption and signature in public-key cryptography. More subtle and complex cryptographic operations can be modelled. In section 4 we present a registration protocol we have specified that uses a zero-knowledge identification scheme.
ACT ONE is not only used to define the data transferred in messages, it is also used to define the internal database of information of each principal. For instance, a registration principal need to manage a registration database that will also be defined in ACT ONE as a table of records with multiple fields. This application is quite common and will not be developed further in this paper.
Definition of abstract data types can rapidly become very cumbersome to design. Thus our specification are written using data type language extensions, as offered by the APERO tool [Pec96] included in the Eucalyptus toolbox. The original text has to be preprocessed by the APERO translator to get a valid LOTOS specification. This provides for a smaller and more readable specification and for some level of immunity w.r.t. underlying processing tools. However, some types were written from scratch, hence, it was necessary to take tools restrictions explicilty into account. The other parts of the toolset will be explained in section 3.3.