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 supports the development of the OFMC tool, the On-the-Fly Model-Checker for security protocols. As shown in the figure (right), the user specifies the protocol and the goal (e.g. mutual authentication) as the input for OFMC:
As is standard in formal protocol verification, OFMC uses an abstract model of cryptographic primitives (such as symmetric and asymmetric encryption, hash functions, or modular exponentiation). In contrast to most existing approaches, this interpretation is not fixed, but can be chosen by the user in form of an algebraic theory of the used function symbols. As a result, OFMC either replies with “Verified” in case no attack is found or with an “Attack Trace” which illustrates a violation of the goal that can happen.
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.
Images
Figure 1. OFMC tool.
