Comparison of theorem provers for cryptographic protocols
Organisatsiooni nimi
Cryptography
Kokkuvõte
When checked by humans, the security of proofs for cryptographic
protocols are inherently error-prone. One way out is to use formal
(i.e., computer-aided) verification. Several frameworks for such
verification exist these days, such as EasyCrypt, CertiCrypt,
CryptoVerif, Foundational Cryptography Framework, CryptHOL. The task
of this thesis is to survey and compare the existing approaches, and
to identify and study their respective strengths and weaknesses.
[All thesis topics should be seen as suggestions. Students are
encouraged to discuss variations of these topics with me. The topics
are designed for master theses, however, interested bachelor students
can contact me to discuss "down-scaled" topics suitable for a bachelor
thesis.]
protocols are inherently error-prone. One way out is to use formal
(i.e., computer-aided) verification. Several frameworks for such
verification exist these days, such as EasyCrypt, CertiCrypt,
CryptoVerif, Foundational Cryptography Framework, CryptHOL. The task
of this thesis is to survey and compare the existing approaches, and
to identify and study their respective strengths and weaknesses.
[All thesis topics should be seen as suggestions. Students are
encouraged to discuss variations of these topics with me. The topics
are designed for master theses, however, interested bachelor students
can contact me to discuss "down-scaled" topics suitable for a bachelor
thesis.]
Lõputöö kaitsmise aasta
2017-2018
Juhendaja
Dominique Unruh
Suhtlemiskeel(ed)
inglise keel
Nõuded kandideerijale
Crypto I, if possible Crypto II, Introduction to Interactive Theorem Provers
Tase
Magister
Märksõnad
Kandideerimise kontakt
Nimi
Dominique Unruh
Tel
E-mail