Vertical Protocol Composition

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


    The security of key exchange and secure channel protocols, such as TLS, has been studied intensively. However, only few works have considered what happens when the established keys are actually used—to run some protocol securely over the established “channel”. We call this a vertical protocol composition, and it is truly commonplace in today’s communication with the diversity of VPNs and secure browser sessions. In fact, it is normal that we have several layers of secure channels: For instance, on top of a VPN-connection, a browser may establish another secure channel (possibly with a different end point). Even using the same protocol several times in such a stack of channels is not unusual: An application may very well establish another TLS channel over an established one. We call this selfcomposition. In fact, there is nothing that tells us that all these compositions are sound, i.e., that the combination cannot introduce attacks that the individual protocols in isolation do not have. In this work, we prove a composability result in the symbolic model that allows for arbitrary vertical composition (including self-composition). It holds for protocols from any suite of channel and application protocols that fulfills a number of sufficient preconditions. These preconditions are satisfied for many practically relevant protocols such as TLS.
    Original languageEnglish
    Title of host publicationProceedings of the 24th Computer Security Foundations Symposium 2011
    Publication date2011
    Publication statusPublished - 2011
    EventThe Computer Security Foundations Symposium - Abbaye des Vaux de Cernay, France
    Duration: 1 Jan 2011 → …
    Conference number: 24


    ConferenceThe Computer Security Foundations Symposium
    CityAbbaye des Vaux de Cernay, France
    Period01/01/2011 → …


    Dive into the research topics of 'Vertical Protocol Composition'. Together they form a unique fingerprint.

    Cite this