1,721,104 research outputs found
A Composable Cryptographic Library with Nested Operations (Extended Abstract)
No full textMichael Backes [email protected] Birgit Pfitzmann [email protected] Michael Waidner [email protected] ABSTRACT We present the first idealized cryptographic library that can be used like the Dolev-Yao model for automated proofs of cryptographic protocols that use nested cryptographic operations, while coming with a cryptographic implementation that is provably secure under active attacks
How to Break and Repair a "Provably Secure" Untraceable Payment System (Extended Abstract)
No full text) Birgit Pfitzmann 1 , Michael Waidner 2 Abstract On Crypto '88, an untraceable payment system with provable security against abuse by individuals was presented by Damgård. We show how to break the untraceability of that system completely. Next, an improved version of the system is presented. We also augment the system by security for the individuals against loss of money, and we introduce the possibility of receipts for payments. Finally, whereas all this concerned an on-line system, we present a similar construction for untraceable electronic cash. 1 Introduction We start with a brief overview over untraceable payment systems. Then we give an overview over the rest of the paper. 1.1 Untraceable payment systems in general The main characteristic of untraceable payment systems is that, like with conventional cash, the system operator (normally called "bank") cannot completely observe the payment behaviour of the individuals. Also, payer and payee may want to be untraceable by ea..
On the Existence of Statistically Hiding Bit Commitment Schemes and Fail-Stop Signatures
No full text. 1 Introduction almost unique secret key property On the Existence of Statistically Hiding Bit Commitment Schemes and Fail-Stop Signatures Ivan B. Damgard , Torben P. Pedersen and Birgit Pfitzmann In this section, we introduce the two main actors on the scene, fail-stop signatures (FSS) and statistically hiding bit commitments. Fail-stop signatures were introduced in [16]. Further constructions appear in [13, 14, 5, 6]. A formal definition of the concept and a survey of the recent most efficient schemes will appear in [12]. Before going into the properties of FSS schemes, let us discuss some aspects of ordinary digital signatures: In an application of such signatures, what should happen if someone shows up with a message and a valid looking signature from user , but claims that she never signed the message? Suppose the signature scheme is based on a computational problem, , which everybody accepts cannot be solved in polynomial time. Based on this one could claim that it is not reas..
Cryptographically sound analysis of security protocols
Full text linkIn this thesis, we show how formal methods can be used for the cryptographically sound verification of concrete implementations of security protocols in order to obtain trustworthy and meaningful proofs, and to eliminate human inaccuracies. First, we show how to derive secure concrete implementations of a given abstract specification. The security proofs are essentially based on the well-established approach of bisimulation which can be formally verified yielding rigorous proofs. As an example, we present both a specification and a secure implementation of secure message transmission with ordered channels. Moreover, the example comprises a general methodology how secure implementation of arbitrary specifications can be obtained. Thereafter, we concentrate on the actual goals the protocol should fulfill. Thus, we define integrity properties in our underlying model and we show that logic derivations among them carry over specification to the concrete implementation, which makes them accessible for tool-assisted verification. As an example, we formally verify one concrete protocol using the theorem prover PVS yielding the first machine-aided and sound proof of a cryptographic protocol. As additional properties of security protocols, we consider liveness and noninterference. The standard definition of these properties is not suited to cope with protocols involving real cryptographic primitives, so we introduce new definitions which are restricted to polynomial runs and include error probabilities. We show that both properties carry over from the specification to the concrete implementation, and we present two examples, one for each property, which we prove to fulfill our definitions.Diese Arbeit behandelt formale Verifikation von Sicherheitsprotokollen mit dem Ziel,maschinell verifizierte Beweise zu ermöglichen, die die kryptographische Semantik respektieren, d.h., deren Aussagen bzgl. der zugrundeliegenden Kryptographie und den kryptographischen Sicherheitsdefinitionen gültig sind (engl. cryptographically sound proofs).Als erstes zeigen wir, wie formale Methoden benutzt werden können, um sichere konkrete Implementationen anhand einer gegebenen abstrakten Spezifikation herzuleiten. Wir geben dafür eine allgemeingültige Methodologie an, die auf formal verifizierten Bisimulationen basiert, was uns rigorose und glaubhafte Sicherheitsbeweise liefert. Als
Beispiel geben wir eine Spezifikation und eine konkrete Implementation für sichere geordnete Nachrichtenübertragung an. Die im Sicherheitsbeispiel der Implementation auftretende Bisimulation verifizieren wir mit Hilfe des Theorembeweisers PVS. Als zweites konzentrieren wir uns auf die Ziele, die ein Sicherheitsprotokoll erfüllen soll. Wir definieren Integritätseigenschaften in unserem zugrundeliegenden Modell, und wir beweisen, dass sich logische Schlussfolgerungen bzgl. dieser Eigenschaften von der Spezifikation auf die Implementation übertragen, was eine essentielle Voraussetzung für maschinelle Verifikation darstellt. Als Beispiel verifizieren wir ein konkretes Protokoll mit Hilfe des Theorembeweisers PVS, was uns den ersten Beweis eines Sicherheitsprotokolls liefert, der sowohl maschinell verifiziert ist als auch
der kryptographischen Semantik "treu'; bleibt, d.h., der wirklich ein Beweis gegen die kryptographischen Primitive und deren kryptographische Sicherheitsdefinitionen ist. Als zusätzliche Eigenschaften von Sicherheitsprotokollen betrachten wir Lebendigkeit (engl. liveness) und Unbeeinflussbarkeit (engl. non-interference). Da sich die Standarddefinition dieser wichtigen Eigenschaften als ungeeignet für echte Kryptographie
herausstellt, führen wir allgemeinere Definitionen ein, die auf polynomielle Länge beschränkt sind und Fehlerwahrscheinlichkeiten berücksichtigen.Wir zeigen, dass sich diese Eigenschaften von der Spezifikation auf die Implementation übertragen,was wiederum den Bezug zu formalen Methoden herstellt. Wir präsentieren zwei Beispiele, je eines für jede Eigenschaft, von denen wir beweisen, dass sie die entsprechende Definition erfüllen
Optimistic fair exchange
Full text linkA fair exchange guarantees that a participant only reveals its items (such as signatures, payments, or data) if it receives the expected items in exchange. Efficient fair exchange requires a so-called third party, which is assumed to be correct. Optimistic fair exchange involves this third party only if needed, i.e., if the participants cheat or disagree.
In Part I, we prove lower bounds on the message and time complexity of two particular instances of fair exchange in varying models, namely contract signing (fair exchange of two signatures under a contract) and certified mail (fair exchange of data for a receipt). We show that all given bounds are tight by describing provably time- and message-optimal protocols for all considered models and instances.
In Part II, we have a closer look at formalizing the security of fair exchange. We introduce a new formal notion of security (including secrecy) for reactive distributed systems. We illustrate this new formalism by a specification of certified mail as an alternative to the traditional specification given in Part I.
In Part III, we describe protocols for generic and optimistic fair exchange of arbitrary items. These protocols are embedded into the SEMPER Fair Exchange Layer, which is a central part of the SEMPER Framework for Secure Electronic Commerce.Ein Austausch ist fair, wenn eine Partei die angebotenen Güter, wie zum Beispiel digitale Signaturen, Zahlungen oder Daten, nur abgibt, wenn sie die erwarteten Güter im Tausch erhält. Ohne eine als korrekt angenommene dritte Partei, welche eine mit einem Notar vergleichbare Rolle übernimmt, ist fairer Austausch nicht effizient möglich. Ein fairer Austausch heißt optimistisch, falls diese dritte Partei nur in Problemfällen am Protokoll teilnimmt. In Teil I werden beweisbar zeit- und nachrichtenoptimale Protokolle für die Spezialfälle ';elektronische Vertragsunterzeichnung" (fairer Austausch zweier Signaturen; engl. contract signing) und ';elektronisches Einschreiben" (fairer Austausch von Daten gegen eine Quittung; engl. certified mail) von fairem Austausch vorgestellt. Teil II beschreibt einen neuen Integritäts- und Geheimhaltungsbegriff für reaktive Systeme. Dieser basiert auf einer Vergleichsrelation ';so sicher wie", welche die Sicherheit zweier Systeme vergleicht. Ein verteiltes, reaktives System wird dann als sicher bezeichnet, wenn es so sicher wie ein idealisiertes System (engl. trusted host) für diesen Dienst ist. Mit diesem Formalismus geben wir eine alternative Sicherheitsdefinition von ';elektronischem Einschreiben" an, deren Semantik im Gegensatz zu der in Teil I beschriebenen Definition nun unabhängig vom erbrachten Dienst ist. Teil III beschreibt ein Design und optimistische Protokolle für generischen fairen Austausch von zwei beliebigen Gütern und den darauf aufbauenden SEMPER Fair Exchange Layer. Dieser ist ein wesentlicher Baustein des SEMPER Framework for Secure Electronic Commerce
Secure group key agreement
Full text linkAs a result of the increased popularity of group-oriented applications and protocols, group communication occurs in many different settings: from network multicasting to application layer tele- and video-conferencing. Regardless of the application environment, security services are necessary to provide communication privacy and integrity. This thesis considers the problem of key management in a special class of groups, namely dynamic peer groups. Key management, especially in a group setting, is the corner stone for all other security services. Dynamic peer groups require not only initial key agreement but also auxiliary key agreement operations such as member addition, member exclusion and group fusion. We discuss all group key agreement operations and present a concrete protocol suite, CLIQUES, which offers all of these operations. By providing the first formal model for group key establishment and investigating carefully the underlying cryptographic assumptions as well as their relations, we formally prove the security of a subset of the protocols based on the security of the Decisional Diffie-Hellman assumption; achieving as a side-effect the first provably secure group key agreement protocolMit der Verbreitung offener Netze, insbesondere des Internets, fand auch
die Gruppenkommunikation eine rasante Verbreitung. Eine Vielzahl heutiger
Protokolle sind gruppen-orientiert: angefangen bei Multicast-Diensten
in der Netzwerkschicht bis hin zu Videokonferenzsystemen auf der Anwendungsschicht. Alle diese Dienste haben Sicherheitsanforderungen wie Vertraulichkeit und Integrität zu erfüllen, die den Einsatz kryptographischer
Techniken und die Verfügbarkeit gemeinsamer kryptographischen Schlüssel
oft unumgänglich machen.
In der folgenden Doktorarbeit betrachte ich dieses grundlegendste Problem
der Gruppenkommunikation, nämlich das Schlüsselmanagement, für dynamische Gruppen, die sogenannten "Dynamic Peer-Groups';. Die Dynamik dieser Gruppen erfordert nicht nur initialen Schlüsselaustausch innerhalb einer Gruppe sondern auch sichere und effiziente Verfahren für die Aufnahme neuer und den Ausschluß alter Gruppenmitglieder. Ich diskutiere alle dafür notwendigen Dienste und präsentiere CLIQUES, eine Familie von Protokollen, die diese Dienste implementiert. Ich gebe erstmalig eine formale Definition fü sicheres Gruppen-Schlüsselmanagement und beweise die Sicherheit der genannten Protokolle basierend auf einer kryptographischen Standardannahme, der "Decisional Diffie-Hellman'; Annahme. Diese Sicherheitsbetrachtung wird durch eine detaillierte Untersuchung dieser Annahme und ihrer Relation zu verwandten Annahmen abgeschlossen
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Appropriate Similarity Measures for Author Cocitation Analysis
Full text linkWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
- …
