next up previous
Next: Validation process Up: LOTOS specification Previous: Specification of the intruder

Finite model

 

The LOTOS specification will be translated into a labelled transition system (a graph) where the nodes are the state of the LOTOS specification and the transitions are labelled by the LOTOS actions. This labelled transition system (LTS) must comprise all the possible executions of the protocol. But this graph must be kept finite to be generated.

Some elements like random numbers or time stamps are specific to one run of the protocol leading to an infinite number of possible messages. This infinity must be controlled by giving some well chosen properties to these specific elements. Trusted principals will use one specific element for each run they perform, so we give them a limited set of elements that will be used during their executions. We also give the intruder one element but which is different from those of the trusted principals. When the intruder will use his element in a particular message, this will, in fact, model all the possible messages where the specific elements is not the one expected by a trusted principal.

Messages with a specific element can be split into messages with a correct specific element and messages with a wrong specific element. The first ones are limited in number but not the second ones. With our abstraction we can keep our model finite because a simple message is enough to represent all the incorrect ones.

In some protocols, we may need to consider an infinity or a big number of possible principals. As the LTS must be kept finite and also of reasonable size to be managed, the number of trusted principals must sometimes be drastically limited. The intruder's knowledge allows him to act as any other principal in a trusted or untrusted way, but it may not be sufficient to cover all cases.

There exist other ways to prevent the exponential growth of states. An infinite loop in the behaviour of a principal can be replaced by a limited number of runs adjusted to still cover all the possible intruder's attacks. Multiple configurations with multiple specifications can be planned to address several independant aspects of the protocol.

Great care must be taken with the restrictions imposed by the assumptions we are forced to make. We do not prove formally the correctness of our abstract finite model with respect to these assumptions. It would be interesting to consider such proof on the case studies we derive from this method. Some work in this direction is proposed in [Low96] where the verification with a limited number of principals is generalized or in [Bol97] where an abstraction function automates the computation of a correct abstract model. The main difficulty comes from the complexity of the protocols we want to verify.

Now that we have presented the complete specification, we will enter deeply into the verification process.


next up previous
Next: Validation process Up: LOTOS specification Previous: Specification of the intruder