Newer
Older
---
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.