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.