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

合作研究：CT-M：密码协议分析统一实验室

• 批准号: 0831305
• 负责人: Christopher Lynch
• 金额: $ 12.5万
• 依托单位: Clarkson University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-09-01 至 2010-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0831305&HistoricalAwards=false
• 关键词: Collaborative; Research; CT; Unification; Laboratory

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.

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