Felix Stutz gave a talk on Monday on Automated Verification of Security Protocols. He presented the latest work on the project he is doing with Emanuele D’Osualdo and which will inform his Master Thesis.

The abstract is: Security protocols are distributed programs that are designed to achieve secure communications using cryptography. A distinctive feature of the security properties of protocols is that they must hold in the presence of an active adversarial environment, and this makes them challenging to verify. An important example of such a security property is secrecy: can the protocol leak a (secret) message to the environment as a result of interference by the intruder? This project’s goal is to develop a new algorithm to verify secrecy of cryptographic protocols with unbounded sessions and nonces. The novelty of the approach, based on a new decidability result by D’Osualdo et al. (CSF17), is in how the unboundedness caused by the use of unlimited nonces can be tamed algorithmically. We will present a new verification algorithm for secrecy based on symbolic representations of inductive invariants of protocols.