Methods for Automatic Analysis of Security Sensitive Protocols

Methods for Automatic Analysis of Security Sensitive Protocols

Status

This project has started in April 2005 and ended in March 2007.

Researchers

Prof. Dr. David Basin, Information Security Group, ETH
Sebastian Mödersheim, Information Security Group, ETH

Background

Since 2001, we are developing, and continously extending a tool for the analysis of security sensitive protocols: the On-the-Fly Model-Checker OFMC. OFMC is integrated in the AVISPA project where a common input language for several analysis tools has been defined. Besides developing and implementing methods, we have also investigated the theoretical background of modeling security protocols.

Results

• Algebraic reasoning. We have formalized, and implemented into OFMC, a framework for handling algebraic properties of cryptographic operators. For instance, Diffie-Hellman based protocols rely on a property of (modular) exponentiation, namely that exponents commute. Our framework provides a great amount of flexibility to the user who can specify an algebraic theory modulo which the analysis of protocols is performed. Also, the framework allows for the integration of existing specialized algorithms for algebraic reasoning. OFMC now can handles cancelation theory (such as “encryption and decryption cancel each other out”) and finite theories (such as commutativity and associativity of operators).
• Comparison of models. We have considered the relationship between two popular models in protocol verification: a transition system style model as used in OFMC and a trace based model that does not have an explicit notion of local states of honest agents. Several approaches are inspired on the trace based model as it over-approximates the search space. This over-approximation, together with abstract interpretation techniques, offers an efficient approach for verifying security protocols without bounding the number of sessions.