Sebastian Mödersheim



Associate professor in LBT at DTU Compute.

Contact

Sebastian Mödersheim
DTU Informatics
Richard Petersens Plads, Building 324, Room 160
DK-2800 Kgs. Lyngby, Denmark
Email: samo@imm.dtu.dk
Phone: +45 45 25 35 97

Cool: Hot Spot


Tools

Open-Source Fixed-Point Model-Checker OFMC

  • Latest version 2014 supporting both AnB and a fragment of ASLan.
    1. Release includes source code and executables for windows and mac.
    2. Compiling from source requires the Haskell Platform
    3. Previous version: 2013a.
  • 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.

  • Related tool: An Automatic Protocol Composition Checker by Ivana Kojovic (Master Thesis).

    AIF Framework (Set-based abstraction)

  • Latest version 2010b (including source code and SEVECOM example).
  • Relevant papers: Abstraction by Set-Membership, Verifying SeVeCom Using Set-based Abstraction

    Publications

    Journals

    1. 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.
    2. Sebastian Mödersheim. On the Relationships between Models in Protocol Verification. In Journal of Information and Computation, 206 (2-4), pages 291-311, 2008.
    3. 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.

    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 Alexander 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.

    Conferences and Workshops

    1. Sebastian Mödersheim and Georgios Katsoris. A Sound Abstraction of the Parsing Problem. CSF 2014, to appear. Extended version available.
    2. Sebastian Mödersheim and Luca ViganÚ. Sufficient Conditions for Vertical Composition of Security Protocols. ASIACCS 2014, to appear. Extended version.
    3. Sebastian Mödersheim, Thomas Groß and Luca ViganÚ. Defining Privacy is Supposed to be Easy. LPAR 2013.
    4. Sören Bleikertz, Thomas Groß, Sebastian Mödersheim. Security Analysis of Dynamic Infrastructure Clouds. Workshop on Trustworthy Clouds. 2013
    5. Alessio Di Mauro, Xenofon Fafoutis, Sebastian Mödersheim, Nicola Dragoni. Detecting and Preventing Beacon Replay Attacks. Nordsec 2013.
    6. 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.
    7. Sebastian Mödersheim, Flemming Nielson, Hanne Riis Nielson. Lazy Mobile Intruders. POST 2013. Available as IMM TR-2012-13.
    8. Sebastian Mödersheim. Deciding Security for a Fragment of ASLan. ESORICS 2012. Extended Version IMM-TR-2012-06 .
    9. The AVANTSSAR project. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. TACAS 2012.
    10. Sören Bleikertz, Thomas Groß, and Sebastian Mödersheim. Automated Verification of Virtualized Infrastructures. CCSW 2011.
    11. Sebastian Mödersheim. Diffie-Hellman without Difficulty. FAST 2011.
    12. Thomas Groß and Sebastian Mödersheim. Vertical Protocol Composition. CSF 2011. (Extended version available)
    13. 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.
    14. David v. Oheimb and Sebastian Mödersheim. ASLan++ FMCO 2010.
    15. Sebastian Mödersheim. Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases, CCS 2010. Implementation available: AIF Framework.
    16. Sebastian Mödersheim and Dieter Sommer and Jan Camenisch. A Formal Model of Identity Mixer, FMICS 2010, LNCS 6371, 2010.
    17. 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.
    18. 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.
    19. Sebastian Mödersheim and Luca ViganÚ. Secure Pseudonymous Channels. Proceedings of ESORICS 2009. Springer-Verlag. Extended version available as IBM Research Report RZ3724.
    20. 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.
    21. 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.
    22. 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.
    23. David Basin, Sebastian Mödersheim, and Luca ViganÚ. Algebraic Intruder Deductions. In Proceedings of LPAR'05. LNAI 3835, pages 549-564. Springer-Verlag, 2005.
    24. 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.
    25. 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
    26. 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.
    27. 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.
    28. 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.
    29. 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.
    30. 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.
    31. 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.
    32. 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.

    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.