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.

对不同方程理论进行推理的能力对于加密协议的分析非常重要。 对协议使用的函数的方程属性的理解可以由入侵者探索，这对于发现可能遗漏的缺陷是无价的。 文献中存在许多示例，并且均匀的方案中存在。具有方程理论的加密协议分析的一种非常强大的工具是方程统一。方程式化是NRL协议分析仪（Maude-NPA）的基础。这些理论的使用使其既可以重现现有的缺陷，又可以在其他工具的时间以外的精确级别上以某种精确的方式重现出来。这表明，如果正确地延迟了方程式统一，则可以以类似的方式提供与使用符合更富有表现力理论的函数的分析方案的支持。该项目的目的是为方程统一提供鉴定性，该方程统一将开发算法和技术，可用于支持加密协议分析中的方程式化。这项努力将是两个部分的努力：开发统一算法为密码协议分析的利益理论，以及用于在加密协议分析中采用统一的新技术的开发。该项目将有助于设计和实施下一代工具进行协议分析。在项目中开发的工具将提供给从事正式协议分析方法的其他研究人员以及用于实验的协议设计人员。该项目的教育组成部分将涉及两个机构的本科生和研究生。