This paper presents a formal verification process for security protocols using LOTOS. We have shown how to specify a protocol with the concept of trusted and untrusted principals. The flexibility of abstract data types allows the description of a wide range of cryptographic operations. We have shown the modelling of the classical public-key scheme but also a more complex one: the Guillou-Quisquater algorithm.
We have shown how intrusion can be taken into account by adding an intruder process replacing the communication channels. Our model of this intruder is very simple and powerful. He can mimic very easily all reasonable real-world attacks, that is all non cryptographic and non repetitive attacks.
We have explained the validation process and the formalization of security properties. They can be modelled as safety properties with the help of special events triggered when crucial states are reached. The verification is based on the safety preorder which should hold between the system and the property.
Our method is illustrated with a registration protocol where we have found a subtle flaw that could probably not have been discovered, at least so early, by a human-being. The verification is quite automatic and allows one to make efficient corrections and improvements. Some assumptions on the model were required and formal proofs of their correctness are an interesting future work. Nevertheless, this example demonstrates that LOTOS is suitable to verify complex cryptographic protocols that can enforce a wide variety of security properties.