RISC Seminars (Research on Information Security and Cryptology)
Archives: [2024] [2023] [2022] [2021] [2020] [2019] [2018] [2017] [2016] [2015] [2014] [2013] [2012] [2011] [2010] [2009] [2008] [2007] [2006] [2005] [2004] [List of Speakers](To receive information about upcoming seminars, register for the RISC mailing list.)
[print]
Special RISC Seminar on Formal Methods and Cryptography
Date: | March 9 |
Location: | NIKHEF, Room H331 |
Schedule: | |
10:45-11:30 | Michael Backes (Saarland University): Strong Cryptographic Soundness of Dolev-Yao Models in the sense of Blackbox Reactive Simulatability (BRSIM)/UC, and Limitations Thereof 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. |
11:30-12:15 | Martin Abadi (UC Santa Cruz): Security Analysis of Cryptographically Controlled Access to XML Documents 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. |
12:15-13:30 | Lunch break |
13:30-14:00 | Dennis Hofheinz (CWI): On the (Im-)Possibility of Extending Coin Toss 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
|
14:00-14:30 | Jaco van de Pol (CWI): Confluence reduction and Parallel algorithms for Verification 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.
|
14:30-15:00 | Sjouke Mauw (TU Eindhoven): Generalizing Needham-Schroeder-Lowe for Multi-Party Authentication 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 |
15:00-15:30 | Sandro Etalle (Twente University): Towards A Logic for Accountability |
15:30-15:45 | Break |
15:45-16:15 | Ronald Cramer (CWI & Leiden University): Algebraic Geometric Aspects of Secure Computation |
16:15-16:30 | Simon Kramer (EPFL Lausanne): Logical Concepts in Cryptography |
16:30-16:45 | Robbert de Haan (CWI): Atomic Secure Multi-Party Multiplication with Low Communication |
16:45-17:00 | Mohammed Dashti (CWI): Dolev-Yao intruder: A process algebraic look |
0.04978s