@book{8f490c17712a410a830d9c0bf7a20f43,
title = "Sufficient Conditions for Vertical Composition of Security Protocols (Extended Version)",
abstract = "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.",
author = "M{\"o}dersheim, {Sebastian Alexander} and Luca Vigan{\`o}",
note = "The work presented in this paper was partially supported by the EU FP7 Projects no. 318424, {"}FutureID: Shaping the Future of Electronic Identity{"} (futureid.eu), 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.",
year = "2014",
language = "English",
series = "DTU Compute-Technical Report-2014",
publisher = "DTU Compute",
number = "7",
}