Descriptif

The security of communications heavily relies on cryptography. For decades, mathematicians have invested an immense effort in providing cryptography that is built on firm mathematical foundations. This has lead to a collection of cryptographic primitives whose correctness can be proved by drawing on results from branches of mathematics such as complex analysis, algebraic geometry, representation theory and number theory. A stated goal of recent competitions for cryptographic standards is to gain trust from the broad cryptography community through open and transparent processes.

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.