Die Bedeutung von digitalen Signaturen und ihre Anwendung in den verschiedensten Bereichen der Gesellschaft, Industrie und Politik nimmt stetig zu. In vielen Fällen wird in Zukunft die digitale Unterschrift einer manuellen gleichgestellt sein. Infolgedessen steigt der Bedarf nach leistungsfähigen Werkzeugen und Methoden für die Qualifizierung und Analyse von Prozessen zur Verarbeitung digitaler Signaturen. Diese Arbeit befasst sich mit allgemeingültigen Kriterien zur vollständigen Verifikation einer digital geleisteten Unterschrift. Abgesehen von juristischen Aspekten und frei vereinbarten Regeln, gibt es eindeutige Indizien um festzustellen, ob eine digitale Signatur gültig ist. Die technische Gültigkeitsprüfung mit einer eigens dafür entwickelten Logik ist Gegenstand dieser Betrachtungen. Dabei soll mit Hilfe einer formalen Sprache eine vollständige und widerspruchsfreie Aussage zur Gültigkeit einer digitalen Signatur ermöglicht werden. Als Basis für die logische Ableitung dienen die Eigenschaften und Besonderheiten einer Public-Key-Infrastruktur (PKI), die mit den Symbolen der hier vorgestellten Logik formulierbar sind. Für die Realisierung von Komponenten zur Bearbeitung von digitalen Signaturen ist eine exakte Definition der einzelnen Prüfkriterien notwendig. Insbesondere unterschiedliche Realisierungen müssen auf Basis einer gemeinsamen Entscheidungsgrundlage bei einer Signaturprüfung zum selben Ergebnis kommen. In vielen Fällen ist dafür eine allgemeinsprachlich abgefasste Spezifikation der gesamten PKI zuständig. Allerdings kann, wie in Kapitel 6 gezeigt wird, eine derartige Beschreibungsform mit Lücken behaftet sein und Inkonsistenzen aufweisen. Mit Hilfe einer logischen Sprache wird es einfacher, eine konsequente Umsetzung aller an die Verifikation gestellten Vorgaben zu erreichen. Zusätzlich erzwingen die festen Regeln der Sprache eine in sich schlüssige Darstellung. Aufgrund dieser Erkenntnis wird in der vorliegenden Arbeit eine Logik zur Beschreibung der an der Verifikation beteiligten Prozesse vorgestellt. Die hier vorgestellte Signatur-BAN (SigBAN) zur Modellierung der Verifikation von digitalen Signaturen beruht auf einer Modifizierung und Erweiterung der BAN-Logik. Die BAN-Logik wurde Mitte der 90er Jahre von Burrows, Abadi und Needham zur Untersuchung von Authentisierungsprotokollen entworfen. Als Grundlage nutzen diese Protokolle dieselben kryptographischen Verfahren wie digitale Signaturen. Allerdings gelten für die Überprüfung von Signaturen andere Anforderungen als bei der Protokollanalyse. Diesen veränderten Bedingungen wird in den Axiomen der SigBAN-Logik Rechnung getragen. Basierend auf den ermittelten Axiomen und einem Teil der BAN-Regeln wird die SigBAN-Syntax definiert. Im Anschluss an die Definition der SigBAN-Logik werden ihre Einsatzmöglichkeiten an unterschiedlichen Beispielen demonstriert. Anhand mehrerer PKI-Anordnungen wird nicht nur der praktische Einsatz, sondern auch die Vollständigkeit und Widerspruchsfreiheit der logischen Beschreibungsform veranschaulicht. Besonderes Augenmerk liegt dabei auf einer Analyse der Verifikation nach dem deutschen Signaturgesetz (SigG). Mit Hilfe der SigBAN-Logik werden Probleme bei einem SigG-konformen Zeitstempeldienst erkannt und ein Verbesserungsvorschlag erarbeitet. Auch bei den Gültigkeitsmodellen nach dem SigG werden Lücken nachgewiesen, die das SigBAN-Modell vermeidet.     «

Die Bedeutung von digitalen Signaturen und ihre Anwendung in den verschiedensten Bereichen der Gesellschaft, Industrie und Politik nimmt stetig zu. In vielen Fällen wird in Zukunft die digitale Unterschrift einer manuellen gleichgestellt sein. Infolgedessen steigt der Bedarf nach leistungsfähigen Werkzeugen und Methoden für die Qualifizierung und Analyse von Prozessen zur Verarbeitung digitaler Signaturen. Diese Arbeit befasst sich mit allgemeingültigen Kriterien zur vollständigen Verifikation e...     »

Digital signatures and their applications in society, industry and politics are becoming increasingly important. There are a lot of cases in which a digital signature is equivalent to a handwritten signature. Consequently a need arises for tools and methods which qualify and analyse the processes involved in the generation and verification of digital signatures. This paper concerns universally applicable criteria necessary to verify a digital signature. There are technical considerations which are necessary in determining the validity of a digital signature aside from legal aspects and other defined rules. The main topics of this paper are the technical validation of digital signatures and a proposal for a new logic for this purpose. This logic enables the derivation of obvious and consistent conclusions about the validity of a digital signature. The formal derivation is based on the characteristics of a Public Key Infrastructure (PKI), which is described by the symbols defined in the introduction of the logic. It is necessary to define exact validity requirements for the realisation of software which make use of digital signatures. In particular, applications from different vendors have to arrive at the same result when applying common criteria. In most cases these criteria are part of the agreed specifications of the PKI. However, as shown in chapter 6, these specifications can be inconsistent and incomplete. This can be avoided by the additional formal description of the processes involved in the verification. Formal rules enforce a consistent specification and help to avoid logical gaps. In this light, a proposal is made for a new logic in the description of the processes involved in the verification of digital signatures. The Signature-BAN (SigBAN) logic, introduced in this paper, is based on several modifications and extensions to the BAN logic. The BAN logic was developed by Burrows, Abadi and Needham for the analysis of authentication protocols in 1989. Moreover, authentication protocols are based on the same cryptographic principles as digital signatures. The verification of digital signatures, however, differs from the analysis of authentication protocols. For this reason the SigBAN logic is based on completely newly developed axioms. As a result the SigBAN syntax differs from the BAN syntax. After the definition, the SigBAN logic is applied to different examples. Practical use, completeness and the lack of contradictions are shown by the analysis of different PKIs. Particular attention is paid to the analysis of the verification processes according to the interoperability specifications of the German signature act (SigG/SigV). Additionally, a proposal to improve the SigG time stamping service is developed with SigBAN syntax. Inconsistencies in the two different SigG validity models are shown by a comparison with SigBAN.     «

Digital signatures and their applications in society, industry and politics are becoming increasingly important. There are a lot of cases in which a digital signature is equivalent to a handwritten signature. Consequently a need arises for tools and methods which qualify and analyse the processes involved in the generation and verification of digital signatures. This paper concerns universally applicable criteria necessary to verify a digital signature. There are technical considerations which a...     »