Verifying Cryptographic Implementations with F*

Course at Summer School on Models and Tools for Cryptographic Proofs, Nancy, France, 10-13 July 2017

Lecturers: Cătălin Hriţcu, Markulf Kohlweiss, Kenji Maillard

Materials

• Lecture 1 (Markulf): Verifying TLS in F*; Everest Project
• Lecture 2 (Catalin): A Gentle Introduction to F* (code)
• Lecture 3 & 4 (Catalin, Kenji): Verifying Stateful Programs with F* (code)
• Lecture 5 (Markulf): Code-Based Cryptographic Verification in F*

Code

• Code from F* slides
• Exercises from F* slides; solutions
• Encrypt then mac example

Setup

• Online editor
• Other ways to install F*

More references

• F* website
• F* tutorial
• F* code on GitHub