Equational unification and its application in formal verification of cryptographic protocols
Paliath Narendran, Lida Wang · 2004
The goal of cryptographic protocols is to provide secure communication, and after one time running of a protocol is finished, some accomplishments should be achieved. These accomplishments may include: a key is shared secretly between two authentic users; a user is successfully convinced of the identity of another user; etc. However, if a cryptographic protocol is not designed correctly, it may fail to accomplish the goal it is designed to accomplish. Security flaws can be subtle and hard to find. Formal verification of cryptographic protocols intends to give rigorous and thorough means of protocol analysis so that even the subtlest error of a protocol can be found. Most versions of the state-based approach towards formal cryptographic protocol analysis is based on Dolev and Yao model. Their model of intruder activity does not consider any algebraic property of cryptographic primitives, making the perfect encryption assumption: that is, the cryptosystems are free of any properties except that encryption and decryption with the same key cancel each other out. The NRL Protocol Analyzer (NPA) by Catherine Meadows that this thesis is inspired by is also based on the Dolev-Yao model, but it extends it in many ways, and in particular, relaxes the perfect encryption assumption. Currently, the NPA exploits the state exploration facility by simple unification in combination with equational unification using a narrowing procedure (Narrowing is a procedure that is used to find solutions with respect to a set of terminating rewrite rules). We study equational unification problems with respect to five theories capturing properties of modular multiplication and exponentiation operations that are used in many modern cryptographic algorithms and could not be represented using terminating rewrite systems. For two of these theories, algorithms of equational unification are given, whereas for the remaining three theories, equational unification problems are proved to be undecidable. As a byproduct, we develop a new algorithm for computing strong Grobner bases for right ideals in Z , an algebraic structure similar to a polynomial ring over the integers, except that the indeterminates do not commute.