Rewinding in 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.
The task of this thesis is to study the applicability of EasyCrypt to proofs that use "rewinding". Such proofs include, for example, security proofs for commitment schemes and zero-knowledge protocols. Can the logic in EasyCrypt already capture such techniques? If not, how should it be extended?
The task of this thesis is to study the applicability of EasyCrypt to proofs that use "rewinding". Such proofs include, for example, security proofs for commitment schemes and zero-knowledge protocols. Can the logic in EasyCrypt already capture such techniques? If not, how should it be extended?
Lõputöö kaitsmise aasta
2019-2020
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