Affiliations: [a] Institute of Networks and Security, Johannes Kepler University, Linz, Austria | [b] Institute of Information Security, Department of Computer Science, ETH Zurich, Switzerland | [c] Department of Computer Science, University of Oxford, United Kingdom
Note: [**] Most of this work was done while this author was working at ETH Zurich, Switzerland.
Abstract: We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We propose abstractions that transform a term’s structure based on its type as well as abstractions that remove atomic messages, variables, and redundant terms. Our theory improves on previous work by supporting rewrite theories with the finite-variant property, user-defined types, and untyped variables to cover type flaw attacks. We prove soundness results for an expressive property language that includes secrecy and authentication. Applying our abstractions to realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers.
