## CryptoDB

### Michael Backes

#### Publications

**Year**

**Venue**

**Title**

2019

PKC

Efficient Non-Interactive Zero-Knowledge Proofs in Cross-Domains Without Trusted Setup
Abstract

With the recent emergence of efficient zero-knowledge (ZK) proofs for general circuits, while efficient zero-knowledge proofs of algebraic statements have existed for decades, a natural challenge arose to combine algebraic and non-algebraic statements. Chase et al. (CRYPTO 2016) proposed an interactive ZK proof system for this cross-domain problem. As a use case they show that their system can be used to prove knowledge of a RSA/DSA signature on a message m with respect to a publicly known Pedersen commitment $$g^m h^r$$. One drawback of their system is that it requires interaction between the prover and the verifier. This is due to the interactive nature of garbled circuits, which are used in their construction. Subsequently, Agrawal et al. (CRYPTO 2018) proposed an efficient non-interactive ZK (NIZK) proof system for cross-domains based on SNARKs, which however require a trusted setup assumption.In this paper, we propose a NIZK proof system for cross-domains that requires no trusted setup and is efficient both for the prover and the verifier. Our system constitutes a combination of Schnorr based ZK proofs and ZK proofs for general circuits by Giacomelli et al. (USENIX 2016). The proof size and the running time of our system are comparable to the approach by Chase et al. Compared to Bulletproofs (SP 2018), a recent NIZK proofs system on committed inputs, our techniques achieve asymptotically better performance on prover and verifier, thus presenting a different trade-off between the proof size and the running time.

2019

EUROCRYPT

Ring Signatures: Logarithmic-Size, No Setup—from Standard Assumptions
📺
Abstract

Ring signatures allow for creating signatures on behalf of an ad hoc group of signers, hiding the true identity of the signer among the group. A natural goal is to construct a ring signature scheme for which the signature size is short in the number of ring members. Moreover, such a construction should not rely on a trusted setup and be proven secure under falsifiable standard assumptions. Despite many years of research this question is still open.In this paper, we present the first construction of size-optimal ring signatures which do not rely on a trusted setup or the random oracle heuristic. Specifically, our scheme can be instantiated from standard assumptions and the size of signatures grows only logarithmically in the number of ring members.We also extend our techniques to the setting of linkable ring signatures, where signatures created using the same signing key can be linked.

2018

ASIACRYPT

Signatures with Flexible Public Key: Introducing Equivalence Classes for Public Keys
Abstract

We introduce a new cryptographic primitive called signatures with flexible public key $$(\mathsf{SFPK})$$. We divide the key space into equivalence classes induced by a relation $$\mathcal {R}$$. A signer can efficiently change his or her key pair to a different representatives of the same class, but without a trapdoor it is hard to distinguish if two public keys are related. Our primitive is motivated by structure-preserving signatures on equivalence classes ($$\mathsf{SPS\text {-}EQ}$$), where the partitioning is done on the message space. Therefore, both definitions are complementary and their combination has various applications.We first show how to efficiently construct static group signatures and self-blindable certificates by combining the two primitives. When properly instantiated, the result is a group signature scheme that has a shorter signature size than the current state-of-the-art scheme by Libert, Peters, and Yung from Crypto’15, but is secure in the same setting.In its own right, our primitive has stand-alone applications in the cryptocurrency domain, where it can be seen as a straightforward formalization of so-called stealth addresses. Finally, it can be used to build the first efficient ring signature scheme in the plain model without trusted setup, where signature size depends only sub-linearly on the number of ring members. Thus, we solve an open problem stated by Malavolta and Schröder at ASIACRYPT’2017.

2015

EPRINT

2010

EPRINT

Computationally Sound Verification of Source Code
Abstract

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

2009

EPRINT

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

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

2008

EPRINT

Computational Soundness of Symbolic Zero-Knowledge Proofs Against Active Attackers
Abstract

The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev-Yao models offering the core cryptographic operations such as encryption and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. Recent work, however, has started to extend Dolev-Yao models to more sophisticated operations with unique security features. Zero-knowledge proofs arguably constitute the most amazing such extension.
In this paper, we first identify which additional properties a cryptographic zero-knowledge proof needs to fulfill in order to serve as a computationally sound implementation of symbolic (Dolev-Yao style) zero-knowledge proofs; this leads to the novel definition of a symbolically-sound zero-knowledge proof system. We prove that even in the presence of arbitrary active adversaries, such proof systems constitute computationally sound implementations of symbolic zero-knowledge proofs. This yields the first computational soundness result for symbolic zero-knowledge proofs and the first such result against fully active adversaries of Dolev-Yao models that go beyond the core cryptographic operations.

2008

EPRINT

Formally Bounding the Side-Channel Leakage in Unknown-Message Attacks
Abstract

We propose a novel approach for quantifying a system's resistance to unknown-message side-channel attacks. The approach is based on a measure of the secret information that an attacker can extract from
a system from a given number of side-channel measurements. We
provide an algorithm to compute this measure, and we use it to
analyze the resistance of hardware implementations of cryptographic
algorithms with respect to power and timing attacks. In particular,
we show that message-blinding -- the common countermeasure against
timing attacks -- reduces the rate at which information about the
secret is leaked, but that the complete information is still
eventually revealed. Finally, we compare information measures
corresponding to unknown-message, known-message, and chosen-message
attackers and show that they form a strict hierarchy.

2007

EPRINT

On the Security of Protocols with Logarithmic Communication Complexity
Abstract

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

2007

EPRINT

On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography
Abstract

The abstraction of cryptographic operations by term algebras, called
Dolev-Yao models or symbolic cryptography, is essential in almost
all tool-supported methods for proving security protocols. Recently
significant progress was made -- using two conceptually different
approaches -- in proving that Dolev-Yao models can be sound with
respect to actual cryptographic realizations and security
definitions. One such approach is grounded on the notion of
simulatability, which constitutes a salient technique of Modern
Cryptography with a longstanding history for a variety of different
tasks. The other approach strives for the so-called mapping
soundness -- a more recent technique that is tailored to the
soundness of specific security properties in Dolev-Yao models, and
that can be established using more compact proofs. Typically, both
notions of soundness for similar Dolev-Yao models are established
separately in independent papers.
In this paper, the two approaches are related for the first time.
Our main result is that simulatability soundness entails mapping
soundness provided that both approaches use the same cryptographic
implementation. Interestingly, this result does not dependent on
details of the simulator, which translates between cryptographic
implementations and their Dolev-Yao abstractions in simulatability
soundness. Hence, future research may well concentrate on
simulatability soundness whenever applicable, and resort to mapping
soundness in those cases where simulatability soundness is too
strong a notion.

2007

EPRINT

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

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

2006

EPRINT

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos
Abstract

We present a computational analysis of basic Kerberos with and without its public-key extension PKINIT in which we consider authentication and key secrecy properties. Our proofs rely on the Dolev--Yao-style model of Backes, Pfitzmann, and Waidner, which allows for mapping results obtained symbolically within this model to cryptographically sound proofs if certain assumptions are met. This work was the first verification at the computational level of such a complex fragment of an industrial protocol. By considering a recently fixed version of PKINIT, we extend symbolic correctness results we previously attained in the Dolev--Yao model to cryptographically sound results in the computational model.

2006

EPRINT

Cryptographically Sound Theorem Proving
Abstract

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

2006

EPRINT

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

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

2006

EPRINT

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

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

2006

EPRINT

Conditional Reactive Simulatability
Abstract

Simulatability has established itself as a salient notion for defining
and proving the security of cryptographic protocols since it entails
strong security and compositionality guarantees, which are achieved by
universally quantifying over all environmental behaviors of the
analyzed protocol. As a consequence, however, protocols that are
secure except for certain environmental behaviors are not simulatable,
even if these behaviors are efficiently identifiable and thus can be
prevented by the surrounding protocol.
We propose a relaxation of simulatability by conditioning the
permitted environmental behaviors, i.e., simulation is only required
for environmental behaviors that fulfill explicitly stated
constraints. This yields a more fine-grained security definition that
is achievable i) for several protocols for which unconditional
simulatability is too strict a notion or ii) at lower cost for the
underlying cryptographic primitives. Although imposing restrictions
on the environment destroys unconditional composability in general, we
show that the composition of a large class of conditionally
simulatable protocols yields protocols that are again simulatable
under suitable conditions. This even holds for the case of cyclic
assume-guarantee conditions where protocols only guarantee suitable
behavior if they themselves are offered certain guarantees.
Furthermore, composing several commonly investigated protocol classes
with conditionally simulatable subprotocols yields protocols that are
again simulatable in the standard, unconditional sense.

2006

EPRINT

Computationally Sound Secrecy Proofs by Mechanized Flow Analysis
Abstract

We present a novel approach for proving secrecy properties of security
protocols by mechanized flow analysis. In contrast to existing tools
for proving secrecy by abstract interpretation, our tool enjoys
cryptographic soundness in the strong sense of blackbox reactive
simulatability/UC which entails that secrecy properties proven by our
tool are automatically guaranteed to hold for secure cryptographic
implementations of the analyzed protocol, with respect to the more
fine-grained cryptographic secrecy definitions and adversary models.
Our tool is capable of reasoning about a comprehensive language for
expressing protocols, in particular handling symmetric encryption and
asymmetric encryption, and it produces proofs for an unbounded number
of sessions in the presence of an active adversary. We have
implemented the tool and applied it to a number of common protocols
from the literature.

2006

EPRINT

On the Necessity of Rewinding in Secure Multiparty Computation
Abstract

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

2005

EPRINT

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

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

2005

EPRINT

On Fairness in Simulatability-based Cryptographic Systems
Abstract

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

2005

EPRINT

Secure Key-Updating for Lazy Revocation
Abstract

We consider the problem of efficient key management and user
revocation in cryptographic file systems that allow shared access to
files. A performance-efficient solution to user revocation in such
systems is lazy revocation, a method that delays the re-encryption
of a file until the next write to that file. We formalize the notion
of key-updating schemes for lazy revocation, an abstraction to
manage cryptographic keys in file systems with lazy revocation, and
give a security definition for such schemes. We give two composition
methods that combine two secure key-updating schemes into a new
secure scheme that permits a larger number of user revocations. We
prove the security of two slightly modified existing constructions
and propose a novel binary tree construction that is also provable
secure in our model. Finally, we give a systematic analysis of the
computational and communication complexity of the three
constructions and show that the novel construction improves the
previously known constructions.

2005

EPRINT

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

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

2004

EPRINT

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

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

2004

EPRINT

The Reactive Simulatability (RSIM) Framework for Asynchronous Systems
Abstract

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

2004

EPRINT

Relating Symbolic and Cryptographic Secrecy
Abstract

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

2003

EPRINT

A Universally Composable Cryptographic Library
Abstract

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

2003

EPRINT

Unifying Simulatability Definitions in Cryptographic Systems under Different Timing Assumptions
Abstract

The cryptographic concept of simulatability has become a salient
technique for faithfully analyzing and proving security properties of
arbitrary cryptographic protocols. We investigate the relationship
between simulatability in synchronous and asynchronous frameworks by
means of the formal models of Pfitzmann et. al., which are seminal in
using this concept in order to bridge the gap between the
formal-methods and the cryptographic community. We show that the
synchronous model can be seen as a special case of the asynchronous
one with respect to simulatability, i.e., we present an embedding
between both models that we show to preserve simulatability. We show
that this result allows for carrying over lemmas and theorems that
rely on simulatability from the asynchronous model to its synchronous
counterpart without any additional work. Hence future work can
concentrate on the more general asynchronous case, without having to
neglect the analysis of synchronous protocols.

2003

EPRINT

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

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

2003

EPRINT

Symmetric Authentication Within a Simulatable Cryptographic Library
Abstract

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

2003

EPRINT

Public-Key Steganography with Active Attacks
Abstract

A complexity-theoretic model for public-key steganography with
active attacks is introduced. The notion of steganographic
security against adaptive chosen-covertext attacks (SS-CCA) and a
relaxation called steganographic security against
publicly-detectable replayable adaptive chosen-covertext attacks
(SS-PDR-CCA) are formalized. These notions are closely related
to CCA-security and PDR-CCA-security for public-key
cryptosystems. In particular, it is shown that any SS-(PDR-)CCA
stegosystem is a (PDR-)CCA-secure public-key cryptosystem and that
an SS-PDR-CCA stegosystem can be realized from any PDR-CCA-secure
public-key cryptosystem with pseudorandom ciphertexts.

2003

EPRINT

How to Break and Repair a Universally Composable Signature Functionality
Abstract

Canetti and Rabin recently proposed a universally composable ideal functionality F_SIG for digital signatures. We show that this functionality cannot be securely realized by \emph{any} signature scheme, thereby disproving their result that any signature scheme that is existentially unforgeable under adaptive chosen-message attack is a secure realization.
Next, an improved signature functionality is presented. We show that our improved functionality can be securely realized by precisely those signature schemes that are secure against existential forgery under adaptive chosen-message attacks.

#### Program Committees

- Crypto 2011
- TCC 2010
- Eurocrypt 2005
- Asiacrypt 2004

#### Coauthors

- Muhammad Rizwan Asghar (1)
- David Basin (1)
- Fabian Bendun (1)
- Christian Cachin (3)
- Iliano Cervesato (1)
- Nico Döttling (1)
- Peter Druschel (1)
- Markus Duermuth (2)
- Markus Dürmuth (1)
- Dario Fiore (1)
- Lucjan Hanzlik (3)
- Amir Herzberg (1)
- Dennis Hofheinz (4)
- Aaron D. Jaggard (1)
- Aniket Kate (4)
- Kamil Kluczniak (2)
- Boris Köpf (1)
- Ralf Küsters (2)
- Peeter Laud (1)
- Matteo Maffei (2)
- Praveen Manoharan (1)
- Ninja Marnau (1)
- Sebastian Meiser (3)
- Sebastian Mödersheim (1)
- Esfandiar Mohammadi (2)
- Jörn Müller-Quade (3)
- Alina Oprea (1)
- Arpita Patra (1)
- Birgit Pfitzmann (12)
- Ivan Pryvalov (1)
- Raphael M. Reischuk (1)
- Andre Scedrov (2)
- Jonas Schneider (2)
- Dominique Schröder (1)
- Milivoj Simeonovski (1)
- Christoph Sprenger (1)
- Joe-Kay Tsay (1)
- Dominique Unruh (10)
- Luca Viganò (1)
- Michael Waidner (6)