International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Michael Backes

Publications

Year
Venue
Title
2019
PKC
Efficient Non-Interactive Zero-Knowledge Proofs in Cross-Domains Without Trusted Setup
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 📺
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
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.
2016
PKC
2015
EPRINT
2014
EPRINT
2014
EPRINT
2014
EPRINT
2011
ASIACRYPT
2010
EPRINT
Computationally Sound Verification of Source Code
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
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
ASIACRYPT
2008
ASIACRYPT
2008
EPRINT
Computational Soundness of Symbolic Zero-Knowledge Proofs Against Active Attackers
Michael Backes Dominique Unruh
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
Michael Backes Boris Köpf
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
TCC
2007
EPRINT
On the Security of Protocols with Logarithmic Communication Complexity
Michael Backes Dominique Unruh
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
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
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
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
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
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
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
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
Michael Backes Peeter Laud
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
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
TCC
2005
EPRINT
Limits of the Cryptographic Realization of Dolev-Yao-style XOR
Michael Backes Birgit Pfitzmann
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
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
Michael Backes Christian Cachin Alina Oprea
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
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
TCC
2004
EPRINT
Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library
Michael Backes Birgit Pfitzmann
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
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
Michael Backes Birgit Pfitzmann
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
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
Michael Backes
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
Michael Backes Birgit Pfitzmann
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
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
Michael Backes Christian Cachin
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
Michael Backes Dennis Hofheinz
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