EasyCrypt Tutorials

Here is a collection of slides giving example-driven introductions to some features of the EasyCrypt proof assistant. These were developed in connection with the course Formal Methods in Security and Privacy that I co-teach with Marco Gaboardi.

• EasyCrypt's Ambient Logic
• EasyCrypt's While Language and Hoare logic
• EasyCrypt's Relational Hoare Logic and proving noninterference results
• EasyCrypt's Probabilistic Relational Hoare Logic and proving probabilistic noninterference results (prob-noninter.ec)
• EasyCrypt's Probabilistic Hoare Logic, and using it in conjunction with Probabilistic Relational Hoare Logic and Ambient Logic (phl-prhl.ec)