Linking CryptoVerif and EasyCrypt

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. Probably the most popular tool
today for this purpose is EasyCrypt, which allows to interactively
design a proof that the computer will be able to understand and
check. Another popular tool is CryptoVerif which takes a very
different, and more automated approach. EasyCrypt seems to be more
powerful, yet lacks automation. A combination of the two approaches
would be helpful.

The aim of this thesis is to link CryptoVerif and EasyCrypt. Can a
CryptoVerif proof be transformed ("compiled") into an EasyCrypt proof?
This would allow us to do some proofs in CryptoVerif (where possible)
and then combine them in EasyCrypt with proofs that can only be
performed in EasyCrypt.

[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
#tcs #crypto #verification

Kandideerimise kontakt

 
Nimi
Dominique Unruh
Tel
E-mail
unruh@ut.ee