salle A. Turing CE4
18 October 2012 - 14h00
My Own Little Hilbert's Program: Relative Soundness Results in Protocol Verification
by Sebastian Moedersheim from DTU Informatics
Abstract: In protocol verification there is an increasing
number of relative soundness results that allow to reduce complex
verification problems to simpler ones. For example for large classes
of protocols we can show: if there is an attack then there is a
well-typed attack. Another example are compositionality results of
the form: if the composition of several protocols has an attack,
then one of them in isolation already has an attack. What these
results have in common is that in both cases we can work with some
notion of types of messages and that confusions are either
excluded or irrelevant. Moreover there is a simple way to prove such
results by using a popular protocol verification technique, briefly
called the lazy intruder.
My own little Hilbert's program is to explore how far we can get
with this approach and how to use it in practical protocol
verification. We will discuss several relative soundness results and
a decision procedure for a typeable fragment of the AVANTSSAR
Specification Language ASLan.
Slides of the Presentation.
