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

题目：合作研究：CT-M：加密协议分析统一实验室机构：纽约州立大学奥尔巴尼分校摘要：日期：08年8月13日对不同方程理论的推理能力对于加密协议的分析是非常重要的。了解协议使用的函数的相等性质是如何被入侵者利用的，这对于发现可能被遗漏的缺陷是非常宝贵的。在文献中，甚至在现场协议中都有许多例子。用等式理论进行密码协议分析的一个非常强大的工具是等式统一。均衡性统一是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.