FormaCrypt project: meeting March 6, 2006

ENS Ulm, Room R, level -2 of the computer science department.

9:55 Welcome

Michael Backes, Strong Cryptographic Soundness of Dolev-Yao Models in the sense of Blackbox Reactive Simulatability (BRSIM)/UC, and Limitations Thereof (cancelled)

Blackbox Reactive Simulatability (BRSIM)/UC has proved to be a salient technique for defining and analyzing the security of general reactive systems, especially since it entails strong compositionality guarantees. Arguably one of the most important usages of BRSIM/UC was its successful application for coming up with the first proof that abstractions from cryptography by term algebras, so-called Dolev-Yao models, can be securely realized by actual cryptographic implementations under arbitrary active attacks. As the notion of BRSIM/UC essentially entails the preservation of arbitrary security properties under active attacks in arbitrary protocol environments, this result enables cryptographically sound, abstract protocol analyses of common Dolev-Yao style protocols, and by the compositionality of BRSIM/UC, automatically also for all protocols using them. These positive results hold for many of the common Dolev-Yao operations such as (a-)symmetric encryption, signatures, MACs, and pairing, and base terms such as nonces and payload data.

More recently, it has been shown that extending the relationship between Dolev-Yao models and cryptographic realizations in the sense of BRSIM/UC is not always possible as soon as operations with algebraic properties are added. The first such operation considered is typically XOR because of its clear structure and cryptographic usefulness. We show that it is impossible to extend the strong soundness results in the sense of BRSIM/UC to XOR, at least not with remotely the same generality and naturalness as for the core cryptographic systems. A similar negative result holds for hash functions: We show that it is impossible to extend the strong BRSIM/UC results to usual Dolev-Yao models of hash functions in the general case, i.e., by treating hash functions as free operators of the term algebra.

On the positive side we can show a Dolev-Yao model with hashes sound in the same strict sense of BRSIM/UC in the random oracle model of cryptography. For the standard model of cryptography, we also discuss several conceivable restrictions to the Dolev-Yao models with hashes and classify them into possible and impossible cases. Moreover, we show the soundness of a rather general Dolev-Yao model with XOR and its realization under passive attacks.

10-11 Bruno Blanchet, Automated Security Proofs with Sequences of Games (joint work with David Pointcheval) slides

This paper presents the first automatic technique for proving not only protocols but also primitives in the exact security computational model. Automatic proofs of cryptographic protocols were up to now reserved to the Dolev-Yao model, which however makes quite strong assumptions on the primitives. On the other hand, with the proofs by reductions, in the complexity theoretic framework, more subtle security assumptions can be considered, but security analyses are manual. A process calculus is thus defined in order to take into account the probabilistic semantics of the computational model. It is already rich enough to describe all the usual security notions of both symmetric and asymmetric cryptography, as well as the basic computational assumptions. As an example, we illustrate the use of the new tool with the proof of a quite famous asymmetric primitive: UF-CMA of the FDH-signature scheme under the (trapdoor)-one-wayness of some permutations.

11-12 Cédric Fournet, Cryptographically Sound Implementations for Communicating Processes (joint work with Pedro Adao) slides

We design a core language of principals running distributed programs over a public network. Our language is a variant of the pi calculus, with secure communications, mobile names, and high-level certificates, but without any explicit cryptography. Within this language, security properties can be conveniently studied using trace properties and observational equivalences, even in the presence of an arbitrary (abstract) adversary.

With some care, these security properties can be achieved in a concrete setting, relying instead on standard cryptographic primitives and computational assumptions, even in the presence of an adversary modelled as an arbitrary probabilistic polynomial-time algorithm. To this end, we develop a cryptographic implementation that preserves all properties for all safe programs. We give a series of soundness and completeness results that precisely relate the language to its implementation. We also illustrate our approach using a series of protocols and properties expressible in our language, and motivate some unusual design choices.

12-14: Lunch, restaurant "Les Bugnes"

14-14:30 Mathieu Baudet, Guessing Attacks and the Computational Soundness of Static Equivalence (joint work with Martín Abadi and Bogdan Warinschi) slides

The indistinguishability of two pieces of data (or two lists of pieces of data) can be represented formally in terms of a relation called static equivalence. Static equivalence depends on an underlying equational theory. The choice of an inappropriate equational theory can lead to overly pessimistic or overly optimistic notions of indistinguishability, and in turn to security criteria that require protection against impossible attacks or worse yet that ignore feasible ones. In this paper, we define and justify an equational theory for standard, fundamental cryptographic operations. This equational theory yields a notion of static equivalence that implies computational indistinguishability. Static equivalence remains liberal enough for use in applications. In particular, we develop and analyze a principled formal account of guessing attacks in terms of static equivalence.

14:30-15 Véronique Cortier, Computationally Sound Symbolic Secrecy in the Presence of Hash Functions (joint work with Steve Kremer, Ralf Küsters, and Bogdan Warinschi) slides

In this paper we devise a novel, cryptographically sound secrecy notion. Motivated by difficulties related to the use of hash functions, we depart from the more established deducibility-based definition and base our new criterion on patterns. Interestingly, our new notion is both necessary and sufficient for computational secrecy. The cryptographic primitives that we consider are pairing, (INDCCA secure) public-key encryption, and hashing, which is modeled as a random oracle. We also prove that any concrete trace resulting from a protocol execution in the cryptographic model can be mapped to a Dolev-Yao trace with overwhelming probability. To obtain our results we develop a new proof technique which is of independent interest.

15-15:30 Coffee Break

15:30-16 Discussion "Modular approach"

Introduction by Bogdan Warinschi slides

16-16:30 Discussion "Intermediate approach"

Introduction by Mathieu Turuani slides

16:30-17 Discussion "Direct approach"

Introduction by David Pointcheval slides
Page maintained by Bruno Blanchet