Sep 25

Automatic synthesis of cryptographic protocols

Automatic synthesis methods, developed by the formal methods community, are based on different extensions of game theory and aim to produce algorithms and tools that automatically write (synthesize) pieces of code that comply with certainty with a given specification. These methods have mainly been applied to safely synthesize key elements of critical systems, where no failures are tolerated. The objective of this thesis is to explore the opportunity to apply these same techniques to synthesize cryptographic protocols such as fair-exchange protocols and/or key exchange protocols.

Directors: Gilles Geeraerts and Olivier Markowitch