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.