Sound Security Protocol Transformations
Thanh Binh Nguyen, Christoph Sprenger · Repository for Publications and Research Data (ETH Zurich) · 2013
We propose a class of protocol transformations, which can be used to (1) develop (families of) security protocols by refinement and (2) abstract existing protocols to increase the efficiency of verification tools. We prove the soundness of these transformations with respect to an expressive security property specification language covering secrecy and authentication properties. Our work clarifies and significantly extends the scope of earlier work in this area. We illustrate the usefulness of our approach on a family of key establishment protocols.