Refine
Year of publication
Document Type
- Diploma Thesis (46) (remove)
Language
- German (46)
Has Fulltext
- yes (46)
Is part of the Bibliography
- no (46)
Keywords
- Algebraische Gleichung (1)
- BMRT (1)
- BRDF (1)
- BTF (1)
- Beleuchtungsmodell (1)
- Computerlinguistik (1)
- Contextual Equivalence (1)
- Echtzeitprogrammierung (1)
- GPI (1)
- Gleichheitsanalyse (1)
Institute
- Informatik (46) (remove)
Die Implementation der Striktheits-Analyse, die im Zuge dieser Arbeit vorgenommen wurde, stellt eine effiziente Approximation der abstrakten Reduktion mit Pfadanalyse dar. Durch die G#-Maschine, ein neues, auf der G-Maschine basierendes Maschinenmodell, wurde die verwendete Methode systematisch dargelegt. Die große Ähnlichkeit mit der G-Maschin, die in unserer Implementation beibehalten werden konnte, zeigt, wie natürlich die verwendete Methode der Reduktion in funktionalen Programmiersprachen entspricht. Obwohl die Umsetzung mehr Wert auf Nachvollziehbarkeit, als auf Effizienz legt, zeigt sie, daß die Methode der abstrakten Reduktion mit Pfadanalyse auch in einer funktionalen Implementierung durchaus alltagstauglich ist und Striktheits-Information findet, die Umsetzungen anderer Methoden nicht finden. Es bestehen Möglichkeiten zur Optimierung u. a. von Programmteilen, die für jede simulierte G#-Maschinen-Anweisung ausgeführt werden. Bei vorsichtiger Einschätzung erscheint eine Halbierung der Laufzeit mit vertretbarem Aufwand erreichbar.
In Abschnitt 4.1 wurden Algebren auf Mengen und Relationen vorgestellt. Desweitern wurde in Abschnitt 4.2 eine zu ALC erweiterte terminologische Wissensrepräsentationssprache ALCX definiert und gezeigt, daß die in Abschnitt 4.1 vorgestellten Algebren zur Festlegung der odell-theoretischen Semantik der Sprache ALCX benutzt werden können. Als Ergebnis einer derartigen Festlegung kann jeder terminologische Ausdruck direkt mit einem algebraischen Term assoziiert werden. Desweitern können alle in den Algebren aufgeführten universellen Identitäten in semantisch äquivalente terminologische Identitäten überführt werden. Eine mittels ALCX repräsentierte Wissensbasis ist in meinem Programm mit Hilfe der in der funktionalen Programmiersprache Gofer (Version 2.28) gegebenen Möglichkeiten formuliert. Mein Programm bietet durch Simplifizierung von Anfrageausdrücken eine optimierte Lösung des aus dem Bereich der Wissensrepräsentation bekannten Retrieval-Problems. Die Simplifizierung von Anfrageausdrücken wird in meinem Programm erzielt, indem in den oben genannten Algebren erfüllte universelle Identitäten als Simplifikationshilfsmittel benutzt werden. Die in den Algebren aufgeführten universellen Identitäten bestehen stets aus zwei äquivalenten Termen, für die eine unterschiedliche Anzahl von Reduktionsschritten zur Evaluierung benötigt werden. Es existieren universelle Identitäten, bei denen unabhängig von den Instanzen der Argumentterme ein Term gegenüber einem anderen Term effizienter auswertbar ist. Bei diesen universellen Identitäten kann eine Simplifikation von einem Term zu einem anderen Term immer unproblematisch realisiert werden. Es gibt jedoch auch universelle Identitäten, bei denen die Unabhängigkeit von den Instanzen der Argumentterme nicht gegeben ist. In diesen Fällen wird ein von der Wissensbasis abhängiges Komplexitätsabschätzungsverfahren eingesetzt, um den effizienter auswertbaren Term von zwei an einer universellen Identität beteiligten Termen zu ermitteln. Daß die Simplifikation eines Anfrageausdrucks große Einsparungen bei dessen Auswertung nach sich ziehen kann, wurde an verschiedenen Beispielen in Abschnitt 5.4.4 gezeigt. Über eine weitere Möglichkeit, die zum Simplifizieren von Anfrageausdrucken verwendet werden kann, wurde in Abschnitt 5.4.5 berichtet. Die Genauigkeit der Komplexitätsabschätzung kann erhöht werden, indem das Komplexitätsabschätzungsverfahren erweitert wird. So kann beispielsweise die Komplexität der Funktion "oder" genauer abgeschätzt werden, indem für zu vereinigende Mengen überprüft wird, ob Teilmengenbeziehungen vorhanden sind. Durch eine genauere Abschätzung der Mächtigkeit entstehender Vereinigungsmengen wird die Komplexitätsabschätzung insgesamt in ihrer Genauigkeit gesteigert. Eine Änderung der Instanzen meiner terminologischen Datenbank erfordert eine Änderung des Skripts meines Programms. Indem die Instanzen-Daten in einer veränderlichen Datenbank festgehalten würden, könnte hier Abhilfe geschaffen werden. Dies könnte im Rahmen der Erstellung einer benutzterfreundlichen Ein- und Ausgabe-Schnittstelle realisiert werden.
A und B möchten digitale Unterschriften auf faire Weise austauschen, d.h. A soll genau dann eine Unterschrift von B erhalten, wenn B eine Unterschrift von A erhält. Der triviale Ansatz zum Austausch zweier Unterschriften, daß A seine Unterschrift an B sendet und dann B seine Unterschrift an A schickt, ist nicht fair, da B nach Erhalt der Unterschrift von A das Protokoll vorzeitig beenden oder eine ungültige Unterschrift senden kann. Bei den bekannten praktikablen Protokollen zum fairen Austausch unterteilen die Teilnehmer die Unterschriften in kleine Blöcke aus wenigen Bits und tauschen die Blöcke dann schrittweise aus. Diese Protokolle garantieren einerseits, daß man sofort überprüfen kann, ob ein erhaltener Block korrekt ist. Andererseits geben die bereits ausgetauschten Blöcke so wenig wie möglich über den restlichen Teil der Unterschrift preis. Versucht in diesem Fall ein Teilnehmer zu betrügen, indem er beispielsweise einen falschen Wert sendet, so kann der andere Teilnehmer dies unmittelbar bemerken und stoppen. Da die noch nicht ausgetauschten Blöcke fast nichts über den übrigen Teil der Unterschrift preisgeben, hat der Betrüger höchstens einen Block mehr als der ehrliche Teilnehmer erhalten. Ist die Blockgröße hinreichend klein, kann der ehrliche Teilnehmer den Nachteil durch Raten bzw. Probieren ausgleichen. In dieser Diplomarbeit entwickeln wir Protokolle zum fairen Austausch sogenannter Diskreter- Logarithmus-Unterschriften. Die bekannten praktikablen Protokolle zum Austausch dieses Unterschriftentyps verwenden als Sicherheitsvoraussetzung die Faktorisierungsannahme. Im Unterschied dazu beruht die Sicherheit unseres Austauschprotokolls auf der Diskreten- Logarithmus-Annahme und damit auf der des Unterschriftenverfahrens. Ferner erlauben unsere Protokoll die Herausgabe der Blöcke in beliebiger, auch vom Protokollverlauf abhängiger Reihenfolge, während die Reihenfolge bei den bisherigen Protokollen von vornherein festgelegt ist.
Um in verschiedenen Anwendungsumgebungen eingesetzt werden zu können, lässt die CORBA-Spezifikation einen weiten Spielraum für Implementierungen. Sollte CORBA in einem speziellen Umfeld eingesetzt werden, so war bisher eine Neu-Implementierung notwendig, da herkämmliche CORBA-Implementierungen nicht oder nur sehr eingeschränkt an spezielle Anwendungsumgebungen anpassbar sind. In dieser Arbeit wurde ein Ansatz für eine erweiterbare CORBA-Implementierung vorgestellt und implementiert.
Wir betrachten das auf der Crypto '97 vorgeschlagene gitterbasierte Kryp- tosystem von Goldreich, Goldwasser und Halevi (GGH) [11]. Die Autoren veröffentlichten Challenges zu den Sicherheitsparametern 200, 250, 300, 350 und 400 [12]. Jeder Challenge besteht aus dem öffentlichen Schlüssel, sowie einem Ciphertext. Für den Angriff entwickeln wir numerisch stabile Gitterreduktionsalgorithmen, die es ermöglichen, das System in diesen Dimensionen anzugreifen. Es werden Methoden zur Orthogonalisierung, die sogenannten House- holder-Reflexionen und Givens-Rotationen behandelt, und eine praktikable Gleitpunkt-Arithmetik Version des LLL-Algorithmus nach Lenstra, Lenstra und Lov'asz [16] angegeben. Wir entwickeln und analysieren den LLL-Block- Algorithmus, der die Gitterreduktion in Blöcken organisiert. Die Gleitpunkt-Arithmetik Version des LLL-Block-Algorithmus wird experimentell auf das GGH-Schema angewendet und mit der LLL-Reduktion in den Dimensio- nen 100 bis 400 verglichen. Neben der besseren numerischen Stabilität ist die LLL-Block-Reduktion um den Faktor 10 bis 18 mal schneller als die gewöhnliche LLL-Reduktion. Das GGH-Kryptosystem wurde ebenfalls von Nguyen [22] angegriffen, und die ursprünglichen Nachrichten wurden bis in Dimension 350 rekonstruiert. Wir stellen weitere Angriffe auf das Kryptosystem vor. Es zeigt sich, dass die öffentlichen Parameter für erfolgreiche Angriffe benutzt werden können. Der private Schlüssel in der Dimension 200 wird nach ca. 10 Stunden rekonstruiert und Ciphertext-Attaken sind bis in Dimension 300 erfolgreich.
In der vorliegenden Diplom-Arbeit wurde das in [19] vorgeschlagene Modell zur Partitionierung hybrider Systeme diskutiert und die Anwendbarkeit verschiedener verschiedener Optimierungsverfahren auf das Problem untersucht.
Hierbei wurde der Systemgraph um die Ein-/Ausgabe-Blöcke erweitert, damit der Systemgraph eine eine konsistente Erweiterung des des Graphen-Modells darstellt. Weiterhin wurden die Probleme und Einschränkungen aufgezeigt, die sich bei der Abbildung eines hybriden Systems auf den Systemgraphen ergeben.
Gegenstand der Arbeit ist ein Gleichheitskalkül für den Kern einer nicht-strikten funktionalen Programmiersprache. Funktionale Programmiersprachen unterstützen bestens die Prinzipien Abstraktion, Einkapselung, Hierarchiesierung und Modularisierung, die gemeinhin als Grundelemente des Software-Engineering betrachtet werden. Darüber hinaus bieten funktionale Programmiersprachen aufgrund ihrer Entwicklung aus dem Lambda-Kalkül eine große Nähe zu mathematischen Modellen. Daher besitzen sie im Bereich der Programmverifikation ausgeprägte Vorteile gegenüber imperativen oder objekt-orientierten Programmiersprachen. In der Arbeit wird nun ein Gleichheitsbegriff für Ausdrücke in funktionalen Programmiersprachen entwickelt und dessen Praktikabilität durch die Implementierung eines Beweisers untermauert. Dieser Gleichheitsbegriff ist die kontextuelle Gleichheit, die Ausdrücke aufgrund ihres Terminierungsverhaltens als Unterprogramme in allen möglichen Kontexten einordnet. Kontextuelle Gleichheit wird in Kapitel 2 vorgestellt, nachdem der klassische und der sogenannte "lazy" Lambda-Kalkül eingeführt wurden. Kapitel 3 enthält einen Überblick über die funktionale Programmierung, da auch die Implementierung des o.g. Beweisers in einer funktionalen Programmiersprache, nämlich Haskell, durchgeführt wird. In Kapitel 4 wird die funktionale Kernsprache, die Gegenstand der Untersuchung sein wird, beschrieben. Sie enthält alle wesentlichen Elemente wie z.B. Funktionsdefinition und -anwendung sowie Datentypen. Im selben Kapitel wird auch der Gleichheitsbegriff für diese Kernsprache definiert. Kapitel 5 schließlich entwickelt auf Basis der zuvor erfolgten Definitionen einen Kalkül für den Gleichheitsbeweis. Außerdem wird in diesem Kapitel auch die Umsetzung dieses Gleichheitskalküls präsentiert. Aus der Dissertation von Marko Schütz werden hierbei Erkenntnisse über die Kontextanalyse verwendet, um erfüllende Belegungen von freien Variablen zu berechnen. Die Arbeit schließt mit Beispielanalysen und Meßwerten sowie einer Diskussion der Ergebnisse und möglicher Erweiterungen.
Wir betrachten in dieser Diplomarbeit die Sicherheit des ringbasierten Public Key Kryptosystems NTRU, das 1996 von J. Hoffstein, J. Pipher und J.H. Silverman vorgeschlagen wurde. Dieses Kryptosystem bietet schnelle Kodierung und Dekodierung in Laufzeit O(n exp 2) bei kleinem Sicherheitsparameter n. Die Sicherheit des Systems beruht auf einem Polynomfaktorisierungsproblem (PFP)im Polynomring Zq[X]/(X exp n -1). Das PFP wurde von Coppersmith und Shamir auf ein Kürzestes Vektor Problem im Gitter Lcs reduziert. Die neuen Ergebnisse dieser Arbeit bauen auf dem Gitter Lcs auf. Wir betrachten die Nachteile von Lcs und konstruieren verbesserte Gitterbasen zum Angriff auf das NTRU-Kryptosystem. Dabei nutzen wir Strukturen des Polynomrings Zq[X]/(X exp n -1) und der geheimen Schlüssel aus. Durch die neuen Gitterbasen wird der Quotient aus der Länge des zweitkürzesten und der Länge des kürzesten Gittervektors vergrößert. Da wir Approximationsalgorithmen zum Finden eines kürzesten Vektors verwenden, beschleunigt dies die Attacken. Wir präsentieren verschiedene Methoden, wie man die Dimension der Gitterbasen verkleinern kann. Durch die verbesserten Gitterattacken erhalten wir eine Cryptanalyse des NTRU-Systems in der vorgeschlagenen mittleren Sicherheitsstufe. Beträgt die Zeit zum Brechen eines Public-Keys unter Verwendung der Coppersmith/Shamir-Basis 1 Monat, so verringert sich die Laufzeit durch einen kombinierten Einsatz der neuen Gitterbasen auf ca. 5 Stunden auf einem Rechner und bei Parallelisierung auf ca. 1:20 Stunde auf 4 Rechnern. Wir erwarten, daß die neuen Methoden NTRU in hoher Sicherheitsstufe n = 167 brechen, obwohl für dieses n bisher nur "schwache" Schlüssel gebrochen wurden. Trotz signifikanter Verbesserungen deuten die experimentellen Ergebnisse auf ein exponentielles Laufzeitverhalten bei steigendem Sicherheitsparameter n hin. Der Laufzeitexponent kann allerdings gesenkt werden, so daß man n größer wählen muß, um Sicherheit gegenüber den neuen Attacken zu erzielen. Auch wenn das NTRU-Kryptosystem nicht vollständig gebrochen wird, verliert es seinen größten Vorteil gegenüber anderen Public Key Kryptosystemen: Die effiziente Kodierung und Dekodierung bei kleinem Sicherheitsparameter n.
Ziel dieser Arbeit war es, ein System zu entwickeln, mit dem Sätze von Reduktionsdiagrammen auf ihre Vollständigkeit überprüft werden können. Das System sollte in der puren, funktionalen Programmiersprache Haskell realisiert werden und speziell auf einen nichtdeterministischen Kalkül mit Konstruktoren, einem case-Konstrukt und einem rekursiven let- Ausdruck (letrec) ausgerichtet sein. Dazu wurde in Kapitel 2 der lambda-Kalkül und funktionale Programmiersprachen eingeführt, um die Entwicklung der Kalküle lambda-nd und lambda-nd,rec zu motivieren. Die Basis-Kalküle lambda-nd und lamda-nd,rec wurden in Kapitel 3 bezüglich ihrer Sprachdefinition und Reduktionsregeln vorgestellt. Die Implementierung der beiden Kalküle und der Parser für die verwendete Kernsprache wurden ebenso angegeben wie die Mechanismen zur Markierung und Reduktion der Terme. Die Unterscheidung eines reduzierbaren Terms in NO- und internen Redex, sowie deren Erkennung wurde in diesem Kapitel besonders herausgestellt, da sie die Grundlage für die zu validierenden Reduktionsdiagramme darstellt. Damit ist der Grundstock für diese Arbeit gelegt worden. In Kapitel 4 haben wir kurz Methoden vorgestellt, die lamda-Kalkülen und deren Derivate eine Bedeutung zuzumessen versuchen, um Programme oder Terme miteinander vergleichen zu können. Also nicht nur ihre Termstruktur, sondern ihr Verhalten zu vergleichen. Dabei ist festgestellt worden, daß für nichtdeterministische Kalküle nur eine Methode verfügbar ist, und zwar die der kontextuellen Äquivalenz. Da wir gängige Programmtransformationen dahingehend überprüfen wollten, ob sie der kontextuellen Äquivalenz genügen, also nicht die Auswertung oder das Ergebnis derselben verändern, haben wir ein Kontext-Lemma vorgestellt. Mit Hilfe des Kontext-Lemmas ist es uns möglich gewesen, die Gültigkeit von Beweisen in Reduktionskontexten auf beliebige Kontexte auszudehnen. Für die eigentlichen Beweise werden Reduktionsdiagramme benötigt, die Reduktionsfolgen in verschiedener Weise umstellen. Wir haben die Reduktionsdiagramme ebenfalls in Kapitel 4 definiert. Die Reduktionsdiagramme müssen an jeder Stelle einer Reduktionsfolge anwendbar sein, da sonst die Äquivalenz-Beweise nicht möglich sind. D. h. es müßte bewiesen werden, daß mindestens ein Reduktionsdiagramm einer definierten Menge von Reduktionsdiagrammen für jeden Term und jede seiner Reduktionsfolgen anwendbar ist. Der naive Weg wäre, alle Terme und seine Reduktionsfolgen dahingehend zu überprüfen. Da dies jedoch nicht möglich ist, haben wir uns dazu entschlossen so viele Terme wie möglich zu untersuchen, nicht um die Vollständigkeit der Diagramme zu beweisen, sondern um zu zeigen, daß auf viele verschiedenartige Terme Reduktionsdiagramme erfolgreich angewendet werden können. Die Generierung der Terme haben wir in Kapitel 5 ausführlich dargestellt. In Kapitel 6 haben wir die Sprache zur Darstellung von Reduktionsdiagrammen und die Implementierung der Diagramm-Validierung beschrieben. Weiterhin haben wir ein Verfahren vorgestellt, mit dem wir fehlende Diagramme für Terme suchen und meist auch finden können. Das gesamte System haben wir so aufgebaut, daß eine große Menge an Termen generiert wird, für die Diagramme anwendbar sein müssen. Wenn keines der Diagramme auf einen Term anwendbar ist, also nicht validiert werden kann, dann wird ein passendes Diagramm gesucht. Mit Hilfe des entwickelten Systems Jonah sind in Kapitel 7 verschiedene Programmtransformationen dahingehend überprüft worden, ob die angegebenen Reduktionsdiagramme für große Mengen von Termen gültig sind. Dabei ist als Ergebnis herausgekommen, daß ein vollständiger Satz an Reduktionsdiagrammen für die (cp)-Reduktion nur sehr schwer zu finden ist. Selbst neu hinzugefügte Transformationen, die dabei helfen sollten, die Schwierigkeiten zu umgehen, konnten nicht verwendet werden, da es uns ebenfalls nicht möglich gewesen ist, für sie vollständige Diagrammsätze zu finden. Daraufhin haben wir den Basis-Kalkül zweimal erweitert, um die Schwierigkeiten der (cp)-Diagramme in den Griff zu bekommen. Aber auch diese Ansätze haben kein zufriedenstellendes Ergebnis geliefert. Als positives Ergebnis dieser Arbeit kann aber festgestellt werden, daß das System Jonah bei der Entwicklung nichtdeterministischer Kalküle auf Basis von lambda-Kalkülen eine sehr gute Hilfestellung sein kann, auch wenn es nicht zum vollständigen Beweis der Gültigkeit von Reduktionsdiagrammen dienen kann.