See also the list of talks.
Abstract: We formalize security properties of zero-knowledge protocols and their proofs in EasyCrypt. Specifically, we focus on sigma protocols (three-round protocols). Most importantly, we also cover properties whose security proofs require the use of rewinding; prior work has focused on properties that do not need this more advanced technique. On our way we give generic definitions of the main properties associated with sigma protocols, both in the computational and information-theoretical setting. We give generic derivations of soundness, (malicious- verifier) zero-knowledge, and proof of knowledge from simpler assumptions with proofs which rely on rewinding. Also, we address sequential composition of sigma protocols. Finally, we illustrate the applicability of our results on three zero-knowledge protocols: Fiat-Shamir (for quadratic residues), Schnorr (for discrete logarithms), and Blum (for Hamiltonian cycles, NP- complete).
Permalink: http://www.ut.ee/~unruh/publications/zk-easycrypt.html
Abstract: We implement the Schnorr protocol in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge and zero-knowledge properties) and the absence of leakage through timing side-channels of that implementation in EasyCrypt.
In order to do so, we provide a semantic characterization of leakage-freeness for probabilistic Jasmin programs (that are not constant-time). We design a library for multiple-precision integer arithmetic in Jasmin – the "libjbn" library. Among others, we implement and verify algorithms for fast constant-time modular multiplication and exponentiation (using Barrett reduction and Montgomery ladder). We also implement and verify correctness and leakage-freeness of the rejection sampling algorithm. And finally, we put it all together and show the security of the overall implementation (end-to-end verification) of the Schnorr protocol, by connecting our implementation to prior security analyses in EasyCrypt (Firsov, Unruh, CSF 2023).
Permalink: http://www.ut.ee/~unruh/publications/jasmin-schnorr.html
Abstract: Compressed oracles (Zhandry, Crypto 2019) are a powerful technique to reason about quantum random oracles, enabling a sort of lazy sampling in the presence of superposition queries. A long-standing open question is whether a similar technique can also be used to reason about random (efficiently invertible) permutations.
In this work, we make a step towards answering this question. We first define the compressed permutation oracle and illustrate its use. While the soundness of this technique (i.e., the indistinguishability from a random permutation) remains a conjecture, we show a curious 2-for-1 theorem: If we use the compressed permutation oracle methodology to show that some construction (e.g., Luby-Rackoff) implements a random permutation (or strong qPRP), then we get the fact that this methodology is actually sound for free.
Permalink: http://www.ut.ee/~unruh/publications/towards-cpo.html
Abstract: Cryptography based on the hardness of lattice problems over polynomial rings currently provides the most practical solution for pub- lic key encryption in the quantum era. Indeed, three of the four schemes chosen by NIST in the recently-concluded post-quantum standardization effort for encryption and signature schemes are based on the hardness of these problems. While the first encryption scheme utilizing properties of polynomial rings was NTRU (ANTS ’98), the scheme that NIST chose for public key encryption (CRYSTALS-Kyber) is based on the hardness of the somewhat-related Module-LWE problem. One of the reasons for Kyber’s selection was the fact that it is noticeably faster than NTRU and a little more compact. And indeed, the practical NTRU encryption schemes in the literature generally lag their Ring/Module-LWE counter- parts in either compactness or speed, or both.
In this paper, we put the efficiency of NTRU-based schemes on equal (even slightly better, actually) footing with their Ring/Module-LWE counterparts. We provide several instantiations and transformations, with security given in the ROM and the QROM, that are on par, compactness- wise, with their counterparts based on Ring/Module-LWE. Performance- wise, the NTRU schemes instantiated in this paper over NTT-friendly rings of the form Z_q[X]/(X^d − X^{d/2} + 1) are the fastest of all public key encryption schemes, whether quantum-safe or not. When compared to the NIST finalist NTRU-HRSS-701, our scheme is 15% more compact and has a 15X improvement in the round-trip time of ephemeral key exchange, with key generation being 35X faster, encapsulation being 6X faster, and decapsulation enjoying a 9X speedup.
Abstract: The concept of quantum bit commitment was introduced in the early 1980s for the purpose of basing bit commitment solely on principles of quantum theory. Unfortunately, such unconditional quantum bit commitment still turns out to be impossible. As a compromise like in classical cryptography, Dumais, Mayers and Salvail [DMS00] introduce and realize the conditional quantum bit commitment that additionally relies on complexity assumptions. However, in contrast to the classical bit commitment which is widely used in classical cryptography, up until now there is relatively little work towards studying the application of quantum bit commitment in quantum cryptography. This may be partly due to the well-known weakness of the quantum binding, making it unclear whether quantum bit commitment could be used as a primitive (like its classical counterpart) in quantum cryptography.
As the first step towards studying the possible application of quantum bit commitment in quantum cryptography, in this work we consider replacing the classical bit commitment used in some well-known constructions with a perfectly/statistically-binding quantum bit commitment. We show that (quantum) security can still be fulfilled in particular with respect to zero-knowledge, oblivious transfer, and proofs-of-knowledge. In spite of this, we stress that the corresponding security analyses are by no means a trivial adaptation of their classical counterparts. New techniques are needed to handle possible superposition attacks by the cheating sender of the quantum bit commitments.
Since non-interactive quantum bit commitment schemes can be constructed from general quantum-secure one-way functions, we hope to use quantum bit commitment (rather than the classical one that is still quantum-secure) in cryptographic construction to reduce the round complexity and weaken the complexity assumption simultaneously.
Permalink: http://www.ut.ee/~unruh/publications/statistical-qbc.html
Abstract: Quantum relational Hoare logic (qRHL) is a Hoare logic for analyzing pairs of quantum programs and their relationship. Concretely, it allows us to describe how the outputs relate if the inputs satisfy a certain precondition. We describe qRHL, explain its connection to the verification of quantum cryptography, and mention some of the challenges in its use. We describe current progress towards the formalization of qRHL (in Isabelle/HOL) and what the difficulties are.
Permalink: http://www.ut.ee/~unruh/publications/planqc-qrhl.html
Abstract: The random oracle is a popular heuristic in classical security proofs that allows us to construct simpler and more efficient schemes and get simpler proofs in many situations. (At the expense of some soundness.) In the quantum setting, using the random oracle is, unfortunately, much harder. Many of the classical proof techniques break down, their replacements are considerably more complex, if they even exist. But still, the quantum random oracle is a useful technique, and recent years have seen considerable advances in proof techniques in the quantum random oracle model. This lecture will introduce the model and some of the most important proof techniques.
Permalink: http://www.ut.ee/~unruh/publications/ipam-quantum-ro.html
Abstract: Everlasting security models the setting where hardness assumptions hold during the execution of a protocol but may get broken in the future. Due to the strength of this adversarial model, achieving any meaningful security guarantees for composable protocols is impossible without relying on hardware assumptions (Müller-Quade and Unruh, JoC’10). For this reason, a rich line of research has tried to leverage physical assumptions to construct well-known everlasting cryptographic primitives, such as commitment schemes. The only known everlastingly UC secure commitment scheme, due to Müller-Quade and Unruh (JoC’10), assumes honestly generated hardware tokens. The authors leave the possibility of constructing everlastingly UC secure commitments from malicious hardware tokens as an open problem. Goyal et al. (Crypto’10) constructs unconditionally UC-secure commitments and secure computation from malicious hardware tokens, with the caveat that the honest tokens must encapsulate other tokens. This extra restriction rules out interesting classes of hardware tokens, such as physically uncloneable functions (PUFs). In this work, we present the first construction of an everlastingly UC-secure commitment scheme in the fully malicious token model without requiring honest token encapsulation. Our scheme assumes the existence of PUFs and is secure in the common reference string model. We also show that our results are tight by giving an impossibility proof for everlasting UC-secure computation from non-erasable tokens (such as PUFs), even with trusted setup.
Permalink: http://www.ut.ee/~unruh/publications/everlasting-puf.html
Abstract: Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grover's search, and recursive quantum Fourier sampling.
Permalink: http://www.ut.ee/~unruh/publications/recursive-quantum.html
Abstract: In this paper we derive a suite of lemmas which allows users to internally reflect EasyCrypt programs into distributions which correspond to their denotational semantics (probabilistic reflection). Based on this we develop techniques for reasoning about rewinding of adversaries in EasyCrypt. (A widely used technique in cryptology.) We use our reflection and rewindability results to prove the security of a coin-toss protocol.
Permalink: http://www.ut.ee/~unruh/publications/ec-rewinding.html
Abstract: An encryption scheme is called indistinguishable under chosen plaintext attack (short IND-CPA) if an attacker cannot distinguish the encryptions of two messages of his choice. There are other variants of this definition but they all turn out to be equivalent in the classical case. In this paper, we give a comprehensive overview of these different variants of IND-CPA for symmetric encryption schemes in the quantum setting. We investigate the relationships between these notions and prove various equivalences, implications, non-equivalences, and non-implications between these variants.
Permalink: http://www.ut.ee/~unruh/publications/qindcpa.html
Permalink: http://www.ut.ee/~unruh/publications/registers-afp.html
Permalink: http://www.ut.ee/~unruh/publications/quiques-rewinding.html
Permalink: http://www.ut.ee/~unruh/publications/bounded-ops-afp.html
Abstract: We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pairs of programs, our logic allows us to quantitatively reason about how much certain pre-/postconditions are satisfied that refer to the relationship between the programs inputs/outputs.
Permalink: http://www.ut.ee/~unruh/publications/expectation-qrhl.html
Abstract: We present a generic theory of "registers" in imperative programs and instantiate it in the classical and quantum setting. Roughly speaking, a register is some mutable part of the program state, e.g., mutable classical variables and quantum registers and wires in quantum circuits are examples of this. However, registers in our setting can also refer to subparts of other registers, or combinations of parts from different registers, or quantum registers seen in a different basis, etc. Our formalization is intended to be well suited for formalization in theorem provers and as a foundation for modeling quantum/classical variables in imperative programs.
We implemented most results (including a minimal quantum Hoare logic and an analysis of quantum teleportation) in the Isabelle/HOL theorem prover.
Permalink: http://www.ut.ee/~unruh/publications/registers.html
Abstract: We generalize Zhandry's compressed oracle technique to invertible random permutations. (That is, to a quantum random oracle where the adversary has access to a random permutation and its inverse.) This enables security proofs with lazy sampling, i.e., where oracle outputs are chosen only when needed. As an application of our technique, we show the collision-resistance of the sponge construction based on invertible permutations. In particular, this shows the collision-resistance of SHA3 (in the random oracle model).
Permalink: http://www.ut.ee/~unruh/publications/compressed-permutations.html
Abstract: This draft was intended to give a formal treatment of Zhandry's results on recording quantum queries, with all definitions and proofs worked out. It is unfinished and there are currently no plans to finish it. However, since the manuscript has been cited in some places, we provide this incomplete draft as-is for reference.
Permalink: http://www.ut.ee/~unruh/publications/recording-qq.html
Abstract: We present a computer-verified formalization of the post-quantum security proof of the Fujisaki-Okamoto transform (as analyzed by Hövelmanns, Kiltz, Schäge, Unruh, Generic Authenticated Key Exchange in the Quantum Random Oracle Model, 2020). The formalization is done in quantum relational Hoare logic and checked in the qrhl-tool (Unruh, Quantum Relational Hoare Logic, 2019).
Permalink: http://www.ut.ee/~unruh/publications/hksu-verify.html
Abstract: We add local variables to quantum relational Hoare logic (Unruh, POPL 2019). We derive reasoning rules for supporting local variables (including an improved "adversary rule"). We extended the qrhl-tool for computer-aided verification of qRHL to support local variables and our new reasoning rules.
Permalink: http://www.ut.ee/~unruh/publications/qrhl-local.html
Abstract: The concept of quantum bit commitment was introduced in the early 1980s for the purpose of basing bit commitment solely on principles of quantum theory. Unfortunately, such unconditional quantum bit commitment still turns out to be impossible. As a compromise like in classical cryptography, Dumais, Mayers and Salvail [DMS00] introduce and realize the conditional quantum bit commitment that additionally relies on complexity assumptions. However, in contrast to the classical bit commitment which is widely used in classical cryptography, up until now there is relatively little work towards studying the application of quantum bit commitment in quantum cryptography. This may be partly due to the well-known weakness of the quantum binding, making it unclear whether quantum bit commitment could be used as a primitive (like its classical counterpart) in quantum cryptography.
As the first step towards studying the possible application of quantum bit commitment in quantum cryptography, in this work we consider replacing the classical bit commitment used in some well-known constructions with a perfectly/statistically-binding quantum bit commitment. We show that (quantum) security can still be fulfilled in particular with respect to zero-knowledge, oblivious transfer, and proofs-of-knowledge. In spite of this, we stress that the corresponding security analyses are by no means a trivial adaptation of their classical counterparts. New techniques are needed to handle possible superposition attacks by the cheating sender of the quantum bit commitments.
Since non-interactive quantum bit commitment schemes can be constructed from general quantum-secure one-way functions, we hope to use quantum bit commitment (rather than the classical one that is still quantum-secure) in cryptographic construction to reduce the round complexity and weaken the complexity assumption simultaneously.
Permalink: http://www.ut.ee/~unruh/publications/statistical-qbc.html
Abstract: We propose FO_AKE, a generic construction of two-message authenticated key exchange (AKE) from any passively secure public key encryption (PKE) in the quantum random oracle model (QROM). Whereas previous AKE constructions relied on a Diffie-Hellman key exchange or required the underlying PKE scheme to be perfectly correct, our transformation allows arbitrary PKE schemes with non-perfect correctness. Dealing with imperfect schemes is one of the major difficulties in a setting involving active attacks. Our direct construction, when applied to schemes such as the submissions to the recent NIST post-quantum competition, is more natural than previous AKE transformations. Furthermore, we avoid the use of (quantum-secure) digital signature schemes which are considerably less efficient than their PKE counterparts. As a consequence, we can instantiate our AKE transformation with any of the submissions to the recent NIST competition, e.g., ones based on codes and lattices.
FO_AKE can be seen as a generalisation of the well known Fujisaki-Okamoto transformation (for building actively secure PKE from passively secure PKE) to the AKE setting. As a helper result, we also provide a security proof for the Fujisaki-Okamoto transformation in the QROM for PKE with non-perfect correctness which is tighter and tolerates a larger correctness error than previous proofs.
Permalink: http://www.ut.ee/~unruh/publications/bounded-ops-afp.html
Abstract: We present an improved version of the one-way to hiding (O2H) Theorem by Unruh, J ACM 2015. Our new O2H Theorem gives higher flexibility (arbitrary joint distributions of oracles and inputs, multiple reprogrammed points) as well as tighter bounds (removing square-root factors, taking parallelism into account). The improved O2H Theorem makes use of a new variant of quantum oracles, semi-classical oracles, where queries are partially measured. The new O2H Theorem allows us to get better security bounds in several public-key encryption schemes.
Permalink: http://www.ut.ee/~unruh/publications/semiclassical.html
Abstract: Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces "ghost variables" to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually occur in the program and are allowed to have arbitrary quantum states (in a sense, they are existentially quantified), and be entangled with program variables. Ghost variables allow us to express properties such as the distribution of a program variable or the fact that a variable has classical content. And as a case study, we show how quantum Hoare logic with ghost variables can be used to prove the security of the quantum one-time pad.
Abstract: We present a logic for reasoning about pairs of imperative quantum programs – quantum relational Hoare logic (qRHL). This logic follows the spirit of probabilistic relational Hoare logic (Barthe et al. 2009) and allows us to formulate how the outputs of two quantum programs relate given the relationship of their inputs. Probabilistic RHL was used extensively for computer-verified security proofs of classical cryptographic protocols. Since pRHL is not suitable for analyzing quantum cryptography, we present qRHL as a replacement, suitable for the security analysis of post-quantum cryptography and quantum protocols. The design of qRHL poses some challenges unique to the quantum setting, e.g., the definition of equality on quantum registers. Finally, we implemented a tool for verifying proofs in qRHL and developed several example security proofs in it.
Abstract: We study the quantum query complexity of finding a collision for a function f whose outputs are chosen according to a non-uniform distribution D. We derive some upper bounds and lower bounds depending on the min-entropy and the collision-entropy of D. In particular, we improve the previous lower bound in Targhi, Tabia, Unruh, Quantum Collision-Resistance of Non-Uniformly Distributed Functions, 2016 from Ω(2^{k/9}) to Ω(2^{k/5}) where k is the min-entropy of D.
Permalink: http://www.ut.ee/~unruh/publications/collision2.html
Abstract: We consider the task of extending a given coin toss. By this, we mean the two-party task of using a single instance of a given coin toss protocol in order to interactively generate \emph{more} random coins. A bit more formally, our goal is to generate $n$ common random coins from a single use of an ideal functionality that gives $m<n$ common random coins to both 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 that can be obtained "for free".
For the case of standalone security, i.e., a simulation based security definition without an environment, we present a protocol for statistically secure coin toss extension. Our 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.
Short version is Hofheinz, Müller-Quade, Unruh, On the (Im-)Possibility of Extending Coin Toss, 2006.
Permalink: http://www.ut.ee/~unruh/publications/cointoss-joc.html
Abstract: We investigate the post-quantum security of hash functions based on the sponge construction. A crucial property for hash functions in the post-quantum setting is the collapsing property (a strengthening of collision-resistance). We show that the sponge construction is collapsing (and in consequence quantum collision-resistant) under suitable assumptions about the underlying block function. In particular, if the block function is a random function or a (non-invertible) random permutation, the sponge construction is collapsing.
(Merger of Unruh, Collapsing sponges: Post-quantum security of the sponge construction, 2017 and Czajkowski, Bruinderink, Hülsing, Schaffner, Quantum preimage, 2nd-preimage, and collision resistance of SHA3, 2017.)
Permalink: http://www.ut.ee/~unruh/publications/sponge2.html
Abstract: We study the indifferentiability of classical constructions in the quantum setting, such as the Sponge construction or Feistel networks. (But the approach easily generalizes to other constructions, too.) We give evidence that, while those constructions are known to be indifferentiable in the classical setting, they are not indifferentiable in the quantum setting. Our approach is based on a quantum-information-theoreoretical conjecture.
Permalink: http://www.ut.ee/~unruh/publications/qindiff.html
Abstract: A protocol has everlasting security if it is secure against adversaries that are computationally unlimited after the protocol execution. This models the fact that we cannot predict which cryptographic schemes will be broken, say, several decades after the protocol execution. In classical cryptography, everlasting security is difficult to achieve: even using trusted setup like common reference strings or signature cards, many tasks such as secure communication and oblivious transfer cannot be achieved with everlasting security. An analogous result in the quantum setting excludes protocols based on common reference strings, but not protocols using a signature card. We define a variant of the Universal Composability framework, everlasting quantum-UC, and show that in this model, we can implement secure communication and general multi-party computation using signature cards as trusted setup.
Permalink: http://www.ut.ee/~unruh/publications/qeverlasting-joc.html
Abstract: The Fiat-Shamir construction (Crypto 1986) is an efficient transformation in the random oracle model for creating non-interactive proof systems and signatures from sigma-protocols. In classical cryptography, Fiat-Shamir is a zero-knowledge proof of knowledge assuming that the underlying sigma-protocol has the zero-knowledge and special soundness properties. Unfortunately, Ambainis, Rosmanis, and Unruh (FOCS 2014) ruled out non-relativizing proofs under those conditions in the quantum setting.
In this paper, we show under which strengthened conditions the Fiat-Shamir proof system is still post-quantum secure. Namely, we show that if we require the sigma-protocol to have computational zero-knowledge and statistical soundness, then Fiat-Shamir is a zero-knowledge simulation-sound proof system (but not a proof of knowledge!). Furthermore, we show that Fiat-Shamir leads to a post-quantum secure unforgeable signature scheme when additionally assuming a "dual-mode hard instance generator" for generating key pairs.
Abstract: We revisit the security definitions of blind signatures as proposed by Pointcheval and Stern (J Cryptol 13(3):361–396, 2000). Security comprises the notions of one-more unforgeability, preventing a malicious user to generate more signatures than requested, and of blindness, averting a malicious signer to learn useful information about the user’s messages. Although this definition is well established nowadays, we show that there are still desirable security properties that fall outside of the model. More precisely, in the original unforgeability definition is not excluded that an adversary verifiably uses the same message m for signing twice and is then still able to produce another signature for a new message m′≠m. Intuitively, this should not be possible; yet, it is not captured in the original definition, because the number of signatures equals the number of requests. We thus propose a stronger notion, called honest-user unforgeability, that covers these attacks. We give a simple and efficient transformation that turns any unforgeable blind signature scheme (with deterministic verification) into an honest-user unforgeable one.
Permalink: http://www.ut.ee/~unruh/publications/bsrevisit-joc.html
Abstract: We investigate the post-quantum security of hash functions based on the sponge construction. A crucial property for hash functions in the post-quantum setting is the collapsing property (a strengthening of collision-resistance). We show that the sponge construction is collapsing (and in consequence quantum collision-resistant) under suitable assumptions about the underlying block function. In particular, if the block function is a random function or a (non-invertible) random permutation, the sponge construction is collapsing.
Abstract: In this paper, we present a hybrid encryption scheme that is chosen ciphertext secure in the quantum random oracle model. Our scheme is a combination of an asymmetric and a symmetric encryption scheme that are secure in a weak sense. It is a slight modification of the Fujisaki-Okamoto transform that is secure against classical adversaries. In addition, we modify the OAEP-cryptosystem and prove its security in the quantum random oracle model based on the existence of a partial-domain one-way injective function secure against quantum adversaries.
Permalink: http://www.ut.ee/~unruh/publications/fujioka.html
Abstract: Unlike classical money, which is hard to forge for practical reasons (e.g. producing paper with a certain property), quantum money is attractive because its security might be based on the no-cloning theorem. The first quantum money scheme was introduced by Wiesner circa 1970. Although more sophisticated quantum money schemes were proposed, Wiesner's scheme remained appealing because it is both conceptually clean and relatively easy to implement.
We show efficient adaptive attacks on Wiesner's quantum money scheme (and its variant by Bennett et al.), when valid money is accepted and passed on, while invalid money is destroyed. We propose two attacks, the first is inspired by the Elitzur-Vaidman bomb testing problem, while the second is based on the idea of protective measurements. It allows us to break Wiesner's scheme with 4 possible states per qubit, and generalizations which use more than 4 states per qubit.
Permalink: http://www.ut.ee/~unruh/publications/adaptive-money.html
Abstract: We construct collapse-binding commitments in the standard model. Collapse-binding commitments were introduced by Unruh, Computationally binding quantum commitments, 2016 to model the computational-binding property of commitments against quantum adversaries, but only constructions in the random oracle model were known.
Furthermore, we show that collapse-binding commitments imply selected other security definitions for quantum commitments, answering an open question by (Unruh 2016).
Permalink: http://www.ut.ee/~unruh/publications/collapse-std.html
Abstract: We present a new definition of computationally binding commitment schemes in the quantum setting, which we call "collapse-binding". The definition applies to string commitments, composes in parallel, and works well with rewinding-based proofs. We give simple constructions of collapse-binding commitments in the random oracle model, giving evidence that they can be realized from hash functions like SHA-3. We evidence the usefulness of our definition by constructing three-round statistical zero-knowledge quantum arguments of knowledge for all NP languages.
Permalink: http://www.ut.ee/~unruh/publications/collapse.html
Abstract: We introduce a variant of the Universal Composability framework (UC; Canetti, FOCS 2001) that uses symbolic cryptography. Two salient properties of the UC framework are secure composition and the possibility of easily defining security by giving an ideal functionality as specification. These advantages are now also available in a symbolic modeling of cryptography, allowing for a modular analysis of complex protocols.
We furthermore introduce a new technique for modular design of protocols that uses UC but avoids the need for powerful cryptographic primitives that often comes with UC protocols; this "virtual primitives" approach is unique to the symbolic setting and has no counterpart in the original computational UC framework.
Permalink: http://www.ut.ee/~unruh/publications/symbolic-uc-jcs.html
Abstract: We study the quantum query complexity of finding a collision for a function f whose outputs are chosen according to a distribution with min-entropy k. We prove that $Ω(2^{k/9})$ quantum queries are necessary to find a collision for function f. This is needed in some security proofs in the quantum random oracle model (e.g. the Fujisaki-Okamoto transform).
Permalink: http://www.ut.ee/~unruh/publications/collision.html
Abstract: We examine the IND-qCPA security of the wide-spread block cipher modes of operation CBC, CFB, OFB, CTR, and XTS (i.e., security against quantum adversaries doing queries in superposition).
We show that OFB and CTR are secure assuming that the underlying block cipher is a standard secure PRF (a pseudorandom function secure under classical queries). We give counterexamples that show that CBC, CFB, and XTS are not secure under the same assumption.
And we give proofs that CBC and CFB mode are secure if we assume a quantum secure PRF (secure under queries in superposition).
Abstract: Timed-release encryption is a kind of encryption scheme that a recipient can decrypt only after a specified amount of time T (assuming that we have a moderately precise estimate of his computing power). A revocable timed-release encryption is one where, before the time T is over, the sender can “give back” the timed-release encryption, provably loosing all access to the data. We show that revocable timed-release encryption without trusted parties is possible using quantum cryptography (while trivially impossible classically).
Along the way, we develop two proof techniques in the quantum random oracle model that we believe may have applications also for other protocols.
Finally, we also develop another new primitive, unknown recipient encryption, which allows us to send a message to an unknown/unspecified recipient over an insecure network in such a way that at most one recipient will get the message.
Permalink: http://www.ut.ee/~unruh/publications/qtc-jacm.html
Abstract: We study the quantum query complexity of finding a collision for a function $f$ whose outputs are chosen according to a distribution with min-entropy $k$. We prove that $Ω(2^{k/9})$ quantum queries are necessary to find a collision for function f.
Permalink: http://www.ut.ee/~unruh/publications/qcollision-qcrypt.html
Abstract: In this paper, we present a hybrid encryption scheme that is chosen ciphertext secure in the quantum random oracle model. Our scheme is a combination of an asymmetric and a symmetric encryption scheme that are secure in a weak sense. It is a slight modification of Fujisaki and Okamoto's transformation that is secure against classical adversaries.
Permalink: http://www.ut.ee/~unruh/publications/qfo-qcrypt.html
Abstract: Increasingly, modern cryptography (crypto) has moved beyond the problem of secure communication to a broader consideration of securing computation. The past thirty years have seen a steady progression of both theoretical and practical advances in designing cryptographic protocols for problems such as secure multiparty computation, searching and computing on encrypted data, verifiable storage and computation, statistical data privacy, and more. More recently, the programming-languages (PL) community has begun to tackle the same set of problems, but from a different perspective, focusing on issues such as language design (e.g., new features or type systems), formal methods (e.g., model checking, deductive verification, static and dynamic analysis), compiler optimizations, and analyses of side-channel attacks and information leakage. This seminar helped to cross-fertilize ideas between the PL and crypto communities, exploiting the synergies for advancing the development of secure computing, broadly speaking, and fostering new research directions in and across both communities.
Permalink: http://www.ut.ee/~unruh/publications/synergy.html
Abstract: We present a construction for non-interactive zero-knowledge proofs of knowledge in the random oracle model from general sigma-protocols. Our construction is secure against quantum adversaries. Prior constructions (by Fiat-Shamir and by Fischlin) are only known to be secure against classical adversaries, and Ambainis, Rosmanis, Unruh (FOCS 2014) gave evidence that those constructions might not be secure against quantum adversaries in general.
To prove security of our constructions, we additionally develop new techniques for adaptively programming the quantum random oracle.
Permalink: http://www.ut.ee/~unruh/publications/qro-nizk.html
Abstract: Quantum zero-knowledge proofs and quantum proofs of knowledge are inherently difficult to analyze because their security analysis uses rewinding. Certain cases of quantum rewinding are handled by the results by Watrous (SIAM J Comput, 2009) and Unruh (Eurocrypt 2012), yet in general the problem remains elusive. We show that this is not only due to a lack of proof techniques: relative to an oracle, we show that classically secure proofs and proofs of knowledge are insecure in the quantum setting.
More specifically, sigma-protocols, the Fiat-Shamir construction, and Fischlin's proof system are quantum insecure under assumptions that are sufficient for classical security. Additionally, we show that for similar reasons, computationally binding commitments provide almost no security guarantees in a quantum setting.
To show these results, we develop the "pick-one trick", a general technique that allows an adversary to find one value satisfying a given predicate, but not two.
Permalink: http://www.ut.ee/~unruh/publications/qpok-imposs.html
Abstract: We present a quantum position verification scheme in the random oracle model. In contrast to prior work, our scheme does not require bounded storage/retrieval/entanglement assumptions. We also give an efficient position-based authentication protocol. This enables secret and authenticated communication with an entity that is only identified by its position in space.
Abstract: Timed-release encryption is a kind of encryption scheme that a recipient can decrypt only after a specified amount of time T (assuming that we have a moderately precise estimate of his computing power). A revocable timed-release encryption is one where, before the time T is over, the sender can "give back" the timed-release encryption, provably loosing all access to the data. We show that revocable timed-release encryption without trusted parties is possible using quantum cryptography (while trivially impossible classically).
Along the way, we develop two proof techniques in the quantum random oracle model that we believe may have applications also for other protocols.
Finally, we also develop another new primitive, unknown recipient encryption, which allows us to send a message to an unknown/unspecified recipient over an insecure network in such a way that at most one recipient will get the message.
Abstract: A protocol has everlasting security if it is secure against adversaries that are computationally unlimited after the protocol execution. This models the fact that we cannot predict which cryptographic schemes will be broken, say, several decades after the protocol execution. In classical cryptography, everlasting security is difficult to achieve: even using trusted setup like common reference strings or signature cards, many tasks such as secure communication and oblivious transfer cannot be achieved with everlasting security. An analogous result in the quantum setting excludes protocols based on common reference strings, but not protocols using a signature card. We define a variant of the Universal Composability framework, everlasting quantum-UC, and show that in this model, we can implement secure communication and general multi-party computation using signature cards as trusted setup.
Permalink: http://www.ut.ee/~unruh/publications/qeverlasting.html
Abstract: We introduce a variant of the Universal Composability framework (UC; Canetti, FOCS 2001) that uses symbolic cryptography. Two salient properties of the UC framework are secure composition and the possibility of easily defining security by giving an ideal functionality as specification. These advantages are now also available in a symbolic modeling of cryptography, allowing for a modular analysis of complex protocols.
We furthermore introduce a new technique for modular design of protocols that uses UC but avoids the need for powerful cryptographic primitives that often comes with UC protocols; this "virtual primitives" approach is unique to the symbolic setting and has no counterpart in the original computational UC framework.
Permalink: http://www.ut.ee/~unruh/publications/symbolic-uc.html
Abstract: To formalize participants in cryptographic protocols, it is common to use probabilistic Turing machines. We point out subtleties in common definitions of probabilistic Turing machines, which imply that the common cryptographic operation of uniform random sampling in a finite set {1,...,s}⊆Z is in general not possible within this model. From a technical point of view, this invalidates in particular a standard proof of the perfect zero knowledge property of the popular graph isomorphism proof system. The observed limitation appears to be relevant for other cryptographic protocol analyses as well, and we suggest one possible tweak of the definition of a probabilistic Turing machine.
Abstract: The abstraction of cryptographic operations by term algebras, called symbolic models, is essential in almost all tool-supported methods for analyzing security protocols. Significant progress was made in proving that symbolic models offering basic cryptographic operations such as encryption and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. Even abstractions of sophisticated modern cryptographic primitives such as zero-knowledge (ZK) proofs were shown to have a computationally sound cryptographic realization, but only in ad-hoc formalisms and at the cost of placing strong assumptions on the underlying cryptography, which leaves only highly inefficient realizations.
In this paper, we make two contributions to this problem space. First, we identify weaker cryptographic assumptions that we show to be sufficient for computational soundness of symbolic ZK proofs. These weaker assumptions are fulfilled by existing efficient ZK schemes as well as generic ZK constructions. Second, we conduct all computational soundness proofs in CoSP, a recent framework that allows for casting computational soundness proofs in a modular manner, independent of the underlying symbolic calculi. Moreover, all computational soundness proofs conducted in CoSP automatically come with mechanized proof support through an embedding of the applied π-calculus.
Permalink: http://www.ut.ee/~unruh/publications/zk-cosp.html
Abstract: The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for verifying security protocols. Recently significant progress was made in establishing computational soundness results: these results prove that Dolev-Yao style models can be sound with respect to actual cryptographic realizations and security definitions. However, these results came at the cost of imposing various constraints on the set of permitted security protocols: e.g., dishonestly generated keys must not be used, key cycles need to be avoided, and many more. In a nutshell, the cryptographic security definitions did not adequately capture these cases, but were considered carved in stone; in contrast, the symbolic abstractions were bent to reflect cryptographic features and idiosyncrasies, thereby requiring adaptations of existing verification tools.
In this paper, we pursue the opposite direction: we consider a symbolic abstraction for public-key encryption and identify two cryptographic definitions called PROG-KDM (programmable key-dependent message) security and MKE (malicious-key extractable) security that we jointly prove to be sufficient for obtaining computational soundness without imposing assumptions on the protocols using this abstraction. In particular, dishonestly generated keys obtained from the adversary can be sent, received, and used. The definitions can be met by existing cryptographic schemes. This yields the first computational soundness result that holds for arbitrary protocols using this abstraction (in particular permitting to send and receive dishonestly generated keys), and that is accessible to all existing tools for reasoning about Dolev-Yao models without further adaptations.
Permalink: http://www.ut.ee/~unruh/publications/unrestr-soundness.html
Abstract: We present the notion of PROG-KDM security for public-key encryption schemes. This security notion captures both KDM security and revealing of secret keys (key corruptions) in a single definition. This is achieved by requiring the existence of a simulator that can program ciphertexts when a secret key is revealed, i.e., the simulator can delay the decision what plaintext is contained in what ciphertext to the moment where the ciphertext is opened. The definition is formulated in the random oracle model.
We show that PROG-KDM security can be achieved by showing that a natural and practical construction in the ideal cipher model is PROG-KDM secure (hybrid encryption using authenticated CBC encryption).
Permalink: http://www.ut.ee/~unruh/publications/progkdm.html
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 case of reactively polynomial time protocols and attacks.
Permalink: http://www.ut.ee/~unruh/publications/polytime-uc.html
Abstract: We revisit the definition of unforgeability of blind signatures as proposed by Pointcheval and Stern (Journal of Cryptology 2000). Surprisingly, we show that this established definition falls short in two ways of what one would intuitively expect from a secure blind signature scheme: It is not excluded that an adversary submits the same message $m$ twice for signing, and then produces a signature for m' != m. The reason is that the forger only succeeds if all messages are distinct. Moreover, it is not excluded that an adversary performs k signing queries and produces signatures on k+1 messages as long as each of these signatures does not pass verification with probability 1.
Finally, we proposed a new definition, honest-user unforgeability, that covers these attacks. We give a simple and efficient transformation that transforms any unforgeable blind signature scheme (with deterministic verification) into an honest-user unforgeable one.
Permalink: http://www.ut.ee/~unruh/publications/bsrevisit.html
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.
Abstract: Constructing round-optimal blind signatures in the standard model has been a long standing open problem. In particular, Fischlin and Schröder recently ruled out a large class of three-move blind signatures in the standard model (Eurocrypt'10). In particular, their result shows that finding security proofs for the well-known blind signature schemes by Chaum, and by Pointcheval and Stern in the standard model via black-box reductions is hard. In this work we propose the first round-optimal, i.e., two-move, blind signature scheme in the standard model (i.e., without assuming random oracles or the existence of a common reference string). Our scheme relies on the Decisional Diffie Hellman assumption and the existence of sub-exponentially hard 1-to-1 one way functions. This scheme is also secure in the concurrent setting.
Merger of Schröder, Unruh, Round Optimal Blind Signatures, 2011 and "Round Optimal Blind Signatures in the Standard Model" by Sanjam Garg, Vanishree Rao, and Amit Sahai.
Permalink: http://www.ut.ee/~unruh/publications/2roundbs.html
Abstract: We defined a new notion of computational indistinguishability: termination-insensitive computational indistinguishability (tic-indistinguishability). Tic-indistinguishability models indistinguishability with respect to distinguishers that cannot distinguish between termination and non-termination.
We sketch how the new notion allows to get computational soundness results of symbolic models for equivalence-based security properties (such as anonymity) for processes that contain loops, solving an open problem.
Permalink: http://www.ut.ee/~unruh/publications/ti-indist.html
Abstract: All known round optimal (i.e., two-move) blind signature schemes either need a common reference string, rely on random oracles, or assume the hardness of some interactive assumption. At Eurocrypt 2010, Fischlin and Schröder showed that a broad class of three-move blind signature scheme cannot be instantiated in the standard model based on any non-interactive assumption. This puts forward the question if round optimal blind signature schemes exist in the standard model. Here, we give a positive answer presenting the first round optimal blind signature scheme that is secure in the standard model without any setup assumptions. Our solution does not need interactive assumptions.
Merged into Schröder, Unruh, Garg, Rao, Sahai, Round Optimal Blind Signatures, 2011
Permalink: http://www.ut.ee/~unruh/publications/2roundbs-orig.html
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.
Permalink: http://www.ut.ee/~unruh/publications/bqsm-uc.html
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.
Permalink: http://www.ut.ee/~unruh/publications/rcf-soundness.html
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 (non-interactive) 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.
A preliminary version appeared at Backes, Unruh, Computational Soundness of Symbolic Zero-Knowledge Proofs Against Active Attackers, 2008.
Permalink: http://www.ut.ee/~unruh/publications/zk-soundness.html
Abstract: We present the UC/c framework, a general definition for secure and incoercible multi-party protocols. Our framework allows to model arbitrary reactive protocol tasks (by specifying an ideal functionality) and comes with a universal composition theorem. We show that given natural setup assumptions, we can construct incoercible two-party protocols realising arbitrary functionalities (with respect to static adversaries).
Permalink: http://www.ut.ee/~unruh/publications/unruh09ucc.html
Abstract: We give a simple example that there is no symbolic theory for exclusive or (XOR) that is computationally sound.
Permalink: http://www.ut.ee/~unruh/publications/sound-xor.html
Abstract: The Universal Composability model (UC) by Canetti (FOCS 2001) allows for secure composition of arbitrary protocols. We present a quantum version of the UC model which enjoys the same compositionality guarantees. We prove that in this model statistically secure oblivious transfer protocols can be constructed from commitments. Furthermore, we show that every statistically classically UC secure protocol is also statistically quantum UC secure. Such implications are not known for other quantum security definitions. As a corollary, we get that quantum UC secure protocols for general multi-party computation can be constructed from commitments.
Permalink: http://www.ut.ee/~unruh/publications/quantum-uc.html
Abstract: We describe CoSP, a general framework for conducting computational soundness proofs of symbolic models and for embedding these proofs into formal calculi. CoSP considers arbitrary equational theories and computational implementations, and it abstracts away many details that are not crucial for proving computational soundness, such as message scheduling, corruption models, and even the internal structure of a protocol. CoSP enables soundness results, in the sense of preservation of trace properties, to be proven in a conceptually modular and generic way: proving x cryptographic primitives sound for y calculi only requires x+y proofs (instead of x*y proofs without this framework), and the process of embedding calculi is conceptually decoupled from computational soundness proofs of cryptographic primitives. We exemplify the usefulness of CoSP 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 CoSP and give a sound implementation of public-key encryption and digital signatures.
Permalink: http://www.ut.ee/~unruh/publications/backes09cosp.html
Abstract: We elaborate on the problem of polynomial runtime in simulatability definitions for multi-party computation. First, the need for a new definition is demonstrated by showing which problems occur with common definitions of polynomial runtime. Then, we give a definition which captures in an intuitive manner what it means for a protocol or an adversary to have polynomial runtime.
We show that this notion is suitable for simulatability definitions for multi-party computation. In particular, a composition theorem is shown for this notion.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz09polynomial2.html
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.
Permalink: http://www.ut.ee/~unruh/publications/longterm-uc.html
Abstract: We describe a technique that enables accountability in systems that use randomized protocols. Byzantine faults whose effects are observed by a correct node are eventually detected and irrefutably linked to a faulty node. At the same time, correct nodes are always able to defend themselves against false accusations. The key contribution is a novel technique for generating cryptographically strong, accountable randomness. The technique generates a pseudo-random sequence and a proof that the elements of this sequence have been correctly generated, while avoiding that future values of the sequence can be predicted. External auditors can check if a node deviates from its expected behavior without learning anything about the node's future random choices. In particular, an accountable node does not need to leak secrets that would make its future actions predictable. The technique is practical and efficient. We demonstrate that our technique is practical by applying it to a simple server that uses random sampling for billing purposes.
Permalink: http://www.ut.ee/~unruh/publications/backes09csar.html
Abstract: The collision-resistance of hash functions is an important foundation of many cryptographic protocols. Formally, collision-resistance can only be expected if the hash function in fact constitutes a parametrized family of functions, since for a single function, the adversary could simply know a single hard-coded collision. In practical applications, however, unkeyed hash functions are a common choice, creating a gap between the practical application and the formal proof, and, even more importantly, the concise mathematical definitions.
A pragmatic way out of this dilemma was recently formalized by Rogaway: instead of requiring that no adversary exists that breaks the protocol (existential security), one requires that given an adversary that breaks the protocol, we can efficiently construct a collision of the hash function using an explicitly given reduction (constructive security).
In this paper, we show the limits of this approach: We give a protocol that is existentially secure, but that provably cannot be proven secure using a constructive security proof.
Consequently, constructive security—albeit constituting a useful improvement over the state of the art—is not comprehensive enough to encompass all protocols that can be dealt with using existential security proofs.
Permalink: http://www.ut.ee/~unruh/publications/backes08limits.html
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. We extend this definition to include the cases of adaptive corruptions and arbitrary active attacks, called adKDM security incorporating several novel design choices and substantially differing from prior definitions for public-key security. We also show that the OAEP encryption scheme (using a partial-domain one-way function) satisfies the strong notion of adKDM security in the random oracle model.The OAEP construction thus constitutes a suitable candidate for implementating symbolic abstractions of encryption schemes in a computationally sound manner under active adversaries.
Permalink: http://www.ut.ee/~unruh/publications/backes08oaep.html
Abstract: Game-based cryptographic proofs are typically expressed using pseudocode, which lacks a formal semantics. This can lead to ambiguous specifications, hidden mistakes, and even wrong proofs. We propose a language for expressing proofs that is expressive enough to specify all constructs occurring in cryptographic games, including probabilistic behaviors, the usage of oracles, and polynomial-time programs. The language is a probabilistic higher-order lambda calculus with recursive types, references, and support for events, and is simple enough that researchers without a strong background in the theory of programming languages can understand it. The language has been implemented in the proof assistant Isabelle/HOL.
Permalink: http://www.ut.ee/~unruh/publications/backes08formal.html
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 with more sophisticated operations with unique security features, out of which zero-knowledge proofs arguably constitute the most amazing such extension.
In this paper, we first identify which properties a cryptographic zero-knowledge proof needs to fulfill beyond the standard ones 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.
Permalink: http://www.ut.ee/~unruh/publications/backes08computational.html
Abstract: We present a novel eavesdropping technique for spying at a distance on data that is displayed on an arbitrary computer screen, including the currently prevalent LCD monitors. Our technique exploits reflections of the screen's optical emanations in various objects that one commonly finds in close proximity to the screen and uses those reflections to recover the original screen content. Such objects include eyeglasses, tea pots, spoons, plastic bottles, and even the eye of the user. We have demonstrated that this attack can be successfully mounted to spy on even small fonts using inexpensive, off-the-shelf equipment (less than 1500 dollars) from a distance of up to 10 meters. Relying on more expensive equipment allowed us to conduct this attack from over 30 meters away, demonstrating that similar attacks are feasible from the other side of the street or from a close-by building. We additionally establish theoretical limitations of the attack; these limitations may help to estimate the risk that this attack can be successfully mounted in a given environment.
Permalink: http://www.ut.ee/~unruh/publications/backes08compromising.html
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.
Permalink: http://www.ut.ee/~unruh/publications/backes08zero.html
Abstract: Alleine in ihrem Büro wähnen Mitarbeiter eines Unternehmens in der Regel ihre Bildschirminhalte vor Ausspähung geschützt - zumal, wenn das Display dem Fenster abgekehrt ist. Doch Reflexionen in Einrichtungsgegenständen können der Spionage Vorschub leisten und vertrauliche Daten Unbefugten zugänglich machen.
This article is written in German. The paper Backes, Dürmuth, Unruh, Compromising Reflections or How to Read LCD Monitors Around the Corner, 2008 covers similar content and is available online.
Permalink: http://www.ut.ee/~unruh/publications/backes08gespiegelt.html
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).
Permalink: http://www.ut.ee/~unruh/publications/hofheinz08towards.html
Abstract: We elaborate on the problem of polynomial runtime in simulatability definitions for multi-party computation. First, the need for a new definition is demonstrated by showing which problems occur with common definitions of polynomial runtime. Then, we give a definition which captures in an intuitive manner what it means for a protocol or an adversary to have polynomial runtime.
We show that this notion is suitable for simulatability definitions for multi-party computation. In particular, a composition theorem is shown for this notion.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz05polynomial.html
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 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.
Permalink: http://www.ut.ee/~unruh/publications/unruh07random.html
Abstract: The well-known page description language PostScript is a full-fledged programming language. We show that this can lead to unexpected problems and possibilities for manipulation.
This article is written in German. The paper Backes, Dürmuth, Unruh, Information Flow in the Peer-Reviewing Process (extended abstract), 2007 covers similar content and is available online.
Permalink: http://www.ut.ee/~unruh/publications/backes08gespiegelt.html
Abstract: This is a short summary of the Ph.D. thesis Unruh, Protokollkomposition und Komplexität, 2007 published as part of the nomination process for the award offered by the German Society for Computer Science (Gesellschaft für Informatik) for the best German, Austrian and Swiss Ph.D. thesis.
Both this summary and the thesis are written in German. Wide parts of this thesis are covered by the English papers Hofheinz, Unruh, Comparing Two Notions of Simulatability, 2005, Hofheinz, Unruh, Simulatable Security and Polynomially Bounded Concurrent Composition, 2006 and Unruh, Relations among Statistical Security Notions - or - Why Exponential Adversaries are Unlimited, 2005.
Permalink: http://www.ut.ee/~unruh/publications/unruh07thesisdagstuhl.html
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.
Permalink: http://www.ut.ee/~unruh/publications/backes07security.html
Abstract: We investigate a new type of information flow in the electronic publishing process. We show that the use of PostScript in this process introduces serious confidentiality issues. In particular, we explain how the reviewer's anonymity in the peer-reviewing process can be compromised by maliciously prepared PostScript documents. A demonstration of this attack is available. We briefly discuss how this attack can be extended to other document formats as well.
Permalink: http://www.ut.ee/~unruh/publications/backes07information.html
Abstract: We show how to model the semantics of quantum programs that give classical output during their execution. That is, in our model even non-terminating programs may have output. The modelling interprets a program as a measurement process on the machines state, with the classical output as measurement result. The semantics presented here are fully abstract in the sense that two programs are equal if and only if they give the same outputs in any composition.
Permalink: http://www.ut.ee/~unruh/publications/unruh07quantum.html
Abstract: Algorithmic progress and future technology threaten today's cryptographic protocols. Long-term secure protocols should not even in future reveal more information to a--then possibly unlimited--adversary.
In this work we initiate the study of protocols which are 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 general zero knowledge arguments. Surprisingly, nontrivial zero knowledge protocols are possible based on a coin tossing functionality: We give a long-term secure composable zero knowledge protocol proving the knowledge of the factorisation of a Blum integer.
Furthermore we give practical alternatives (e.g., signature cards) to the usual setup-assumptions and show that these allow to implement the important primitives commitment and zero-knowledge argument.
Permalink: http://www.ut.ee/~unruh/publications/muellerquade07long.html
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.
Permalink: http://www.ut.ee/~unruh/publications/backes07necessity.html
Abstract: In the setting of Reactive Simulatability/UC there are two different notions of security differing in the order of quantifiers. In the case of universal security/UC, the environment is chosen depending on the simulator, while in the case of general security/specialised-simulator UC the simulator may depend on the environment. It was a longstanding open question whether these two notions are equivalent.
Furthermore, the notion of (polynomially-bounded) general composability has been introduced. It captures the minimal security notion that allow for a certain general kind of secure composition. Although it was known that universal security implies general composability, the relation to the other notions was open.
We analyse all open relations between these security notions in the case of computational, statistical and perfect security. We show that for computational security, the three notions are different, that is universal security strictly implies general composability which in turn strictly implies general security (given a natural complexity assumption). For statistical security universal security and general composability coincide and strictly imply general security (although when allowing only protocols running in polynomial time, all three notions). And for perfect security all three notions coincide. This gives an answer to the open problems mentioned above.
For showing these relations, we introduced several new techniques. First, the complexity assumption of so-called time-lock puzzles is investigated and shown to be a very effective tool for constructing separating examples between security notions. Further the usefulness of game-theoretic techniques for showing equivalences between different notions of statistical security is demonstrated.
The thesis is written in German. Wide parts of this thesis are covered by the English papers Hofheinz, Unruh, Comparing Two Notions of Simulatability, 2005, Hofheinz, Unruh, Simulatable Security and Polynomially Bounded Concurrent Composition, 2006 and Unruh, Relations among Statistical Security Notions - or - Why Exponential Adversaries are Unlimited, 2005.
Permalink: http://www.ut.ee/~unruh/publications/unruh07protokollkomposition.html
Abstract: We give an attack on a public key encryption scheme suggested by Shpilrain and Zapata. Experimental evidence shows that this attack is practical and works for the proposed parameters. We give a way to repair the encryption scheme so that our attack does not work anymore. However, we also expose weak points of the scheme that do not seem to be repairable in an obvious manner.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz06attack.html
Abstract: We investigate the state of the art in the development of quantum programming languages. Two kinds of such languages are distinguished, those targeting at practical applications like simulation or the programming of actual quantum computers, and those targeting the theoretical analysis of quantum programs. We give an overview over existing work on both types and present open challenges yet to be resolved.
Permalink: http://www.ut.ee/~unruh/publications/unruh06quantum.html
Abstract: We introduce a new notion of polynomial-time UC and Reactive Simulatability that allows the protocols to run in polynomial time in the length of their inputs. In comparison to prior work, our approach allows for a much larger class of protocols, and the definitions are nevertheless very simple.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz06simple.html
Abstract: We present a security definition for reactive protocols that simultaneously captures the notion of deniability/incoercibility and allows for secure composition of protocols.
Permalink: http://www.ut.ee/~unruh/publications/muellerquade06composable.html
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<n bits is already given "for free" to the parties.
Both protocol task and initial assumption can be formulated conveniently as ideal functionalities in the setting of simulatable security (depending on the used framework commonly referred to as Universal Composability or Reactive Simulatability). In this setting, we show the impossibility of extending coin toss for perfect and statistical security (for statistical security, we restrict to polynomial-round protocols). On the other hand, for computational security and suitable n,m, we show how to modify and use a known protocol construction for our purposes.
We also consider not universally composable security definitions (i.e., security definitions without an environment). We show exactly when such a coin-toss extension is possible and when not. In particular, we give an unconditionally secure protocol for extending coin-toss.
Combining our results with already known results, we obtain a (nearly) complete characterization under which circumstances coin toss extension is possible.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz06possibility.html
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.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz06simulatable.html
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.
Permalink: http://www.ut.ee/~unruh/publications/unruh05relations.html
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 captures 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.
Permalink: http://www.ut.ee/~unruh/publications/backes05fairness.html
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.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz05notion.html
Abstract: The framework of universal composability (UC) allows the modular design of cryptographic protocols. However universal composability is a very strict notion of security and the cryptographic tasks of zero-knowledge arguments as well as bit commitment schemes cannot be built from scratch in such a framework. To implement these tasks, additional "helping" functionalities are needed as set-up assumptions. Examples for sufficient set-up assumptions are the common reference string, the random oracle, or a public key infrastructure.
However, in all constructions so far, all these helping functionalities have to be used exclusively as a "helping" functionality, and cannot directly serve any other purpose without endangering the universal composability. E.g., a public key infrastructure used as set-up assumptions in a bit commitment scheme usually may not be used for e.g., encrypting other communication.
In this work, we introduce the concept of catalysts. Informally, a catalyst for some protocol task is a functionality that allows for universally composable implementation of that task, and may nevertheless still be used by arbitrary other applications.
We show that catalysts exist for zero-knowledge and bit commitment and thus, using a result of Canetti et al., for all well formed functionalities. And, what is more, we show that a signature card, which is in accordance with the requirements posed by the German law can be used as such a catalyst. This is of practical importance, as an infrastructure of signature cards is about to be set up in several nations of the EU. Our work proves that this infrastructure can be used to securely implement additional applications without negative side effects (with a non-catalytic approach, one would have to disallow any other use of the signature-cards if using them for composable bit commitment).
Permalink: http://www.ut.ee/~unruh/publications/hofheinz07universally.html
Abstract: We prove that for deniable protocol tasks oblivious transfer is not complete. We introduce the protocol task of bit commitments which can be undone, and prove that this task cannot be realised with OT whereas there exists a secure realisation using string-OT.
Permalink: http://www.ut.ee/~unruh/publications/muellerquade05oblivious.html
Abstract: In this work, relations between the security notions standard simulatability and universal simulatability for cryptographic protocols are investigated.
A simulatability-based notion of security considers a protocol π as secure as an idealization τ of the protocol task, if and only if every attack on π can be simulated by an attack on τ.
Two formalizations, which both provide secure composition of protocols, are common: standard simulatability means that for every π-attack and protocol user H, there is a τ-attack, such that H cannot distinguish π from τ. Universal simulatability means that for every π-attack, there is a τ-attack, such that no protocol user H can distinguish π from τ.
Trivially, universal simulatability implies standard simulatability. We show: the converse is true with respect to perfect security, but not with respect to computational or statistical security.
Besides, we give a formal definition of a time-lock puzzle, which may be of independent interest. Although the described results do not depend on any computational assumption, we show that the existence of a time-lock puzzle gives an even stronger separation of standard and universal simulatability with respect to computational security.
Permalink: http://www.ut.ee/~unruh/publications/hofheinz05comparing.html
Abstract: The notion of simulatable security (reactive simulatability, universal composability) is a powerful tool for allowing the modular design of cryptographic protocols (composition of protocols) and showing the security of a given protocol embedded in a larger one. Recently, these methods have received much attention in the quantum cryptographic community.
We give a short introduction to simulatable security in general and proceed by sketching the many different definitional choices together with their advantages and disadvantages.
Based on the reactive simulatability modelling of Backes, Pfitzmann and Waidner we then develop a quantum security model. By following the BPW modelling as closely as possible, we show that composable quantum security definitions for quantum protocols can strongly profit from their classical counterparts, since most of the definitional choices in the modelling are independent of the underlying machine model.
In particular, we give a proof for the simple composition theorem in our framework.
Permalink: http://www.ut.ee/~unruh/publications/unruh04simulatable.html
Abstract: We present an imperative quantum programming language with physically motivated operational semantics. The language is not restricted to reversible computations, but can be used to describe unitary quantum operations in interaction with measurement and classical control. We are able to model (irreversible) deterministic and probabilistic programs as special cases of quantum programs, in contrast to computational models which assume all quantum operations to be unitary. Due to the presence of loops and conditionals, we have to consider terminating and non-terminating programs. Even with non-terminating programs, it may be of interest to make statements about classical events during the run of the programs like measurement results, contents of classical variables, outputs. For this, we define the notion of classical output, which may already happen before program termination. One application, which would need such classical output, are cryptographic protocols, where we want to define events which must not occur, even in the case of non-terminating protocols.
Programs in our language can contain arbitrary operators and mathematical functions, thus allowing to state very abstract but well-defined specifications and to gradually transform it into programs containing only primitive operations. We also present a simple calculus to transform and reason about programs.
Programs written in pseudo-code can usually easily be transformed into our language, since instructions like "while the measurement on register A does not yield a result satisfying condition P, apply transformation U" have direct counterparts in the formalised language. However, no physically impossible operations (like e.g. cloning) may be expressed.
Permalink: http://www.ut.ee/~unruh/publications/unruh04classical.html
Abstract: When constructing random number generators based on physical processes, it is usually not possible to get uniformly and independently distributed output bits. We therefore present a method for postprocessing the output of the random source and generating good randomness, we call that method the adaptive extraction. Its two main features are: First, we do not need to know the source's behaviour in every detail (i.e. it suffices to put some constraints on the distribution of the output). Secondly, the amount of generated good randomness (i.e. nearly uniformly distributed data) is automatically adapted to the quality of the input.
We then present a technique for modelling sources, similar to hidden Markov models, which is especially suited for use with the adaptive extraction.
Finally we investigate some practical aspects of our theory: We present a statistical test to verify assumptions made on the source, and we examine a given physical source with respect to the feasibility of adaptive extraction.
Permalink: http://www.ut.ee/~unruh/publications/unruh03zufallsextraktoren.html
Abstract: The objective of this work is to introduce the notion of formal security into quantum computation. In order to achieve this, we introduce a new security model, containing a quantum communication model. We will lay some stress on formal details to show which are the problems arising in a formal definition of quantum security.
Based on this model we will analyse some basic aspects of quantum protocols:
- Are quantum protocols composable?
- Do classically secure classical protocols stay secure in a quantum environment?
Both questions we will answer by and large positively. This discussion (and especially the proofs) will be less formal, because of the complex nature of the underlying communication processes.
Permalink: http://www.ut.ee/~unruh/publications/unruh02formal.html