Introduction to Formal Methods

In this context, computer-aided verification can impulse a major evolution. Computer-aided proofs can be verified independently and efficiently: to verify a computer-aided proof, it suffices to read (and agree with) its main statement and to run automatically the verification tool to check that it accepts the proof. Because they break the symmetry between building and checking proofs (in terms of the amount of time and expertise required), which prevails in pen-and-paper proofs, computer-aided tools can deliver trustworthy proofs. Second, computer-aided tools can be used to justify many methods used by practitioners for making their implementations secure; for instance, certified program analyses are perfectly suited for resolving the relative lack of mathematical rigor in practical cryptography.

 

This course will introduce formal methods in general and its application in the domain of cryptography, from the provable security of algorithms to the provable and side-channel security of both human-readable and high-performance reference implementations.