Seventh International Workshop on Formal Methods for Industrial Critical Systems (FMICS 02)

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 cryptanalysed. 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 Society.

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 Security.

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.

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.

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.