Cryptography is widely used in many protocols but rarely implemented by someone with a clear idea of what they were doing.
This project involves the analysis of systems using cryptography through an interactive theorem prover.
Relevant background material is cryptography and the programming experience. Experience with interactive theorem provers is a plus but not required.