Verification of security protocols using LOTOS-method and application

We explain how the formal language LOTOS can be used to specify security protocols and cryptographic operations. We describe how security properties can be modelled as safety properties and how a model-based verification method can be used to verify the robustness of a protocol against attacks of an intruder. We illustrate our technique on a concrete registration protocol. We find an attack, correct the protocol, propose a simpler yet secure protocol, and finally a more sophisticated protocol that allows a better discrimination between intruder's attacks and classical protocol errors. (C) 2000 Elsevier Science B.V. All rights reserved.