Abstract:

On the Relationships between Models in Protocol Verification (Extended Version)

Sebastian Mödersheim


We formally investigate the relationship between several models that are widely-used in protocol verification, namely variants of inductive message-trace models inspired by Paulson’s approach based on the Isabelle theorem prover, and models based on rewriting. More precisely, we prove that some of these models are over-approximations of others inthe sense that they allow strictly more traces or reachable states. This is common in verification: often an over-approximation is easier to prove correct than the original model, and proving the over-approximation is safe implies that the original model is safe—provided that the models are indeed in an over-approximation relation. The contributions of this paper are firstly to formally prove such an over-approximation relation between models, and secondly to give a precise account on the differentkinds of over-approximations.