Vertical Composition of Distributed Systems

Sébastien Pierre Christophe Gondron: Communicating on networks, like the Internet, requires to run a wide variety of security protocols.

The specification and the analysis of their security properties is a fully-fledged research area. However, despite their actual deployment within real environment, security protocols have been mostly and comprehensively considered in isolation. Only little work has been undertaken about their compositions. Indeed, being proven secure in isolation is not a guarantee that their compositions are also secure.

In the literature, three families of compositions are classically identified: parallel, sequential and vertical. Based on previous results, the project CompoSec: Secure Composition of Distributed Systems studied these compositions. The goals of the project are to provide compositionality results that are feasible in practice, i.e. that work for real-world protocols.

The previous results focus on parallel and sequential compositions. A number of typing results have been proven for security protocols. One of the main contribution of the project has been to lift these typing results to stateful protocols. Based on these typing results, a parallel composition result for stateful protocol has been obtained and there are initial ideas for using this result also for sequential results. These compositionality results have a modular form: “given a suite of protocols that satisfy certain sufficient conditions and that are secure in isolation then any way to compose them is a secure system as well”. These conditions are easy to check statically.

In this PhD project, we are particularly concerned with vertical compositions. These are of great importance on the layered Internet for instance. One can think of the numerous protocols that establish keys or secure channels, such as Diffie-Hellman or TLS and the protocols actually using these established keys to be run over the secure “channels".

PhD project by Sébastien Pierre Christophe Gondron

Section: Formal methods for safe and secure systems

Principal supervisor: Sebastian Alexander Mödersheim
Co-supervisors: Alberto Lluch Lafuente

Title of project: Vertical Composition of Distributed Systems

Project start: 2018-2021


Sébastien Pierre Christophe Gondron
PhD student
DTU Compute
+45 45 25 37 34


Sebastian Alexander Mödersheim
Associate Professor
DTU Compute
+45 45 25 37 34


Alberto Lluch Lafuente
Head of Section, Associate Professor
DTU Compute
+45 45 25 37 36