When the LOTOS specification is written and the properties are formalized, we can perform the verification itself. We use the CADP package [FGK96] included in the Eucalyptus toolbox to carry out the verification of the protocol. As figure 3 shows, the LOTOS specification with datatype language extensions is converted into ISO LOTOS with the APERO tool. The next step consists of applying the Caesar tool to generate a graph called Labelled Transition System (LTS) from the LOTOS specification. This graph contains all the possible execution sequences of the protocol studied. Section 2.4 has addressed the feasibility of the generation. To gain confidence into the specification, it is simulated with the XSimulator in step-by-step execution mode.
The Aldebaran tool is the last stage of the processing. It performs the comparison of two labelled transition systems. The verification requires the comparison of the LTS of the protocol as created by the Caesar tool with the graphs of our properties. Thus a final step in the formalization is needed. The properties based on special events must appear like a finite-state graph. The process can be automated using the Caesar tool: each property is modelled as a reference LTS generated from a simple LOTOS process containing special events only.
The property discussed in section 3.2 can be specified in LOTOS as follows. The corresponding LTS generated by the Caesar tool is shown in figure 4.
behaviour
System_State! PROVER_START_AUTHENTICATION;Property[System_State]
where
process Property[System_State] : noexit
:=
System_State! PROVER_START_AUTHENTICATION;Property[System_State]
[]
System_State! VERIFIER_AUTHENTICATION_SUCCESSFUL;Property[System_State]
endproc
