The ability to reason about different equational theories is very important to the analysis of cryptographic protocols. An understanding of how equational properties of a function used by a protocol can be exploited by an intruder can be invaluable in finding flaws that might otherwise be missed. Numerous examples exist in the literature and even in fielded protocols. One very powerful tool for cryptographic protocol analysis with equational theories is equational unification. Equational Unification was the basis of the NRL Protocol Analyzer (Maude-NPA). Its use of these theories allowed it to both reproduce existing flaws and find new ones at a level of precision way beyond that available to other tools at its time. This suggests that equational unification if properly extended, can give support in a similar fashion to analysis of cryptographic protocols that use functions that obey more expressive equational theories. The aim of this project is to provide a laboratory for equational unification that will develop the algorithms and techniques that can be used to support the use of equational unification in cryptographic protocol analysis. This effort will consist of two parts: the development of unification algorithms for theories of interest to cryptographic protocol analysis, and the development of new techniques for employing unification in cryptographic protocol analysis. The project will help in the design and implementation of next generation tools for protocol analysis. Tools developed in the project will be made available to other researchers working on formal protocol analysis methods as well as to protocol designers for experimentation. The educational component of the project will involve undergraduate and graduate students at both institutions.
