## CryptoDB

### Dominique Unruh

#### Affiliation: University of Tartu, Estonia

#### Publications

**Year**

**Venue**

**Title**

2013

JOFC

Polynomial Runtime and Composability
Abstract

We devise a notion of polynomial runtime suitable for the simulation-based security analysis of multi-party cryptographic protocols. Somewhat surprisingly, straightforward notions of polynomial runtime lack expressivity for reactive tasks and/or lead to an unnatural simulation-based security notion. Indeed, the problem has been recognized in previous works, and several notions of polynomial runtime have already been proposed. However, our new notion, dubbed reactive polynomial time, is the first to combine the following properties: it is simple enough to support simple security/runtime analyses,it is intuitive in the sense that all intuitively feasible protocols and attacks (and only those) are considered polynomial-time,it supports secure composition of protocols in the sense of a universal composition theorem. We work in the Universal Composability (UC) protocol framework. We remark that while the UC framework already features a universal composition theorem, we develop new techniques to prove secure composition in the case of reactively polynomial-time protocols and attacks.

2010

EPRINT

Quantum Proofs of Knowledge
Abstract

We motivate, define and construct quantum proofs of knowledge, proofs
of knowledge secure against quantum adversaries. Our constructions are
based on a new quantum rewinding technique that allows us to extract
witnesses in many classical proofs of knowledge. We give criteria
under which a classical proof of knowledge is a quantum proof of
knowledge. Combining our results with Watrous' results on quantum
zero-knowledge, we show that there are zero-knowledge quantum proofs
of knowledge for all languages in NP.

2010

EPRINT

Concurrent composition in the bounded quantum storage model
Abstract

We define the BQS-UC model, a variant of the UC model, that deals with
protocols in the bounded quantum storage model. We present a
statistically secure commitment protocol in the BQS-UC model that
composes concurrently with other protocols and an (a-priori)
polynomially-bounded number of instances of itself. Our protocol has
an efficient simulator which is important if one wishes to compose our
protocol with protocols that are only computationally
secure. Combining our result with prior results, we get a
statistically BQS-UC secure constant-round protocol for general
two-party computation without the need for any setup assumption.

2010

EPRINT

The impossibility of computationally sound XOR
Abstract

We give a simple example that there is no symbolic theory for exclusive or (XOR) that is computationally sound.

2010

EPRINT

Computationally Sound Verification of Source Code
Abstract

Increasing attention has recently been given to the formal
verification of the source code of cryptographic protocols. The
standard approach is to use symbolic abstractions of cryptography that
make the analysis amenable to automation. This leaves the possibility
of attacks that exploit the mathematical properties of the
cryptographic algorithms themselves. In this paper, we show how to
conduct the protocol analysis on the source code level (F# in our
case) in a computationally sound way, i.e., taking into account
cryptographic security definitions.
We build upon the prominent F7 verification framework (Bengtson et
al., CSF 2008) which comprises a security type-checker for F# protocol
implementations using symbolic idealizations and the concurrent lambda
calculus RCF to model a core fragment of F#.
To leverage this prior work, we give conditions under which symbolic
security of RCF programs using cryptographic idealizations implies
computational security of the same programs using cryptographic
algorithms. Combined with F7, this yields a computationally sound,
automated verification of F# code containing public-key encryptions
and signatures.
For the actual computational soundness proof, we use the CoSP
framework (Backes, Hofheinz, and Unruh, CCS 2009). We thus inherit the
modularity of CoSP, which allows for easily extending our proof to
other cryptographic primitives.

2009

EPRINT

A general framework for computational soundness proofs - or - The computational soundness of the applied pi-calculus
Abstract

We provide a general framework for conducting computational soundness
proofs of symbolic models. Our framework considers arbitrary sets of
constructors, deduction rules, and computational implementations, and
it abstracts away from many details that are not core for proving
computational soundness such as message scheduling, corruption models,
and even the internal structure of a protocol. We identify several
properties of a so-called simulator such that the existence of a
simulator with all these properties already entails computational
soundness in the sense of preservation of trace properties in our
framework. This simulator-based characterization allows for proving
soundness results in a conceptually modular and generic way.
We exemplify the usefulness of our framework by proving the first
computational soundness result for the full-fledged applied
$\pi$-calculus under active attacks. Concretely, we embed the applied
$\pi$-calculus into our framework and give a sound implementation of
public-key encryption.

2009

EPRINT

Polynomial Runtime and Composability
Abstract

To prove security of a multi-party cryptographic protocol, one often reduces attacks on the protocol to attacks on a suitable computational problem. Thus, if the computational problem is hard, then the protocol is secure. But to allow for a security reduction, the protocol itself and the attack on the protocol must be efficient, i.e., polynomial-time. Of course, the obvious way to enforce an overall polynomial runtime of the protocol is to require each individual protocol machine and adversarial entity to be polynomial-time. However, as the specific case of zero-knowledge protocols demonstrates, an a priori polynomial-time bound on all entities may not be an optimal choice because the running time of some machines needs to depend on that of others. As we want to be able to model arbitrary protocol tasks, we work in the Universal Composability framework (UC). This framework additionally provides strong composability guarantees. We will point out that in the UC setting, finding a useful notion of polynomial-time for the analysis of general protocols is a highly non-trivial task.
Our goal in this work is to find a good and useful definition of polynomial-time for multi-party protocols in the UC setting that matches the intuition of what is feasible. A good definition should have the following properties:
* Flexibility: All "intuitively feasible" protocols and protocol tasks should be considered polynomial-time.
* Soundness: All "intuitively feasible" attacks (i.e., adversaries) should be considered polynomial-time.
* Completeness: Only "intuitively feasible" attacks should be considered polynomial-time. In particular, this implies that the security of protocols can be reduced to computational hardness assumptions.
* Composability: The induced security notion should support secure (universal) composition of protocols.
* Simplicity: The notion should be easy to formulate, and for all practical cases, it should be easy to decide whether a protocol or attack runs in polynomial time.
The problem of finding a good definition of polynomial time in the UC framework has been considered in a number of works, but no definition satisfying the five above criteria had been found so far. This seemingly simple problem is surprisingly elusive and it is hard to come up with a definition that does not involve many technical artifacts.
In this contribution, we give a definition of polynomial time for cryptographic protocols in the UC model, called reactively polynomial, that satisfies all five properties. Our notion is simple and easy to verify. We argue for its flexibility, completeness and soundness with practical examples that are problematic with previous approaches. We give a very general composition theorem for reactively polynomial protocols. The theorem states that arbitrarily many instances of a secure protocol can be used in any larger protocol without sacrificing security. Our proof is technically different from and substantially more involved than proofs for previous protocol composition theorems (for previous definitions of polynomial runtime). We believe that it is precisely this additional proof complexity, which appears only once and for all in the proof of the composition theorem, that makes a useful definition as simple as ours possible.

2008

EPRINT

Computational Soundness of Symbolic Zero-Knowledge Proofs Against Active Attackers
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 Dolev-Yao models offering the core cryptographic operations such as encryption and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. Recent work, however, has started to extend Dolev-Yao models to more sophisticated operations with unique security features. Zero-knowledge proofs arguably constitute the most amazing such extension.
In this paper, we first identify which additional properties a cryptographic zero-knowledge proof needs to fulfill in order to serve as a computationally sound implementation of symbolic (Dolev-Yao style) zero-knowledge proofs; this leads to the novel definition of a symbolically-sound zero-knowledge proof system. We prove that even in the presence of arbitrary active adversaries, such proof systems constitute computationally sound implementations of symbolic zero-knowledge proofs. This yields the first computational soundness result for symbolic zero-knowledge proofs and the first such result against fully active adversaries of Dolev-Yao models that go beyond the core cryptographic operations.

2007

EPRINT

Random Oracles and Auxiliary Input
Abstract

We introduce a variant of the random oracle model where oracle-dependent auxiliary input is allowed. In this setting, the adversary gets an auxiliary input that can contain information about the random oracle. Using simple examples we show that this model should be preferred over the classical variant where the auxiliary input is independent of the random oracle.
In the presence of oracle-dependent auxiliary input, the most important proof technique in the random oracle model - lazy sampling - does not apply directly. We present a theorem and a variant of the lazy sampling technique that allows one to perform proofs in the new model almost as easily as in the old one.
As an application of our approach and to illustrate how existing proofs can be adapted, we prove that RSA-OAEP is IND-CCA2 secure in the random oracle model with oracle-dependent auxiliary input.

2007

EPRINT

On the Security of Protocols with Logarithmic Communication Complexity
Abstract

We investigate the security of protocols with logarithmic
communication complexity. We show that for the security definitions
with environment, i.e., Reactive Simulatability and Universal
Composability, computational security of logarithmic protocols implies
statistical security. The same holds for advantage-based security
definitions as commonly used for individual primitives. While this
matches the folklore that logarithmic protocols cannot be
computationally secure unless they are already statistically secure,
we show that under realistic complexity assumptions, this folklore
does surprisingly not hold for the stand-alone model without
auxiliary input, i.e., there are logarithmic protocols that are
statistically insecure but computationally secure in this model. The
proof is conducted by showing how to transform an instance of an
NP-complete problem into a protocol with two properties: There exists
an adversary such that the protocol is statistically insecure in the
stand-alone model, and given such an adversary we can find a witness
for the problem instance, hence yielding a computationally secure
protocol assuming the hardness of finding a witness. The proof relies
on a novel technique that establishes a link between cryptographic
definitions and foundations of computational geometry, which we
consider of independent interest.

2007

EPRINT

Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol
Abstract

We devise an abstraction of zero-knowledge protocols that is
accessible to a fully mechanized analysis. The abstraction is
formalized within the applied pi-calculus using a novel equational
theory that abstractly characterizes the cryptographic semantics of
zero-knowledge proofs. We present an encoding from the equational
theory into a convergent rewriting system that is suitable for the
automated protocol verifier ProVerif. The encoding is sound and fully
automated. We successfully used ProVerif to obtain the first
mechanized analysis of the Direct Anonymous Attestation (DAA)
protocol. The analysis in particular required us to devise novel
abstractions of sophisticated cryptographic security definitions based
on interactive games.

2007

EPRINT

Towards Key-Dependent Message Security in the Standard Model
Abstract

Standard security notions for encryption schemes do not guarantee any security if the encrypted messages depend on the secret key. Yet it is exactly the stronger notion of security in the presence of *key-dependent* messages (KDM security) that is required in a number of applications: most prominently, KDM security plays an important role in analyzing cryptographic multi-party protocols in a formal calculus. But although often assumed, the mere existence of KDM secure schemes is an open problem. The only previously known construction was proven secure in the random oracle model.
We present symmetric encryption schemes that are KDM secure in the standard model (i.e., without random oracles). The price we pay is that we achieve only a relaxed (but still useful) notion of key-dependent message security. Our work answers (at least partially) an open problem posed by Black, Rogaway, and Shrimpton. More concretely, our contributions are as follows:
- We present a (stateless) symmetric encryption scheme that is information-theoretically secure in face of a *bounded* number and length of encryptions for which the messages depend in an arbitrary way on the secret key.
- We present a stateful symmetric encryption scheme that is computationally secure in face of an arbitrary number of encryptions for which the messages depend only on the respective *current* secret state/key of the scheme. The underlying computational assumption is minimal: we assume the existence of one-way functions.
- We give evidence that the only previously known KDM secure encryption scheme cannot be proven secure in the standard model (i.e., without random oracles).

2006

EPRINT

Simulatable Security and Polynomially Bounded Concurrent Composition
Abstract

Simulatable security is a security notion for multi-party protocols that implies strong composability features. The main definitional flavours of simulatable security are standard simulatability, universal simulatability, and black-box simulatability. All three come in "computational," "statistical" and "perfect" subflavours indicating the considered adversarial power. Universal and black-box simulatability, in all of their subflavours, are already known to guarantee that the concurrent composition even of a polynomial number of secure protocols stays secure.
We show that computational standard simulatability does not allow for secure concurrent composition of polynomially many protocols, but we also show that statistical standard simulatability does. The first result assumes the existence of an interesting cryptographic tool (namely time-lock puzzles), and its proof employs a cryptographic multi-party computation in an interesting and unconventional way.

2006

EPRINT

On the (Im-)Possibility of Extending Coin Toss
Abstract

We consider the cryptographic two-party protocol task of extending a given coin toss. The goal is to generate n common random coins from a single use of an ideal functionality which gives m<n common random coins to the parties. In the framework of Universal Composability we show the impossibility of securely extending a coin toss for statistical and perfect security. On the other hand, for computational security the existence of a protocol for coin toss extension depends on the number m of random coins which can be obtained "for free".
For the case of stand-alone security, i.e., a simulation based security definition without an environment, we present a novel protocol for unconditionally secure coin toss extension. The new protocol works for superlogarithmic m, which is optimal as we show the impossibility of statistically secure coin toss extension for smaller m.
Combining our results with already known results, we obtain a (nearly) complete characterization under which circumstances coin toss extension is possible.

2006

EPRINT

On the Necessity of Rewinding in Secure Multiparty Computation
Abstract

We investigate whether security of multiparty computation in the information-theoretic setting implies their security under concurrent composition. We show that security in the stand-alone model proven using black-box simulators in the information-theoretic setting does not imply security under concurrent composition, not even security under 2-bounded concurrent self-composition with an inefficient simulator and fixed inputs. This in particular refutes recently made claims on the equivalence of security in the stand-alone model and concurrent composition for perfect and statistical security (STOC'06). Our result strongly relies on the question whether every rewinding simulator can be transformed into an equivalent, potentially inefficient non-rewinding (straight-line) simulator. We answer this question in the negative by giving a protocol that can be proven secure using a rewinding simulator, yet that is not secure for any non-rewinding simulator.

2006

EPRINT

Long-term Security and Universal Composability
Abstract

Algorithmic progress and future technological advances threaten
today's cryptographic protocols. This may allow adversaries to break a
protocol retrospectively by breaking the underlying complexity
assumptions long after the execution of the protocol. Long-term secure
protocols, protocols that after the end of the execution do not reveal
any information to a then possibly unlimited adversary, could meet
this threat. On the other hand, in many applications, it is necessary
that a protocol is secure not only when executed alone, but within
arbitrary contexts. The established notion of universal composability
(UC) captures this requirement.
This is the first paper to study protocols which are simultaneously
long-term secure and universally composable. We show that the usual
set-up assumptions used for UC protocols (e.g., a common reference
string) are not sufficient to achieve long-term secure and composable
protocols for commitments or zero-knowledge protocols.
We give practical alternatives (e.g., signature cards) to these usual
setup-assumptions and show that these enable the implementation of the
important primitives commitment and zero-knowledge protocols.

2005

EPRINT

On the Notion of Statistical Security in Simulatability Definitions
Abstract

We investigate the definition of statistical security (i.e.,
security against unbounded adversaries) in the framework of reactive
simulatability. This framework allows to formulate and analyze
multi-party protocols modularly by providing a composition theorem
for protocols. However, we show that the notion of statistical
security, as defined by Backes, Pfitzmann and Waidner for the
reactive simulatability framework, does not allow for secure
composition of protocols. This in particular invalidates the proof
of the composition theorem.
We give evidence that the reason for the non-composability of
statistical security is no artifact of the framework itself, but of
the particular formulation of statistical security. Therefore, we
give a modified notion of statistical security in the reactive
simulatability framework. We prove that this notion allows for
secure composition of protocols.
As to the best of our knowledge, no formal definition of statistical
security has been fixed for Canetti's universal composability
framework, we believe that our observations and results can also
help to avoid potential pitfalls there.

2005

EPRINT

On Fairness in Simulatability-based Cryptographic Systems
Abstract

Simulatability constitutes the cryptographic notion of a secure refinement and has asserted its position as one of the fundamental concepts of modern cryptography. Although simulatability carefully captures that a distributed protocol does not behave any worse than an ideal specification, it however does not capture any form of liveness guarantees, i.e., that something good eventually happens in the protocol.
We show how one can extend the notion of simulatability to comprise liveness guarantees by imposing specific fairness constraints on the adversary. As the common notion of fairness based on infinite runs and eventual message delivery is not suited for reasoning about polynomial-time, cryptographic systems, we propose a new definition of fairness that enforces the delivery of messages after a polynomial number of steps. We provide strengthened variants of this definition by granting the protocol parties explicit guarantees on the maximum delay of messages. The variants thus capture fairness with explicit timeout signals, and we further distinguish between fairness with local timeouts and fairness with global timeouts.
We compare the resulting notions of fair simulatability, and provide separating examples that help to classify the strengths of the definitions and that show that the different definitions of fairness imply different variants of simulatability.

2005

EPRINT

Relations amount Statistical Security Notions - or - Why Exponential Adversaries are Unlimited
Abstract

In the context of Universal Composability, we introduce the concept of universal environments and simulators. Then, Universal Composability is equivalent to Universal Composability wrt. universal environments and simulators.
We prove the existence of universal environments and simulators and investigate their computational complexity.
From this, we get a number of consequences: First, we see that for polynomial-time protocols, exponential adversarial entities are as powerful as unlimited ones.
Further, for a large class of protocols (those with bounded communication-complexity) we can show that UC and specialised-simulator UC coincide in the case of statistical security, i.e., that it is does not matter whether the simulator is chosen in dependence of the environment or not. This also implies that for the Universal Composition Theorem for polynomial-time protocols specialised-simulator UC is sufficient.
This result is the last piece needed to find all implications and non-implications between the notions of UC, specialised-simulator UC, O(1)-bounded and polynomially-bounded general composability for polynomial-time protocols in the cases of perfect, statistical and polynomial security.
Finally, we introduce the notion of bounded-risk UC, which allows to give explicit security guarantees for concrete security parameters and show that in the above case also this variant coincides with UC.

#### Program Committees

- Asiacrypt 2018
- Eurocrypt 2018
- Crypto 2017
- Asiacrypt 2017
- Eurocrypt 2016
- Asiacrypt 2016
- Asiacrypt 2015
- PKC 2014
- Eurocrypt 2014
- Crypto 2012
- TCC 2011

#### Coauthors

- Andris Ambainis (1)
- Michael Backes (10)
- Markus Dürmuth (1)
- Sanjam Garg (1)
- Dennis Hofheinz (11)
- Matteo Maffei (2)
- Jörn Müller-Quade (11)
- Vanishree Rao (1)
- Ansis Rosmanis (1)
- Amit Sahai (1)
- Dominique Schröder (3)
- Ehsan Ebrahimi Targhi (1)