TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools

该奖项根据 2009 年美国复苏和再投资法案（公法 111-5）提供资金。该项目开发考虑密码系统代数属性的密码协议推理技术。传统上，密码协议验证的正式方法将密码操作视为黑匣子，忽略了可用于设计攻击的密码算法的属性。所提出的研究使用基于方程统一的新颖方法来为与密码协议相关的代数理论构建新的更具表现力和更有效的搜索算法。方程统一给出了所有情况的紧凑表示，在这些情况下，两个不同的项对应于相同的行为。 这些算法被实现并集成到 Maude-NPA 中，该系统在符号协议分析方面取得了成功。事实证明，Maude-NPA 在丰富了如此强大的统一算法后，可以分析协议并确保其可靠性，这是其他方法无法做到的。改进的安全分析技术有助于确保系统没有错误，并基于通过正式分析获得的信心加快新系统的接受速度。这项研究将导致下一代协议分析工具的设计和实现。开发的算法将作为适合协议分析工具使用的库提供给研究人员。该项目的工具将帮助学生理解与协议设计相关的概念并获得实践经验。代数理论的方程统一不仅对于协议分析有用，而且对于一般的程序分析也有用，从而使该项目的结果具有广泛的相关性。

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).The project develops cryptographic protocol reasoning techniquesthat take into account algebraic properties of cryptosystems.Traditionally, formal methods for cryptographic protocolverification view cryptographic operations as a black box,ignoring the properties of cryptographic algorithms that can beexploited to design attacks. The proposed research uses a novelapproach based on equational unification to build new moreexpressive and efficient search algorithms for algebraic theoriesrelevant to cryptographic protocols. Equational unification givesa compact representation of all circumstances under which twodifferent terms correspond to the same behavior. The algorithmsare implemented and integrated into Maude-NPA, a system that hasbeen successful in symbolic protocol analysis. It is demonstratedthat Maude-NPA when enriched with such powerful unificationalgorithms can analyze protocols and ensure their reliability,which could not be done otherwise.Improved techniques for analyzing security are helpful both inassuring that systems are free of bugs, and in speeding up theacceptance of new systems based on the confidence gained by aformal analysis. This research will lead to the design andimplementation of next generation tools for protocol analysis.Algorithms developed will be made available to researchers as alibrary suitable for use with protocol analysis tools. Tools fromthe project will help students understand concepts relevant toprotocol design and get hands-on experience. Equationalunification for algebraic theories is not only useful forprotocol analysis, but also for program analysis in general, thusmaking the results of this project to be widely relevant.