A Model-Checker for the Symbolic Analysis of Internet Security Protocols

Luca Viganò - ETHZ - Zurich (CH)
Data e ora
martedì 22 febbraio 2005 alle ore 17.30 - Ore 17.00 tè, caffè & c.
Maria Paola Bonacina
Referente esterno
Data pubblicazione
24 gennaio 2005


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 a brief introduction to Internet security protocols, I will first
survey some prominent techniques and tools for security protocol
analysis, and then discuss in detail the techniques that underlie the
symbolic on-the-fly model-checker OFMC, a state-of-the-art protocol
analysis tool that I have been developing together with colleagues at
the ETH Zurich. OFMC can successfully analyze and validate Internet
security protocols (such as Kerberos, IKE, and other protocols that have
been proposed by standardization organizations like the IETF) and it has
found a number of new attacks on such protocols.

© 2002 - 2021  Università degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234