next up previous
Next: Introduction

Model-based Design and Verification of Security Protocols
using LOTOS

F. Germeau, G. Leducgif

Research Unit in Networking (RUN)
Institut d'électricité Montefiore B.28, Université de Liège, B-4000 Liège, Belgium


We explain how the formal language LOTOS can be used to specify security protocols and cryptgraphic 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.