---
title: Seminar by Felix Stutz on Automated Verification of Security Protocols 
---
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)](http://vtss.doc.ic.ac.uk/publications/DOsualdo2017Deciding.html), 
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.