CompoSec: Secure Composition of Distributed Systems
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
- TLS to establish a secure connection between an unauthenticated
client and a server
- An identity solution like the Danish NemID to authenticate the
- Some application running between client and server, e.g., online banking
Our goals are:
- Real-world Compositionality Results that are applicable to today's systems
without modification -- instead of strong unrealistic assumptions.
- A Unified Framework. Make explicit and order the diversity of
existing compositionality results within a single
general model with machine-checked proofs in the Isabelle theorem prover.
- Tool Support. Verifier that checks whether a given set
of components satisfies the conditions for secure composition and
suggests changes otherwise.
The latest version of the
Isabelle Compositionality Library for Stateful Security Protocols.
verifier for stateful security protocols in Isabelle, compatible
Results and Publications
Sébastien Gondron and Sebastian
Mödersheim. Vertical Composition and Sound Payload
Abstraction for Stateful Protocols. CSF 2021. Extended version available
Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and
Anders Schlichtkrull: Performing Security Proofs of Stateful
2021. Preprint Isabelle
Formalization (Conference Version) or Isabelle
Formalization (Latest Version)
Gondron and Sebastian Mödersheim. Formalizing and Proving Privacy Properties of Voting
Protocols using Alpha-Beta Privacy. ESORICS 2019.
- Andreas V. Hess, Sebastian A. Mödersheim,
and Achim D. Brucker. Stateful
Protocol Composition. ESORICS 2018. Extended version
- The Isabelle
Formalization (Conference Version) of the full parallel composition result.
- Andreas V. Hess and Sebastian Mödersheim. A Typing
Result for Stateful Protocols CSF 2018, extended version
available as a Technical Report.
- Andreas V. Hess and Sebastian Mödersheim. Formalizing
and Proving a Typing Result for SecurityProtocols in
- The Isabelle Formalization of a Typing Result for Security Protocols.
- 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
- Sebastian Mödersheim and Georgios Katsoris. A Sound Abstraction of the
Parsing Problem. CSF 2014. Extended version available.
- Sebastian Mödersheim and Luca Viganò.
Sufficient Conditions for Vertical Composition of Security
Protocols. ASIACCS 2014.
- Thomas Groß and Sebastian Mödersheim. Vertical
Protocol Composition. CSF 2011. (Extended version available)
- Sebastian Mödersheim and Luca Viganò. Secure Pseudonymous
Channels. Proceedings of ESORICS 2009. Springer-Verlag.
Extended version available as IBM
Research Report RZ3724.