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.