My final year project existed at an interesting crossroads of programming languages and cryptography - the official title of which was "Programming Language Theory Applications for Verified Cryptography in EasyCrypt" which is by far a mouthful. In hindsight a more apt title would be "Type Classes for Verified Cryptography".
The core focus of this project was work on a language called EasyCrypt which the maintainers describe as the following
EasyCrypt is a toolset for reasoning about relational properties of
probabilistic computations with adversarial code. Its main application
is the construction and verification of game-based cryptographic proofs.
When we reference "game based cryptography" we are talking about models of security which when proven for a crypto-scheme highlight some behaviour i.e. what is the probability of correctly guessing a private key used for an encryption when you have access to an oracle that can perform encryption for you. The scope of EasyCrypt's functionality is vast and it has been used to prove a wide range of schemes in its time.
So what was my dissertation? Essentially EasyCrypt has a few limitations in terms of the expressivity of the language. One has to consider that languages like EasyCrypt allow us to verify crypto-schemes by allowing us to construct the schemes in the language and performing verification via the compiler. This construction is the real challenge that exists with any proof assistant; we require a language that is expressive as possible so that this translation from crypto-schemes (mathematics) to code is as easy as possible. My project was on implementing type classes - an idea popular in most functional programming languages - so that EasyCrypt's expressiveness could be extended.
This project was arguably my most enjoyable throughout my time at university. A full copy of my dissertation can be accessed here which goes over all the nitty-gritty details.
Top comments (0)