Every security protocol involves several entities called principals. A principal can be any object that plays a role in the evolution of the protocol. Example of principals are users, hosts or processes. When we address the verification of the security of the protocol, we must make some assumptions on the behaviour of the principals. Thus principals are qualified trusted or not. A trusted principal will always react according to the expected behaviour. A non-trusted principal can try and break the protocol with an unexpected behaviour though is considered genuine by the other entities.
Principals are linked together with communication channels to exhange messages. These communication channels are generally considered insecure, that is an intruder can act passively or actively on the transferred information. He can eavesdrop on messages, intercept them, replay old ones, or create new ones. The goal followed by the intruder ranges from a simple denial of service to the access to prohibited rights.
The behaviour section of a LOTOS specification is composed of several processes which interact with each other through interaction points called gates. Each principal involved in the protocol is modelled by a process that describes its exact behaviour. LOTOS allows the synchronisation of two or more processes via interactions that can occur at each gate. A one way communication channel between two principals is modelled by the synchronisation of the transmission gate of one principal with the reception gate of the other principal. A second synchronisation handles the other way of the communication channel.
For instance, figure 1 depicts a system with two principals where the
communication channel is modelled by the synchronisation of the gate A_to_B of
principal A with the gate A_to_B of principal B and with the synchronisation of
the gate B_to_A of principal A with the according gate of principal B.
To introduce the intruder that will try to threat the protocol we replace the simple communication channels by one central process that will act as the intruder. Thus the intruder can intercept all messages and transmit them or not, with or without modification. We will enter into the details of the intruder's behaviour in section 2.3. Back to our example, the principals are not interacting directly with each others but indirectly through the intruder process (figure 2). The intruder is the only principal considered untrusted. All other principals are trusted. We model cases where a principal is not trusted by giving enough power to the intruder to act as a genuine principal.
Finally, we use an environment to monitor the progress of the protocol. When a
principal reaches a sensitive point, he informs the environment
by sending him a message through the System_State gate. These messages
are called special events and will be developed further in section 3.2. They
will be of a great help to perform the formal verification. The environment is
also responsible for the reception of error messages. Figure 2
presents the complete structure of a typical LOTOS specification that models a
security protocol between two principals.
Each process that represents a principal is parameterized with an initial knowledge. This knowledge includes identifiers, keys or whatever information a principal must know before runs of the prococol can occur. As we will see later, the knowledge is the core of the intruder's modelling.
