Andrew D. Gordon (Microsoft Research, Cambridge, UK)
Authenticity Types for Cryptographic Protocols
based on joint work with Alan Jeffrey, DePaul University (Chicago, IL, USA)
Cryptographic protocols are essential for the security of many critical
networking applications, such as authenticating various financial
transactions. Moreover, many new consumer-to-business and
business-to-business protocols are being proposed and need cryptographic
protection. It is famously hard to specify and verify such protocols,
even if we assume that the underlying cryptographic algorithms cannot be
My invited talk describes a new approach to specifying and verifying
authenticity properties of security protocols, based on a typed process
algebra. The theory has been developed in a series of papers with Alan
Jeffrey. Our approach requires little human effort per protocol, puts
no bound on the size of the opponent attacking the protocol, and
requires no state space enumeration. Moreover, the types for protocol
data provide Some intuitive explanation of how the protocol works. My
talk explains the basic ideas by example, states our main results, and
outlines our plans for applications of this technology.
A.D. Gordon and A. Jeffrey. Types and effects for asymmetric
cryptographic protocols. In 15th IEEE Computer Security Foundations
Workshop (CSFW 2002), Cape Breton, June 24-26, 2002. IEEE Computer
A.D. Gordon and A. Jeffrey. Authenticity by typing for security
protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW
2001), pages 145-159, Cape Breton, June 11-13, 2001. IEEE Computer
Society. A journal version is to appear in the Journal of Computer
A.D. Gordon and A. Jeffrey. Typing correspondence assertions for
communication protocols. In Seventeenth Conference on the Mathematical
Foundations of Programming Semantics (MFPS 2001), Elsevier ENTCS 45,
2001. A journal version is to appear in Theoretical Computer Science.
Andreas Podelski (Max-Planck-Institut für Informatik, Germany)
Abstraction for Software Model Checking
based on joint work with Tom Ball and Sriram Rajamani (Microsoft Research, Redmond WA, USA), and Andrei Rybalchenko (Max-Planck-Institut, Germany)
A program with variables over unbounded data domains (e.g. integers)
generates an infinite-state transition system. Thus, one approach to
extend model checking to software works by mapping an infinite-state
transition system to a finite one. We explain the limitations of that
approach and show how one can go beyond. We present a whole spectrum
of abstractions with different precision/cost trade-off's. In order
to automatize software model checking, we combine the automated
process of abstraction with an automated process to make the
abstraction more and more precise (namely until the property can be
proven in the abstract). We present new ideas on parametrizing such
an `abstraction refinement' process.
T. Ball, A. Podelski, and S. Rajamani. Relative Completeness of
Abstraction Refinement for Software Model Checking. In Proceedings of
TACAS 2002, LNCS 2280, pages 158-172.
Wang Yi (Uppsala University, Sweden)
Synthesis of Verified Real Time Software
In this talk. I will present a unified model for timed systems
to bridge scheduling, model checking and code synthesis. The technical
contributions include a general notion of schedulability for automata
and efficient algorithms for schedulability checking.
TIMES is a tool
developed based on these recent results and our past experience in
developing the UPPAAL tool. It is designed for synthesis of verified
software guaranteeing timing constraints. This talk will review recent
development on TIMES and published results from papers.
Elena Fersman, Paul Pettersson, and Wang Yi.
Timed Automata with Asynchronous Processes: Schedulability and Decidability.
Proceedings of TACAS 2002, LNCS 2280, pages 67-82
Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson,
and Wang Yi.
Times - A Tool for Modelling and Implementation of Embedded Systems.
Proceedings of TACAS 2002, LNCS 2280, pages 460-464.