CompoSec: Secure Composition of Distributed Systems
A
DFF 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:
- TLS to establish a secure connection between an unauthenticated
client and a server
- An identity solution like the Danish NemID to authenticate the
client
- Some application running between client and server, e.g., online banking
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:
- 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.
Downloads
-
StateProtCompIsabelle
The latest version of the
Isabelle Compositionality Library for Stateful Security Protocols.
- PSPSP
An automated
verifier for stateful security protocols in Isabelle, compatible
with StateProtCompIsabelle
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
Protocols. CSF
2021. Preprint Isabelle
Formalization (Conference Version) or Isabelle
Formalization (Latest Version)
- Sébastien
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
available.
- 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
Isabelle/HOL. CSF
2017. Preprint
- The Isabelle Formalization of a Typing Result for Security Protocols.
Previous Results
- 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.
- 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.
Extended version.
- 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.
Researchers
