Collaborative Research: CT-M: Unification Laboratory for Cryptographic Protocol Analysis

对不同方程理论的推理能力对于密码协议的分析是非常重要的。 了解协议所使用的函数的等式性质如何被入侵者利用，对于发现可能被遗漏的缺陷非常重要。 在文献中甚至在现场协议中存在许多例子。等式统一是用等式理论进行密码协议分析的一个非常有力的工具。EquationalUnification是NRL协议分析器（Maude-NPA）的基础。它对这些理论的使用使它既能重现现有的缺陷，又能发现新的缺陷，其精度远远超过当时其他工具的精度。这表明，方程的统一，如果适当的扩展，可以提供支持，以类似的方式分析密码协议，使用的功能，服从更expressiveequational理论。这个项目的目的是提供一个实验室的方程统一，将开发的算法和技术，可用于支持使用的方程统一在密码协议分析。这项工作将包括两个部分：统一算法的发展理论的利益，以密码协议分析，和新技术的发展，采用统一的密码协议分析。该项目将有助于下一代协议分析工具的设计和实现。在项目中开发的工具可以提供给其他研究人员的正式protocolanalysis方法，以及协议设计者的实验。该项目的教育部分将涉及两个机构的本科生和研究生。

The ability to reason about different equational theories is veryimportant to the analysis of cryptographic protocols. An understanding ofhow equational properties of a function used by a protocol can beexploited by an intruder can be invaluable in finding flaws that mightotherwise be missed. Numerous examples exist in the literature and evenin fielded protocols. One very powerful tool for cryptographic protocolanalysis with equational theories is equational unification. EquationalUnification was the basis of the NRL Protocol Analyzer (Maude-NPA). Itsuse of these theories allowed it to both reproduce existing flaws and findnew ones at a level of precision way beyond that available to other toolsat its time. This suggests that equational unification if properlyextended, can give support in a similar fashion to analysis ofcryptographic protocols that use functions that obey more expressiveequational theories. The aim of this project is to provide alaboratory for equational unification that will develop the algorithmsand techniques that can be used to support the use of equationalunification in cryptographic protocol analysis. This effort willconsist of two parts: the development of unification algorithms fortheories of interest to cryptographic protocol analysis, and the developmentof new techniques for employing unification in cryptographic protocolanalysis. The project will help in the design and implementation of nextgeneration tools for protocol analysis. Tools developed in the projectwill be made available to other researchers working on formal protocolanalysis methods as well as to protocol designers for experimentation. Theeducational component of the project will involve undergraduate andgraduate students at both institutions.