Abstractions for security protocol verification

We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. </span>We propose abstractions that transform a term\textquoterights structure based on its\&nbsp;type as well as abstractions that remove atomic messages, variables, and redundant terms.\&nbsp;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.\&nbsp;We prove soundness results for an expressive property language that includes secrecy and authentication.\&nbsp;Applying our abstractions to realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers