CWI Cryptology Group

Abstract: 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.

Abstract: Some promising recent schemes for XML access control employ encryption for implementing security policies on published data, avoiding data duplication. We consider one such scheme, due to Miklau and Suciu. That scheme was introduced with some intuitive explanations and goals, but without precise definitions and guarantees for the use of cryptography (specifically, symmetric encryption and secret sharing). We bridge this gap. Our approach, which relates symbolic and complexity-theoretic definitions, continues a recent thrust in research on security protocols and may be applicable to a broader class of systems that rely on cryptographic data protection.
This talk is based on joint work with Bogdan Warinschi (LORIA). It is mostly based on a paper by the same title that was presented at PODS 2005, and includes at least a brief discussion of more recent advances.

Abstract: We consider the cryptographic two-party protocol task of extending a given coin toss. The protocol goal is thus to generate n common random coins that are uniformly and independently distributed even if one party is corrupted. Since we are dealing with the extension of a given coin toss, we assume that a coin toss of m

Abstract: Verifying reactive systems by model checking consists of generating the state space from a specification and applying graph algorithms on this state space, either during or after generation. Our research at CWI is focused at scaling this up to larger models. One can distinguish two phases: First, the specification is transformed symbolically to a smaller one that still satisfies the same properties. Examples of such techniques are static analysis, abstraction and confluence reduction. The latter will be explained in some detail. The second phase is the generation and analysis of large graphs. We experiment with distributing these graphs over a cluster of workstations, and implementing parallel graph algorithms. This increases the available memory and decreases total running time, despite increased communication overhead.

Abstract: We propose a protocol for multi-party authentication for any number of parties, which generalizes the well-known Needham-Schroeder-Lowe protocol. We argue that the protocol provides authentication of the communicating parties (by proving injective synchronisation) and secrecy of the generated challenges. For p parties, the protocol consists of 2p-1 messages, which we show to be the minimal number of messages required to achieve the desired security properties in the presence of a Dolev-Yao style intruder. The underlying communication structure of the generalized protocol can serve as the backbone of a range of authentication protocols.
Joint work with Cas Cremers