Model-based Design and Verification of Security Protocols using LOTOS
F. Germeau, Guy Leduc · Open Repository and Bibliography (University of Liège) · 1997
We explain how the formal language LOTOS can be used to specify security protocols and cryptographic operations. We describe how to model security properties 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 a simpler protocol that remains secure, and a more sophisticated protocol that allows a better distinction between intruder's attacks and ordinary errors. 1 Introduction Formal description techniques gain increased consideration due to significant advances and results recently obtained. A lot of computer systems achieve mission-critical tasks and thus require an absolute proof that they are working without any errors. Such a proof can be deduced with formal verifications. The ever growing power of computers and the increasing knowledge of verification techniques allow one to perform validations on real problems. W...