## CryptoDB

### Michael Waidner

#### Affiliation: IBM Research Zurich Lab

#### Publications

**Year**

**Venue**

**Title**

2006

EPRINT

Reactively Simulatable Certified Mail
Abstract

(Revision of Sept. 2004 of a journal submission from Dec. 2000.)
Certified mail is the fair exchange of a message
for a receipt, i.e., the recipient gets the message if
and only if the sender gets a receipt. It is an important
primitive for electronic commerce and other atomicity services.
Certified-mail protocols are known in the literature, but there
was no rigorous definition yet, in particular for optimistic protocols
and for many interleaved executions.
We provide such a definition via an ideal system and show that
a specific real certified-mail protocol is as secure as this ideal
system in the sense of reactive simulatability in the standard model
of cryptography and under standard assumptions.
As certified mail without any third party is not practical, we consider optimistic protocols,
which involve a third party only if one party tries to cheat.
The real protocol resembles prior protocols, but we had to use a different
cryptographic primitive to achieve simulatability.
The communication model is synchronous.
This proof first demonstrated that a cryptographic multi-step protocol
can fulfil a general definition of reactive simulatability
enabling concurrent composition.
We also first showed how formal-method style reasoning can be applied
over the ideal system in a cryptographically sound way.
Moreover, the treatment of multiple protocol runs and their modular proof in spite
of the use of common cryptographic primitives for all runs can
be seen as a first example of what is now known as joint-state composition.

2006

EPRINT

Cryptographically Sound Theorem Proving
Abstract

We describe a faithful embedding of the Dolev-Yao model of Backes,
Pfitzmann, and Waidner (CCS 2003) in the theorem prover Isabelle/HOL.
This model is cryptographically sound in the strong sense of reactive
simulatability/UC, which essentially entails the preservation of
arbitrary security properties under active attacks and in arbitrary
protocol environments. The main challenge in designing a practical
formalization of this model is to cope with the complexity of
providing such strong soundness guarantees. We reduce this complexity
by abstracting the model into a sound, light-weight formalization that
enables both concise property specifications and efficient application
of our proof strategies and their supporting proof tools. This yields
the first tool-supported framework for symbolically verifying security
protocols that enjoys the strong cryptographic soundness guarantees
provided by reactive simulatability/UC. As a proof of concept, we have
proved the security of the Needham-Schroeder-Lowe protocol using our
framework.

2006

EPRINT

Limits of the Reactive Simulatability/UC of Dolev-Yao Models with Hashes
Abstract

Automated tools such as model checkers and theorem provers for the
analysis of security protocols typically abstract from cryptography by
Dolev-Yao models, i.e., abstract term algebras replace the real
cryptographic operations. Recently it was shown that in essence this
approach is cryptographically sound for certain operations like
signing and encryption. The strongest results show this in the sense
of blackbox reactive simulatability (BRSIM)/UC with only small changes
to both Dolev-Yao models and natural implementations. This notion
essentially means the preservation of arbitrary security properties
under active attacks in arbitrary protocol environments.
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. These
models treat hash functions as free operators of the term algebra. In
contrast, we show that these models are sound in the same strict sense
in the random oracle model of cryptography. For the standard model of
cryptography, we also discuss several conceivable restrictions to the
Dolev-Yao models and classify them into possible and impossible cases.

2004

EPRINT

The Reactive Simulatability (RSIM) Framework for Asynchronous Systems
Abstract

We define \emph{reactive simulatability} for general
asynchronous systems. Roughly, simulatability means that a real system
implements an ideal system (specification) in a way that preserves
security in a general cryptographic sense.
Reactive means that the system can interact with its users
multiple times, e.g., in many concurrent protocol runs or a multi-round
game. In terms of distributed systems, reactive simulatability
is a type of refinement that preserves particularly strong properties,
in particular confidentiality.
A core feature of reactive simulatability is \emph{composability}, i.e.,
the real system can be plugged in instead of the ideal system within
arbitrary larger systems; this is shown in follow-up papers, and so is the
preservation of many classes of individual security properties
from the ideal to the real systems.
A large part of this paper defines a suitable system model. It is
based on probabilistic IO automata (PIOA) with two main new features:
One is \emph{generic distributed scheduling}. Important special cases
are realistic adversarial scheduling, procedure-call-type scheduling
among colocated system parts, and special schedulers such as for
fairness, also in combinations. The other is the definition of the
\emph{reactive runtime} via a realization by Turing machines such
that notions like polynomial-time are composable. The simple
complexity of the transition functions of the automata is not
composable.
As specializations of this model we define security-specific concepts,
in particular a separation beween honest users and adversaries and several
trust models.
The benefit of IO automata as the main model, instead of only interactive
Turing machines as usual in cryptographic multi-party computation,
is that many cryptographic systems can be specified with an ideal system
consisting of only one simple, deterministic IO automaton without any
cryptographic objects, as many follow-up papers show. This enables the use of
classic formal methods and automatic proof tools for proving
larger distributed protocols and systems that use these cryptographic systems.

2003

EPRINT

A Universally Composable Cryptographic Library
Abstract

Bridging the gap between formal methods and cryptography has recently received a lot of interest, i.e., investigating to what extent proofs of cryptographic protocols made with abstracted cryptographic operations are valid for real implementations. However, a major goal has not been achieved yet: a soundness proof for an abstract crypto-library as needed for the cryptographic protocols typically proved with formal methods, e.g., authentication and key exchange protocols. Prior work that directly justifies the typical Dolev-Yao abstraction is restricted to passive adversaries and certain protocol environments. Prior work starting from the cryptographic side entirely hides the cryptographic objects, so that the operations are not composable: While secure channels or signing of application data is modeled, one cannot encrypt a signature or sign a key.
We make the major step towards this goal: We specify an abstract crypto-library that allows composed operations, define a cryptographic realization, and prove that the abstraction is sound for arbitrary active attacks in arbitrary reactive scenarios. The library currently contains public-key encryption and signatures, nonces, lists, and application data.
The proof is a novel combination of a probabilistic, imperfect bisimulation with cryptographic reductions and static information-flow analysis.

2003

EPRINT

Symmetric Authentication Within a Simulatable Cryptographic Library
Abstract

Proofs of security protocols typically employ simple abstractions of
cryptographic operations, so that large parts of such proofs are
independent of cryptographic details. The typical abstraction is
the Dolev-Yao model, which treats cryptographic operations as a
specific term algebra. However, there is no cryptographic semantics,
i.e., no theorem that says what a proof with the Dolev-Yao
abstraction implies for the real protocol, even if provably secure
cryptographic primitives are used.
Recently we introduced an extension to the Dolev-Yao model for which
such a cryptographic semantics exists, i.e., where security is
preserved if the abstractions are instantiated with provably secure
cryptographic primitives. Only asymmetric operations (digital
signatures and public-key encryption) are considered so far. Here we
extend this model to include a first symmetric primitive,
message authentication, and prove that the extended model still has
all desired properties. The proof is a combination of a probabilistic,
imperfect bisimulation with cryptographic reductions and static
information-flow analysis.
Considering symmetric primitives adds a major complication to the
original model: we must deal with the exchange of secret keys, which
might happen any time before or after the keys have been used for
the first time. Without symmetric primitives only public keys need
to be exchanged.

2000

EPRINT

A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission
Abstract

We present the first rigorous model for secure reactive systems in
asynchronous networks with a sound cryptographic semantics, supporting
abstract specifications and the composition of secure systems. This
enables modular proofs of security, which is essential in bridging
the gap between the rigorous proof techniques of cryptography and
tool-supported formal proof techniques.
The model follows the general simulatability approach of modern
cryptography. A variety of network structures and trust models can
be described, such as static and adaptive adversaries.
As an example of our specification methodology we provide the first
abstract and complete specification for Secure Message Transmission,
improving on recent results by Lynch, and verify one
concrete implementation. Our proof is based on a general theorem on
the security of encryption in a reactive multi-user setting,
generalizing a recent result by Bellare et.al.

1997

EPRINT

Optimistic fair Exchange of Digital Signatures
Abstract

We present a new protocol that allows two players to exchange digital
signatures (including RSA and DSS) over the Internet in a fair way, so
that either each player gets the other's signature, or neither player
does. One obvious application is where the signatures represent items
of value, for example, an electronic check or airline ticket; the
protocol can also be adapted to exchange encrypted data. The protocol
relies on a trusted third party, but is "optimistic," in that the
third party is only needed in cases where one player attempts to cheat
or simply crashes. This is an important property, as it greatly
reduces the load on the third party, which in particular facilitates
a more robust and secure implementation of the third party.

#### Program Committees

- Eurocrypt 2001

#### Coauthors

- N. Asokan (2)
- Michael Backes (6)
- David Basin (1)
- Gerrit Bleumer (1)
- Birgit Pfitzmann (14)
- Andreas Pfitzmann (1)
- Matthias Schunter (2)
- Victor Shoup (2)
- Christoph Sprenger (1)