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

提案标题：协作研究：CT-M：密码协议分析统一实验室机构：位于奥尔巴尼的纽约州立大学摘要日期：08/13/08对不同的方程理论进行推理的能力对密码协议的分析非常重要。了解入侵者如何利用协议使用的函数的等式属性，对于发现本来可能会被忽略的漏洞非常有价值。在文献中甚至在现场协议中都有许多例子。用方程理论分析密码协议的一个非常强大的工具是方程统一。等式统一是NRL协议分析器(Maude-NPA)的基础。这些理论的使用使得它既可以复制现有的缺陷，又可以发现新的缺陷，其精度远远超过当时其他工具所能达到的水平。这表明，如果适当地扩展，等式统一可以以类似的方式支持对使用服从更具表现力的方程理论的函数的密码协议的分析。这个项目的目的是为等式统一提供一个平台，以开发可用于支持在密码协议分析中使用等式统一的算法和技术。这项工作将包括两个部分：为密码协议分析感兴趣的理论开发统一算法，以及开发在密码协议分析中使用统一的新技术。该项目将有助于设计和实施下一代协议分析工具。该项目中开发的工具将提供给从事正式协议分析方法的其他研究人员以及协议设计者进行实验。该项目的教育部分将涉及两所大学的本科生和研究生。

Proposal Title: Collaborative Research: CT-M: Unification Laboratory forCryptographic Protocol AnalysisInstitution: SUNY at AlbanyAbstract Date: 08/13/08The 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.