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