Comparison of theorem provers for cryptographic protocols
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.
Graduation Theses defence year
Spoken language (s)
Requirements for candidates
Crypto I, if possible Crypto II, Introduction to Interactive Theorem Provers
Application of contact