1 Department of Applied Mathematics and Computer Science, Technical University of Denmark2 Language-Based Technology, Department of Applied Mathematics and Computer Science, Technical University of Denmark3 King’s College London
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.