International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Michael Waidner

Affiliation: IBM Research Zurich Lab

Publications

Year
Venue
Title
2006
EPRINT
Reactively Simulatable Certified Mail
(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
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
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
TCC
2004
EPRINT
The Reactive Simulatability (RSIM) Framework for Asynchronous Systems
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
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
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
Birgit Pfitzmann Michael Waidner
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.
1998
EUROCRYPT
1997
EUROCRYPT
1997
EPRINT
Optimistic fair Exchange of Digital Signatures
N. Asokan V. Shoup M. Waidner
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.
1995
EUROCRYPT
1992
EUROCRYPT
1991
CRYPTO
1990
EUROCRYPT
1989
EUROCRYPT
1989
EUROCRYPT
1985
EUROCRYPT

Program Committees

Eurocrypt 2001