Please use this identifier to cite or link to this item: doi:10.22028/D291-26528
Title: Formal verification of cryptographic security proofs
Author(s): Berg, Matthias
Language: English
Year of Publication: 2013
SWD key words: Verifikation
Kryptologie
Sicherheit
Free key words: verification
cryptography
security
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: 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 to this record: urn:nbn:de:bsz:291-scidok-54698
hdl:20.500.11880/26584
http://dx.doi.org/10.22028/D291-26528
Advisor: Backes, Michael
Date of oral examination: 9-Aug-2013
Date of registration: 16-Aug-2013
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
thesis_berg.pdf1,62 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.