Applying programming language theory to EasyCrypt: a language for formal verification of cryptography