Sufficient Conditions for Vertical Composition of Security Protocols (Extended Version)

Research output: Book/ReportReportResearch

129 Downloads (Pure)


Vertical composition of security protocols means that an application protocol (e.g., a banking service) runs over a channel established by another protocol (e.g., a secure channel provided by TLS). This naturally gives rise to a compositionality question: given a secure protocol P1 that provides a certain kind of channel as a goal and another secure protocol P2 that assumes this kind of channel, can we then derive that their vertical composition P2[P1] is secure? It is well known that protocol composition can lead to attacks even when the individual protocols are all secure in isolation. In this paper, we formalize seven easy-to-check static conditions that support a large class of channels and applications and that we prove to be su_cient for vertical security protocol composition.
Original languageEnglish
PublisherDTU Compute
Number of pages20
Publication statusPublished - 2014
SeriesDTU Compute-Technical Report-2014

Bibliographical note

The work presented in this paper was partially supported by the EU FP7 Projects no. 318424, "FutureID: Shaping the Future of Electronic Identity" (, and no. 257876,"SPaCIoS: Secure Provision and Consumption in the Internet of Services", and by the PRIN 2010-2011 Project "Security Horizons". Much of this work was carried out while Luca Vigano was at the Dipartimento di Informatica, Universita di Verona, Italy. This report extends the paper "Sufficient Conditions for Vertical Composition of Security Protocols" appearing in the proceedings of the 9th ACM Symposium on Information, Computer and Communications Security (ASIACCS 2014), held in Kyoto, Japan, June 4{6, 2014.

Fingerprint Dive into the research topics of 'Sufficient Conditions for Vertical Composition of Security Protocols (Extended Version)'. Together they form a unique fingerprint.

Cite this