**CCIS Seminar - Thursday 18 October 2012 - salle A. Turing CE4**

*14:00:00 - *__Salle de salle A. Turing CE4__## My Own Little Hilbert's Program: Relative Soundness Results in Protocol Verification

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

Home page CCIS Seminars

How to come to **salle A. Turing CE4** - http://www-verimag.imag.fr/Plan-d-acces.html?lang=fr