Security proofs 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 goal of this thesis is to formalize a security proof in EasyCrypt of some (preferably practically relevant) cryptographic protocol. Which protocol is to be studied would be decided based on the student’s preferences after the initial literature review.
The goal of this thesis is to formalize a security proof in EasyCrypt of some (preferably practically relevant) cryptographic protocol. Which protocol is to be studied would be decided based on the student’s preferences after the initial literature review.
Graduation Theses defence year
2019-2020
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