CompoSec: Secure Composition of Distributed Systems

A Sapere Aude research project in the Formal Methods group at DTU Compute.

About the Project

Many of the Internet services we use every day are in fact a composition of many components, for instance:

In fact, running different protocols and applications in parallel on the same communication medium is also a composition. While many of these components have been studied intensively in isolation, there is not much research on whether their composition is actually secure.

Our goals are:

Results and Publications

  1. Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull: Performing Security Proofs of Stateful Protocols. CSF 2021, to appear. Preprint Isabelle Sources
  2. Sébastien Gondron and Sebastian Mödersheim. Formalizing and Proving Privacy Properties of Voting Protocols using Alpha-Beta Privacy. ESORICS 2019.
  3. Andreas V. Hess, Sebastian A. Mödersheim, and Achim D. Brucker. Stateful Protocol Composition. ESORICS 2018. Extended version available.
  4. The Isabelle Formalization of the full parallel composition result.
  5. Andreas V. Hess and Sebastian Mödersheim. A Typing Result for Stateful Protocols CSF 2018, extended version available as a Technical Report.
  6. Andreas V. Hess and Sebastian Mödersheim. Formalizing and Proving a Typing Result for SecurityProtocols in Isabelle/HOL. CSF 2017. Preprint
  7. The Isabelle Formalization of a Typing Result for Security Protocols.

Previous Results

  1. Omar Almousa, Sebastian Mödersheim, Paolo Modesti, and Luca Viganò: Typing and Compositionality for Security Protocols: A Generalization to the Geometric Fragment. ESORICS 2015 Extended Version version available.
  2. Sebastian Mödersheim and Georgios Katsoris. A Sound Abstraction of the Parsing Problem. CSF 2014. Extended version available.
  3. Sebastian Mödersheim and Luca Viganò. Sufficient Conditions for Vertical Composition of Security Protocols. ASIACCS 2014. Extended version.
  4. Thomas Groß and Sebastian Mödersheim. Vertical Protocol Composition. CSF 2011. (Extended version available)
  5. Sebastian Mödersheim and Luca Viganò. Secure Pseudonymous Channels. Proceedings of ESORICS 2009. Springer-Verlag. Extended version available as IBM Research Report RZ3724.

Researchers

Sebastian Mödersheim
Forskningsleder
Andreas Viktor Hess
Postdoc
Sébastien Pierre Christophe Gondron
PhD Student