Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Automated Validation of Internet Security Protocols

  • Speaker:   Dr  Luca Vigano  (University of Verona)
  • Host:   Renate Schmidt
  • 25th April 2007 at 14:15 in 1.5
Experience over the last twenty years has shown that the design of protocols for Internet security is highly error-prone and that conventional validation techniques based on informal arguments and/or testing are not up to the task. It is now widely recognized that only formal analysis can provide the level of assurance required by both the developers and the users of the protocols. This is especially true not only when one considers the simple academic protocols that have been proposed as example applications for automated reasoning techniques and tools (such as the Needham-Schroeder Public Key Protocol and the like), but also when one tries to scale up these techniques and tools to industrial-strength Internet security protocols (like Kerberos and IKE).

After an introduction to Internet security protocols and a survey of some prominent techniques and tools for security protocol analysis, I will discuss the techniques that underlie the AVISPA Tool, which is a state-of-the-art tool for push-button protocol validation. The AVISPA Tool provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of automatic protocol analysis techniques. I will in particular focus on one back-end, the symbolic on-the-fly model-checker OFMC. I will also discuss the integration of a framework that allows OFMC to handle algebraic properties of cryptographic operators in a uniform and modular way, and show how this provides a basis also for reasoning about off-line guessing attacks. Finally, I will discuss a first application of OFMC and the AVISPA Tool for reasoning about Web Services.
▲ Up to the top