This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).
The project develops cryptographic protocol reasoning techniques that take into account algebraic properties of cryptosystems. Traditionally, formal methods for cryptographic protocol verification view cryptographic operations as a black box, ignoring the properties of cryptographic algorithms that can be exploited to design attacks. The proposed research uses a novel approach based on equational unification to build new more expressive and efficient search algorithms for algebraic theories relevant to cryptographic protocols. Equational unification gives a compact representation of all circumstances under which two different terms correspond to the same behavior. The algorithms are implemented and integrated into Maude-NPA, a system that has been successful in symbolic protocol analysis. It is demonstrated that Maude-NPA when enriched with such powerful unification algorithms can analyze protocols and ensure their reliability, which could not be done otherwise.
Improved techniques for analyzing security are helpful both in assuring that systems are free of bugs, and in speeding up the acceptance of new systems based on the confidence gained by a formal analysis. This research will lead to the design and implementation of next generation tools for protocol analysis. Algorithms developed will be made available to researchers as a library suitable for use with protocol analysis tools. Tools from the project will help students understand concepts relevant to protocol design and get hands-on experience. Equational unification for algebraic theories is not only useful for protocol analysis, but also for program analysis in general, thus making the results of this project to be widely relevant.
