Rewinding in EasyCrypt
Organization
Cryptography
Abstract
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?
[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. 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?
[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.]
Graduation Theses defence year
2017-2018
Supervisor
Dominique Unruh
Spoken language (s)
English
Requirements for candidates
Crypto I, if possible Crypto II, Introduction to Interactive Theorem Provers
Level
Masters
Keywords
Application of contact
Name
Dominique Unruh
Phone
E-mail