 |
|
|||
| Kontakt | Index | Suche | Rundgang | English |
Proceedings: PDF
16:00 Protokolle zur Gewährleistung gegenseitiger Anonymität (Anna Fricke)
Dieses Paper beschäftigt sich mit Protokollen, die genseitige Anonymität gewährleisten sollen. Ein zentrales Problem von Peer-to-Peer Systemen ist die Wahrung der Anonymität zwischen Initiator und Responder während des Informationsaustausches. Viele bereits existierende Lösungen ereichen gegenseitige Anonymität in reinen Peer-to-Peer Systemen ohne eine vertrauenswürdige zentrale Kontrollinstanz. Ein bekanntes Beispiel ist das Freenet Protokoll. Zum Vergleich wird das "Mix-Based Protokoll" vorgestellt, das von der Existenz eines vertrauenswürdigen Indexservers ausgeht. Um Lauffähigkeit und Korrektheit solcher Protokolle zu testen bzw. zu beweisen, benötigt man eine formale Spezifikation. Unter Verwendung der Rewriting Engine Maude wird ein Beispiel einer Spezifikation des "Mix-Based Protokolls" erläutert. Im zweiten Teil des Papers wird ein weiteres Protokoll die "Dining Cryptographers" und eine mögliche Spezifikation in Maude betrachtet, die auf dem Modell eines Petrinetztes aufbaut. Diese Spezifikation des Protokolls wird durch Model-Checking verifiziert.
10:15 Ein Vergleich zwischen Model-Checking und Theorem-Proving (Daniel Schradick)
Viele Ansätze und Methoden wurden entwickelt, um die Sicherheit und Zuverlässigkeit von Computersystemen zu garantieren. Ein vielversprechender Ansatz ist es, formale Methoden in allen Phasen des Softwareentwicklungsprozesses zu verwenden. Sie setzen Techniken aus mathematischer Logik und diskreter Mathematik ein, um Systeme zu beschreiben, spezifizieren, konstruieren und verifizieren. Ihre Verwendung ermöglicht es, das Verhalten unter bestimmten Annahmen sowie die Eigenschaften eines Systems explizit beschreiben. Dies ermöglicht, mittels der zugrundegelegten Logik über das System mit Inferenzregeln zu schlie?en und dadurch Eigenschaften des Systems zu beweisen. Der Nachteil der formalen Methoden liegt darin, dass sie zum Teil schwer anzuwenden und sehr zeitintensiv sind. Dies betrifft zum einen die genauen mathematischen Beschreibungen und Spezifikationen des Systems, aber vor allem die Beweisführung, auf deren verschiedene Arten in diesem Bericht genauer eingegangen werden soll. Es gibt zwei Hauptzweige in der Verifikation, welche durch die Art des Vorgehens bei der Beweisführung gekennzeichnet sind die man mit Theorem Proving und Model Checking bezeichnet.
11:15 Implementation of the spi-calculus (Jens Grabarske)
The verification of computer processes is becoming more and more important. To be able to express concurrent processes the π-calculus by Robert Milner can be used. The spi calculus is a superset of the π-calculus that allows the user to describe the encryption and decryption of messages using either shared keys or public/private key pairs. The design for an implementation of the spi calculus in Maude is discussed.
12:30 Verifikation des Yahalom-Protokolls (Thilo Mende)
Das Yahalom-Protokoll dient der Verteilung eines gemeinsamen, geheimen Schlüssels mit gegenseitiger Authentifizierung unter Verwendung eines vertauenswürdigen Dritten. Um die Sicherheit eines solchen Protokolls zu garantieren ist eine formale Verifikation nötig, ein möglicher Ansatz dazu ist der Model-Check einer Spezifikation des Protokolls. Mit Hilfe der Rewriting-Engine Maude kann eine solche Spezifikation schon während der Entwicklung getestet werden und diese somit erheblich vereinfachen und beschleunigen, was anhand des Yahalom-Protokolls und unter Einsatz der objektorientierten Erweiterungen zu Maude demonstriert wird. Anschließend wird die entstandene Spezifikation an den für Maude verfügbaren Model-Checker angepasst und auf Sicherheitsprobleme hin untersucht werden.
Korrekturen, Anmerkungen bitte an
Berndt Farwer
Letzte Änderung: 7.7.2004
http://www2.informatik.uni-hamburg.de/tgi/lehre/vl/SS04/mb/