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.
The latest extension of OFMC includes the novel easy-to-use protocol specification language AnB based on Alice and Bob notation. It supports the specification of protocols that require
- Algebraic reasoning
- Secure and pseudonymous channels
- Zero knowledge proofs.
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.
