Model-based Design and Verification of Security Protocols
using LOTOS

F. Germeau, G. Leduc

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.

 
• Introduction
• LOTOS specification
  • Behaviour
  • Abstract data types
    • Principles
    • Public-key encryption and signature
  • The intruder
    • Model
    • Specification of the intruder
  • Finite model
• Validation process
  • Properties to verify
  • Formalizing the properties
  • The verification toolbox
  • The verification
• An example of verification
  • The registration protocol
  • Procotol specification
  • Formalizing the properties
  • A flaw
  • Corrected protocol
  • Enhancements of the protocol
    • The simplest protocol
    • Distinction between failures and errors
• Conclusion
• Acknowledgements
• References
• About this document ...