Sebastian Mödersheim



Associate professor in the Software Systems Engineering section at DTU Compute.

Contact

Sebastian Mödersheim
DTU Informatics
Richard Petersens Plads, Building 321, Room 018
DK-2800 Kgs. Lyngby, Denmark
Email: samo@dtu.dk


Tools and Sources

noname and α-β privacy

PSPSP

Compositional Reasoning

Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL

AIF-Omega (Set-based abstraction)

Open-Source Fixed-Point Model-Checker OFMC

  • Latest version 2024 supporting both AnB and a fragment of ASLan.
  • Most relevant papers: Overview paper, Constraint Differentiation, Algebraic Intruder Deductions, Secure Pseudonymous Channels, Algebraic Properties in Alice and Bob Notation, Integrating Automated and Interactive Protocol Verification.

    SPS/APS and APCC: Protocols, Typing, and Composition

    Tool suite by Omar Almousa, Sebastian Mödersheim, Paolo Modesti, and Luca Viganò.
  • Security Protocol Specification Language SPS: An Alice-and-Bob style language (extends AnB and FutureID's APS) with formats.
  • Includes translators to Applied Pi/ProVerif and IF/OFMC
  • Automatic Protocol Composition Checker APCC: for a given set of protocols check that the sufficient conditions of [AMMV15] for typing and parallel composition are met. This tool is based on a master thesis by Ivana Kojovic.
  • Download as zip.

    • Publications

    Early Access Drafts

    1. Laouen Fernet, Sebastian Mödersheim, Luca Viganò: A Compositionality Result for Alpha-Beta Privacy. Manuscript, 2024.
    2. Laouen Fernet, Sebastian Mödersheim, and Luca Viganò: A Typing Result for Alpha-Beta Privacy. Manuscript, 2024.

    Journals

    1. Andreas Hess, Sebastian Mödersheim, Achim Brucker, and Anders Schlichtkrull: PSPSP: A Tool for Automated Verification of Stateful Protocols in Isabelle/HOL, JCS 2025, doi:10.1177/0926227X251358741. Preprint
    2. Andreas Hess, Sebastian Mödersheim, and Achim Brucker. Stateful Protocol Composition in Isabelle/HOL. In ACM Transactions on Privacy and Security, 2023.
    3. Koen Tange, Sebastian Mödersheim, Apostolos Lalos, Xenofon Fafoutis, and Nicola Dragoni. rTLS: Secure and Efficient TLS Session Resumption for the Internet of Things. In MDPI 21(19), 2021. PDF
    4. Sebastian Mödersheim and Luca Viganò. Alpha-Beta Privacy. In ACM Transactions on Privacy and Security, 2018. Preprint available
    5. Michele Bugliesi, Stefano Calzavara, Sebastian Mödersheim, and Paolo Modesti. Security Protocol Specification and Verification with AnBx. Journal of Information Security and Applications (JISA), 2016. Preprint.
    6. Sebastian Mödersheim, Luca Viganò, and David Basin. Constraint Differentiation: Search-Space Reduction for the Constraint-Based Analysis of Security Protocols. In Journal of Computer Security, 18(4), pages 575-618, 2010.
    7. Sebastian Mödersheim. On the Relationships between Models in Protocol Verification. In Journal of Information and Computation, 206 (2-4), pages 291-311, 2008.
    8. David Basin, Sebastian Mödersheim, and Luca Viganò. OFMC: A symbolic model checker for security protocols. In International Journal of Information Security, 4 (3), pages 181-208, 2005.

    Conferences and Workshops

    1. Sebastian Mödersheim and Siyu Chen: Accountable Banking Transactions, Open Identity Summit 2024.
    2. Laouen Fernet, Sebastian Mödersheim, and Luca Viganò: A Decision Procedure for Alpha-Beta Privacy for a Bounded Number of Transitions, CSF 2024. Extended version.
    3. Laouen Fernet and Sebastian Mödersheim: Private Authentication with Alpha-Beta Privacy. In OID 2023, pp. 61--72. DOI: 10.18420/OID2023_05.
    4. Sébastien Gondron, Sebastian Mödersheim and Luca Viganò: Privacy as Reachability. CSF 2022, Open Access, manuscript available.
    5. Sebastian Mödersheim: Rewriting Privacy. Invited paper at WRLA 2022.
    6. Sebastian Mödersheim and Jorge Cuellar: Three Branches of Accountability. In Festschrift for Joshua Guttman, LNCS 13066, 2021.
    7. Alessandro Bruni, Marco Carbone, Rosario Giustolisi, Sebastian Mödersheim and Carsten Schürmann: Security Protocols as Choreographies. In Festschrift for Joshua Guttman, LNCS 13066, 2021.
    8. Laouen Fernet and Sebastian Mödersheim. Deciding a Fragment of (alpha, beta)-Privacy. STM 2021. Preprint available
    9. Sébastien Gondron, Sebastian Mödersheim and Luca Viganò: Privacy as Reachability. Manuscript, 2021.
    10. Sébastien Gondron and Sebastian Mödersheim. Vertical Composition and Sound Payload Abstraction for Stateful Protocols. CSF 2021. Extended version available
    11. Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull: Performing Security Proofs of Stateful Protocols. CSF 2021. Preprint Isabelle Sources
    12. Lukas Alber, Stefan More, Sebastian Mödersheim, and Anders Schlichtkrull: Adapting the TPL Trust Policy Language for a Self-Sovereign Identity World. OID 2021
    13. Anders Schlichtkrull and Sebastian Mödersheim. Accountable Trust Decisions: A Semantic Approach. OID 2020.
    14. Sébastien Gondron and Sebastian Mödersheim. Formalizing and Proving Privacy Properties of Voting Protocols using Alpha-Beta Privacy. ESORICS 2019.
    15. Sebastian Mödersheim, Anders Schlichtkrull, Georg Wagner, Stefan More and Lukas Alber: TPL: A Trust Policy Language. IFIPTM 2019.
    16. Sebastian Mödersheim and Bihang Ni. GTPL: A Graphical Trust Policy Language. Open Identity Summit 2019.
    17. Andreas V. Hess, Sebastian A. Mödersheim and Achim D. Brucker. Stateful Protocol Composition. ESORICS 2018. Extended version Isabelle sources
    18. Andreas V. Hess and Sebastian Mödersheim. A Typing Result for Stateful Protocols. CSF 2018. Extended version available as a Technical Report.
    19. Andreas V. Hess and Sebastian Mödersheim. Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL. CSF 2017. Preprint Isabelle Sources.
    20. Sebastian Mödersheim and Alessandro Bruni. AIF-omega: Set-Based Protocol Abstraction with Countable Families. POST 2016. Preprint. Tool page.
    21. Sören Bleikertz, Thomas Groß, Sebastian Mödersheim, and Carsten Vogel. Proactive Security Analysis of Changes in Virtualized Infrastructures ACSAC 2015.
    22. 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.
    23. Omar Almousa, Sebastian Mödersheim, and Luca Viganò. Alice and Bob: Reconciling Formal Models and Implementation. Festschrift in honor of Pierpaolo Degano, 2015; extended abstract at CryptoForma 2015; Extended version available
    24. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson, and Hanne Riis Nielson. Set-π: Set Membership π-calculus, CSF 2015; Extended version with corrections of 2018.
    25. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson, and Hanne Riis Nielson. Verification of Stateful Protocols: Set-Based Abstractions in the Applied π-Calculus, NordSec 2014, LNCS vol. 8788, Springer, 2014.
    26. Sebastian Mödersheim and Georgios Katsoris. A Sound Abstraction of the Parsing Problem. CSF 2014. Extended version available.
    27. Sebastian Mödersheim and Luca Viganò. Sufficient Conditions for Vertical Composition of Security Protocols. ASIACCS 2014. Extended version.
    28. Sebastian Mödersheim, Thomas Groß and Luca Viganò. Defining Privacy is Supposed to be Easy. LPAR 2013.
    29. Sören Bleikertz, Thomas Groß, Sebastian Mödersheim. Security Analysis of Dynamic Infrastructure Clouds. Workshop on Trustworthy Clouds. 2013
    30. Alessio Di Mauro, Xenofon Fafoutis, Sebastian Mödersheim, Nicola Dragoni. Detecting and Preventing Beacon Replay Attacks. Nordsec 2013.
    31. Ali Kassem, Pascal Lafourcade, Yassine Lakhnech, Sebastian Mödersheim. A Decision Procedure for Solving Constraint Systems in Presence of Multiple Independent Intruders. Hot Spot 2013.
    32. Sebastian Mödersheim, Flemming Nielson, Hanne Riis Nielson. Lazy Mobile Intruders. POST 2013. Available as IMM TR-2012-13.
    33. Sebastian Mödersheim. Deciding Security for a Fragment of ASLan. ESORICS 2012. Extended Corrected Version of April 2018.
    34. The AVANTSSAR project. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. TACAS 2012.
    35. Sören Bleikertz, Thomas Groß, and Sebastian Mödersheim. Automated Verification of Virtualized Infrastructures. CCSW 2011.
    36. Sebastian Mödersheim. Diffie-Hellman without Difficulty. FAST 2011.
    37. Thomas Groß and Sebastian Mödersheim. Vertical Protocol Composition. CSF 2011. (Extended version available)
    38. Sebastian Mödersheim and Paolo Modesti. Verifying SeVeCom Using Set-based Abstraction. IWCMC 2011. AIF models available as part of the AIF Framework (OFMC-FP-ASLan) version 2010b.
    39. David v. Oheimb and Sebastian Mödersheim. ASLan++ FMCO 2010.
    40. Sebastian Mödersheim. Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases, CCS 2010. Implementation available: AIF Framework.
    41. Sebastian Mödersheim and Dieter Sommer and Jan Camenisch. A Formal Model of Identity Mixer, FMICS 2010, LNCS 6371, 2010.
    42. Jan Camenisch, Sebastian Mödersheim, Gregory Neven, Franz-Stefan Preiss, and Dieter Sommer. A card requirements language enabling privacy-preserving access control. In ACM Symposium on Access Control Models and Technologies (SACMAT) 2010.
    43. Achim Brucker and Sebastian Mödersheim. Integrating Automated and Interactive Protocol Verification. In Workshop on Formal Aspects in Security and Trust (FAST 2009). Lecture Notes in Computer Science (5983), pages 248-262, Springer-Verlag, 2009.
    44. Sebastian Mödersheim and Luca Viganò. Secure Pseudonymous Channels. Proceedings of ESORICS 2009. Springer-Verlag. Extended version available as IBM Research Report RZ3724.
    45. Sebastian Mödersheim. Algebraic Properties in Alice and Bob Notation. Proceedings of Ares 2009. IEEE Computer Society, 2009. Extended version available as IBM Research Report RZ3709.
    46. Paul Hankes Drielsma, Sebastian Mödersheim, Luca Viganò, and David Basin. Formalizing and Analyzing Sender Invariance. In Proceedings of FAST'06, LNCS 4691, pages 80-95. Springer-Verlag, 2006.
    47. Michael Backes, Sebastian Mödersheim, Birgit Pfitzmann, and Luca Viganò. Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario. In Proceedings of FOSSACS'06. LNCS 3921, pages 428-445. Springer-Verlag, 2006.
    48. David Basin, Sebastian Mödersheim, and Luca Viganò. Algebraic Intruder Deductions. In Proceedings of LPAR'05. LNAI 3835, pages 549-564. Springer-Verlag, 2005.
    49. Alessandro Armando, David Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Pierre-Cyrille Heám, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michael Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In Proceedings of CAV'2005. LNCS 3576, pages 281-285. Springer-Verlag, 2005.
    50. Paul Hankes Drielsma, Sebastian Mödersheim, and Luca Viganò. A Formalization of Off-Line Guessing for Security Protocol Analysis. In Proceedings of LPAR'04, LNAI 3452, pages 363-379. Springer-Verlag, 2005
    51. Paul Hankes Drielsma and Sebastian Mödersheim. The ASW Protocol Revisited: A Unified View. In Proceedings of ARSPA'04. ENTCS 125(1), pages 141-156, 2004.
    52. Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Jacopo Mantovani, Sebastian Mödersheim, and Laurent Vigneron. A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In Proceedings of SAPS'04, 2004.
    53. David Basin, Sebastian Mödersheim, and Luca Viganò. An On-The-Fly Model-Checker for Security Protocol Analysis. In Proceedings of Esorics'03. LNCS 2808, pages 253--270. Springer-Verlag, 2003.
    54. David Basin, Sebastian Mödersheim, and Luca Viganò. Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols (Extended Abstract). In Proceedings of SPV'03, pages 8--13. 2003.
    55. David Basin, Sebastian Mödersheim, and Luca Viganò. Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols. In Proceedings of CCS'03, pages 335-344. ACM Press, 2003.
    56. Alessandro Armando, David Basin, Mehdi Bouallagui, Yannick Chevalier, Luca Compagna, Sebastian Mödersheim, Michael Rusinowitch, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. The AVISS Security Protocol Analysis Tool. In Proceedings of CAV'02. LNCS 2404, pages 349--354. Springer-Verlag, 2002.
    57. David Basin, Stefan Friedrich, and Sebastian Mödersheim. B2M: A Semantic Based Tool for BLIF Hardware Descriptions. In Proceedings of FMCAD 2000. LNCS 1954, pages 91-107. Springer-Verlag, 2000.

    Books and Book chapters

    1. Sebastian Mödersheim and Catuscia Palamidessi (Ed.). Proceedings of TOSCA: Theory of Security and Applications, LNCS 6993, 2012. (See also TOSCA webpage.)
    2. Roberto Carbone, Marius Minea, Sebastian Mödersheim, Serena Elisa Ponta, Mathieu Turuani, and Luca Viganò. Towards Formal Validation of Trust and Security of the Internet of Services. FIA Book 2011, LNCS 6656.
    3. Sebastian Mödersheim and Luca Viganò. The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols. Fosad 2007-2008-2009, LNCS 5705, 166-194. Springer-Verlag, 2009.
    4. Sebastian Mödersheim. Models and Methods for the Automated Analysis of Security Protocols. PhD thesis, ETH Zürich, 2007.

    Patents

    1. United States Patent 7,480,801. Method for securing data traffic in a mobile network environment. With Martin Euchner, Volkmar Lotz, and Haykal Tej.