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
{germeau,leduc}@montefiore.ulg.ac.be

Abstract

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.