Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26528
Titel: Formal verification of cryptographic security proofs
Verfasser: Berg, Matthias
Sprache: Englisch
Erscheinungsjahr: 2013
SWD-Schlagwörter: Verifikation
Kryptologie
Sicherheit
Freie Schlagwörter: verification
cryptography
security
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: Verifying cryptographic security proofs manually is inherently tedious and error-prone. The game-playing technique for cryptographic proofs advocates a modular proof design where cryptographic programs called games are transformed stepwise such that each step can be analyzed individually. This code-based approach has rendered the formal verification of such proofs using mechanized tools feasible. In the first part of this dissertation we present Verypto: a framework to formally verify game-based cryptographic security proofs in a machine-assisted manner. Verypto has been implemented in the Isabelle proof assistant and provides a formal language to specify the constructs occurring in typical cryptographic games, including probabilistic behavior, the usage of oracles, and polynomial-time programs. We have verified the correctness of several game transformations and demonstrate their applicability by verifying that the composition of 1-1 one-way functions is one-way and by verifying the IND-CPA security of the ElGamal encryption scheme. In a related project Barthe et al. developed the EasyCrypt toolset, which employs techniques from automated program verification to validate game transformations. In the second part of this dissertation we use EasyCrypt to verify the security of the Merkle-Damgård construction - a general design principle underlying many hash functions. In particular we verify its collision resistance and prove that it is indifferentiable from a random oracle.
Kryptographische Sicherheitsbeweise manuell zu überprüfen ist mühsam und fehleranfällig. Spielbasierte Beweistechniken ermöglichen einen modularen Beweisaufbau, wobei kryptographische Programme - sog. Spiele - schrittweise so modifiziert werden, dass jeder Schritt einzeln überprüfbar ist. Dieser code-basierte Ansatz erlaubt die computergestützte Verifikation solcher Beweise. Im ersten Teil dieser Dissertation präsentieren wir Verypto: ein System zur computergestützten formalen Verifikation spielbasierter kryptographischer Sicherheitsbeweise. Auf Grundlage des Theorembeweisers Isabelle entwickelt, bietet Verypto eine formale Sprache, mit der sich kryptographische Eigenheiten wie probabilistisches Verhalten, Orakelzugriffe und polynomielle Laufzeit ausdrücken lassen. Wir beweisen die Korrektheit verschiedener Spieltransformationen und belegen deren Anwendbarkeit durch die Verifikation von Beispielen: Wir zeigen, dass Kompositionen von 1-1 Einwegfunktionen auch einweg sind und dass die ElGamal Verschlüsselung IND-CPA sicher ist. In einem ähnlichen Projekt entwickelten Barthe et al. das EasyCrypt System, welches Spieltransformationen mit Methoden der Programmanalyse validiert. Im zweiten Teil dieser Dissertation verwenden wir EasyCrypt und verifizieren die Sicherheit der Merkle-Damgård Konstruktion - ein Designprinzip, das vielen Hashfunktionen zugrunde liegt. Wir zeigen die Kollisionsresistenz der Konstruktion und verifizieren, dass sie sich wie ein Zufallsorakel verhält.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-54698
hdl:20.500.11880/26584
http://dx.doi.org/10.22028/D291-26528
Erstgutachter: Backes, Michael
Tag der mündlichen Prüfung: 9-Aug-2013
SciDok-Publikation: 16-Aug-2013
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
thesis_berg.pdf1,62 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.