Understanding Abstractions of Secure Channels

摘要

Many security architectures make use of layered security protocols, where a special-purpose application protocol is layered on top of a general-purpose secure transport protocol. When analysing such an architecture, it makes sense to abstract away from the implementation details of the secure transport protocol and just model the services it provides. But is this abstraction sound, or might it risk losing attacks? This is the question we consider in this paper. We show that -under certain assumptions- the abstraction is sound, in the sense that it correctly models the application-layer behaviour as seen by honest principals.