We are very pleased to welcome Felix Stutz, an MSc student at the International Max Planck Research School for Computer Science, who is due to spend five months with the group, working with Emanuele D’Osualdo on Ideal completions for Verification of Cryptographic Protocols.

These protocols are distributed programs that are designed to achieve secure communications using cryptography; they are notoriously very tricky to design and reasoning about the security properties of these protocols requires proving that no malicious intruder can hack the protocol to gain sensitive information, e.g. your emails.

In fact, every time you log in to your email account, make an online payment or connect to a secure Wi-Fi (and in many other scenarios!) the communication is made secure under the hood by the use of such cryptographic protocols. The project’s goal is to develop new algorithms to verify that a protocol does not leak any secret.

For the theoretical basis for the project please see this paper by D’Osualdo and others, which proposes a new approach for model checking cryptographic protocols.