Project overview
Most weaknesses in security protocols are not due to flaws of the underlying cryptography, but they are caused by logical mistakes in the protocols’ construction. The detection of these mistakes is particularly difficult, since we are concerned with a distributed system where some nodes and the communication medium are hostile. The human mind can easily overlook possible shortcomings in such a setting. We therefore need automated methods to rigorously analyze security protocols and security-critical systems.
IBM is a partner of the AVANTSSAR project that extends existing models and methods of protocol verification to the verification of service-oriented architectures. In particular we plan to
- Design the new specification language ASLan
- Develop methods and tools for automatically analyzing services
- Develop a library of verified examples.
Publications
- Sebastian Mödersheim and Luca Viganò. Secure Pseudonymous Channels. Proceedings of ESORICS 2009, to appear.
Extended version available as IBM Research Report RZ3724.
- Sebastian Mödersheim. Algebraic Properties in Alice and Bob Notation. Proceedings of Ares 2009. DOI Bookmark. IEEE Computer Society, 2009.
Extended version available as IBM Research Report RZ3709. - Sebastian Mödersheim. On the relationships between models in protocol verification . Information and Computation, 206 (2-4), pages 291-311, 2008.
- Sebastian Mödersheim. Models and Methods for the Automated Analysis of Security Protocols. PhD Thesis, ETH Zürich, 2007.
- David Basin and Sebastian Mödersheim and Luca Viganò. Algebraic Intruder Deductions. In LPAR 2005, LNAI 3835, 2005.
- David Basin and 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.
