*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.