## CryptoDB

### Birgit Pfitzmann

#### Publications

**Year**

**Venue**

**Title**

2010

EPRINT

Composable Security Analysis of OS Services
Abstract

We provide an analytical framework for analyzing basic integrity properties of file systems, namely the binding of files to filenames and writing capabilities. A salient feature of our modeling and analysis is that it is *composable*: In spite of the fact that we analyze the filesystem in isolation, security is guaranteed even when the file system operates as a component within an arbitrary, and potentially adversarial system. Such secure composability properties seem essential when trying to assert the security of large systems.
Our results are obtained by adapting the *Universally Composable* (UC) security framework to the analysis of software systems. Originally developed for cryptographic protocols, the UC framework allows the analysis of simple components in isolation, and provides assurance that these components maintain their behavior when combined in a large system, potentially under adversarial conditions.

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

Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario
Abstract

Web services are an important series of industry standards for adding
semantics to web-based and XML-based communication, in particular
among enterprises. Like the entire series, the security standards and
proposals are highly modular. Combinations of several standards are
put together for testing as interoperability scenarios, and these
scenarios are likely to evolve into industry best practices. In the
terminology of security research, the interoperability scenarios
correspond to security protocols. Hence, it is desirable to analyze
them for security. In this paper, we analyze the security of the new
Secure WS-ReliableMessaging Scenario, the first scenario to combine
security elements with elements of another quality-of-service
standard. We do this both symbolically and cryptographically. The
results of both analyses are positive. The discussion of actual
cryptographic primitives of web services security is a novelty of
independent interest in this paper.

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.

2005

EPRINT

Browser Model for Security Analysis of Browser-Based Protocols
Abstract

Currently, many industrial initiatives focus on web-based applications. In this context an important requirement is that the user should only rely on a standard web browser. Hence the underlying security services also rely solely on a browser for interaction with the user.
Browser-based identity federation is a prominent example of such
a protocol. Unfortunately, very little is still known about the security of browser-based protocols, and they seem at least as error-prone as standard security protocols. In particular, standard web browsers have limited cryptographic capabilities and thus new protocols are used. Furthermore, these protocols require certain care by the user in person, which must be modeled. In addition, browsers, unlike normal protocol principals, cannot be assumed to do nothing but execute the given security protocol.
In this paper, we lay the theoretical basis for the rigorous analysis and security proofs of browser-based security protocols. We formally model web browsers, secure browser channels, and the security-relevant browsing behavior of a user as automata. As a first rigorous security proof of a browser-based protocol we prove the security of password-based user authentication in our model. This is not only the most common stand-alone type of browser authentication, but also a fundamental building block for more complex protocols like identity federation.

2005

EPRINT

Limits of the Cryptographic Realization of Dolev-Yao-style XOR
Abstract

The abstraction of cryptographic operations by term algebras, called
Dolev-Yao models, is essential in almost all tool-supported methods
for proving security protocols. Recently significant progress was made
in proving that such abstractions can be sound with respect to actual
cryptographic realizations and security definitions. The strongest
results show this in the sense of reactive simulatability/UC, a notion
that essentially means retention of arbitrary security properties
under arbitrary active attacks and in arbitrary protocol environments,
with only small changes to both abstractions and natural
implementations.
However, these results are so far restricted to cryptographic systems
like encryption and signatures which essentially only have
constructors and destructors, but no further algebraic
properties. Typical modern tools and complexity results around
Dolev-Yao models also allow more algebraic operations. 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 to XOR, at least not with remotely the
same generality and naturalness as for the core cryptographic
systems. On the positive side, we show the soundness of an XOR model
and realization under passive attacks.

2005

EPRINT

Key-dependent Message Security under Active Attacks -- BRSIM/UC-Soundness of Symbolic Encryption with Key Cycles
Abstract

Key-dependent message security, short KDM security, was introduced by
Black, Rogaway and Shrimpton to address the case where key cycles
occur among encryptions, e.g., a key is encrypted with itself. It was
mainly motivated by key cycles in Dolev-Yao models, i.e., symbolic
abstractions of cryptography by term algebras, and a corresponding
soundness result was later shown by Ad\~{a}o et al. However, both the
KDM definition and this soundness result do not allow the general
active attacks typical for Dolev-Yao models and for security protocols
in general.
We extend these definitions so that we can obtain a soundness result
under active attacks. We first present a definition AKDM as a KDM
equivalent of authenticated symmetric encryption, i.e., it provides
chosen-ciphertext security and integrity of ciphertexts even for key
cycles. However, this is not yet sufficient for the desired
soundness, and thus we give a definition DKDM that additionally allows
limited dynamic revelation of keys. We show that this is sufficient
for soundness, even in the strong sense of blackbox reactive
simulatability (BRSIM)/UC and including joint terms with other
operators.
We also present constructions of schemes secure under the new
definitions, based on current KDM-secure schemes. Moreover, we
explore the relations between the new definitions and existing ones
for symmetric encryption in detail, in the sense of implications or
separating examples for almost all cases.

2004

EPRINT

Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library
Abstract

Recently we solved the long-standing open problem of justifying a
Dolev-Yao type model of cryptography as used in virtually all
automated protocol provers under active attacks. The justification
was done by defining an ideal system handling Dolev-Yao-style terms
and a cryptographic realization with the same user interface, and by
showing that the realization is as secure as the ideal system in the
sense of reactive simulatability. This definition encompasses
arbitrary active attacks and enjoys general composition and
property-preservation properties. Security holds in the standard
model of cryptography and under standard assumptions of adaptively
secure primitives.
A major primitive missing in that library so far is symmetric
encryption. We show why symmetric encryption is harder to idealize in
a way that allows general composition than existing primitives in this
library. We discuss several approaches to overcome these problems.
For our favorite approach we provide a detailed provably secure
idealization of symmetric encryption within the given framework for
constructing nested terms.

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.

2004

EPRINT

Relating Symbolic and Cryptographic Secrecy
Abstract

We investigate the relation between symbolic and cryptographic secrecy
properties for cryptographic protocols. Symbolic secrecy of payload
messages or exchanged keys is arguably the most important notion of
secrecy shown with automated proof tools. It means that an adversary
restricted to symbolic operations on terms can never get the entire
considered object into its knowledge set. Cryptographic secrecy
essentially means computational indistinguishability between the real
object and a random one, given the view of a much more general
adversary. In spite of recent advances in linking symbolic and
computational models of cryptography, no relation for secrecy under
active attacks is known yet.
For exchanged keys, we show that a certain strict symbolic secrecy
definition over a specific Dolev-Yao-style cryptographic library
implies cryptographic key secrecy for a real implementation of this
cryptographic library. For payload messages, we present the first
general cryptographic secrecy definition for a reactive scenario. The
main challenge is to separate secrecy violations by the protocol under
consideration from secrecy violations by the protocol users in a
general way. For this definition we show a general secrecy
preservation theorem under reactive simulatability, the cryptographic
notion of secure implementation. This theorem is of independent
cryptographic interest. We then show that symbolic secrecy implies
cryptographic payload secrecy for the same cryptographic library as
used in key secrecy. Our results thus enable existing formal proof
techniques to establish cryptographically sound proofs of secrecy for
payload messages and exchanged keys.

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

A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol
Abstract

We present the first cryptographically sound security proof of the
well-known Needham-Schroeder-Lowe public-key protocol. More precisely,
we show that the protocol is secure against arbitrary active attacks
if it is implemented using provably secure cryptographic primitives.
Although we achieve security under cryptographic definitions, our
proof does not have to deal with probabilistic aspects of cryptography
and is hence in the scope of current proof tools. The reason is that
we exploit a recently proposed ideal cryptographic library, which has
a provably secure cryptographic implementation. Besides establishing
the cryptographic security of the Needham-Schroeder-Lowe protocol, our
result also exemplifies the potential of this cryptographic library
and paves the way for cryptographically sound verification of security
protocols by means of formal proof tools.

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

Anonymous Fingerprinting with Direct Non-Repudiation
Abstract

Fingerprinting schemes support copyright protection by enabling the merchant of a data item to identify the original buyer of a
redistributed copy. In asymmetric schemes, the merchant can also convince an arbiter of this fact. Anonymous fingerprinting schemes enable buyers to purchase digital items anonymously; however, identification is possible if they redistribute the data item.
Recently, a concrete and reasonably efficient construction based on digital coins was proposed. A disadvantage is that the accused
buyer has to participate in any trial protocol to deny charges. Trials with direct non-repudiation, i.e., the merchant alone
holds enough evidence to convince an arbiter, are more useful in real life. This is similar to the difference between ``normal'' and ``undeniable'' signatures.
In this paper, we present an equally efficient anonymous fingerprinting scheme with direct non-repudiation. The main technique
we use, delayed verifiable encryption, is related to coin tracing in escrowed cash systems. However, there are technical differences, mainly to provide an unforgeable link to license conditions.

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

Self-Delegation with Controlled Propagation - or - What If You Lose Your Laptop
Abstract

We introduce delegation schemes wherein a user may delegate rights to
himself, i.e., to other public keys he owns, but may
not safely delegate those rights to others, i.e., to their
public keys. In our motivating application, a user
has a primary (long-term) key that receives rights, such as access
privileges, that may not be delegated to others, yet the user may
reasonably wish to delegate these rights to new
secondary (short-term) keys he creates to use on his laptop when
traveling, to avoid having to store his primary secret key on the
vulnerable laptop.
We propose several cryptographic schemes, both generic and practical,
that allow such self-delegation while providing strong motivation for
the user not to delegate rights that he only obtained for personal use
to other parties.

1993

CRYPTO

#### Program Committees

- TCC 2004
- Eurocrypt 2001 (Program chair)
- Eurocrypt 1998
- Eurocrypt 1995
- Crypto 1993

#### Coauthors

- Ammar Alkassar (1)
- Michael Backes (12)
- Niko Bari (1)
- David Basin (1)
- Gerrit Bleumer (1)
- Ran Canetti (1)
- Suresh Chari (1)
- David Chaum (1)
- Ivan Damgård (2)
- Alexander Geraldy (1)
- Oded Goldreich (2)
- Thomas Groß (1)
- Shai Halevi (1)
- Eugène van Heijst (2)
- Sebastian Mödersheim (1)
- Torben P. Pedersen (3)
- Andreas Pfitzmann (1)
- Ronald L. Rivest (2)
- Arnay Roy (1)
- Ahmad-Reza Sadeghi (5)
- Andre Scedrov (1)
- Matthias Schunter (3)
- Christoph Sprenger (1)
- Michael Steiner (1)
- Wietse Venema (1)
- Luca Viganò (1)
- Michael Waidner (14)