Events

10:00am Bruno Blanchet (CNRS, ENS Ulm)
A Computationally Sound Mechanized Prover for Security ProtocolsWe present a new mechanized prover for secrecy properties of cryptographic protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these games are formalized in a probabilistic polynomial-time process calculus. Our tool provides a generic method for specifying security properties of the cryptographic primitives, which can handle shared- and public-key encryption, signatures, message authentication codes, and hash functions. Our tool produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. We have implemented our tool and tested it on a number of examples of protocols from the literature.

Bruno Blanchet is Chargé de Recherches CNRS in the abstract interpretation team of LIENS, headed by Patrick Cousot.

10:45am Gilles Barthe (INRIA Sophia-Antipolis)
Evidence Preserving Compilation

Program logics and information-flow type systems typically operate at source code, while evidence is often required, especially in the context of mobile code, on compiled programs. In this talk, we shall examine the means to bring the benefits of source code verification to code consumers, through mechanisms that translate evidence.

Gilles Barthe is Directeur de recherches INRIA. He heads the EVEREST team at INRIA Sophia-Antipolis. His research interests lie in the areas of formal methods, programming languages and security. He also has a strong interest in mathematical logic and theoretical computer science, in particular in dependent type theory.

11:15am Coffee break,

11:45am Ricardo Corin (Universiteit Twente)
A Probabilistic Hoare-style Logic for Game-based Cryptographic Proofs

We extend a Probabilistic Hoare-style logic to formalize game-based cryptographic proofs. Our approach provides a systematic and rigorous framework, thus preventing errors from being introduced. We illustrate our technique by proving semantic security of ElGamal.

Ricardo Corin recently defended his Ph.D. thesis at University of Twente.

12:15am Cédric Fournet (MSR Cambridge)
Verified Interoperable Implementations of Security Protocols

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and illustrate our approach with protocols for Web Services security.

Cédric Fournet graduated from Ecole Polytechnique in 1992, worked for a year on deductive databases at BULL, obtained a second engineering degree from Ecole Nationale des Ponts et Chaussées in 1995, then did a PhD in computer science at INRIA Rocquencourt. In this PhD, he applied some concurrency theory to model distributed programming: he proposed a variant of the pi calculus as the core of a distributed programming language. He used this calculus to model the behavior of programs and implementations, in particular agent-based mobility, partial failure, and security. He also wrote the distributed runtime for a prototype implementation of the language. He joined MSR Cambridge in 1998, where he is a member of the Programming Principles and Tools group.

12:45am Jean-Jacques Lévy (INRIA Rocquencourt)
History-based Flow Analysis in the Lambda Calculus

Standard flow analysis is based on the ownership by individuals of expressions and function libraries. Flow analysis can be tested statically as in Pottier-Simonet for the full Caml language without objects. It can also be checked dynamically as in the technique of stack inspection for Java/C# formalized by Fournet-Gordon. We want to study the theory of flow analysis taking care of the history of creation of redexes in the lambda-calculus, as a model of mixing static and dynamic methods for flow analysis in programming languages.

Jean-Jacques Lévy heads the Moscova team at INRIA-Rocquencourt.