Sebastian Mödersheim


Me, hiding between some supervillains (to confuse Google Images).

Associate professor in LBT at DTU Compute.

Contact

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

Tools

Open-Source Fixed-Point Model-Checker OFMC

  • Latest version 2012c supporting both AnB and a fragment of ASLan.
    1. It integrates the older version 2011c and the experimental version of the AVANTSSAR Tool Page
    2. Release includes source code and binaries for windows and mac.
    3. Compiling from source requires the Haskell Platform (tested with version 2012.2.0.0, which uses ghc 7.0.4). The Haskell libraries frequently change without backwards compatibility, so other versions of ghc may not work without adapting the source code.
  • 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.

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