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

点击翻译按钮获取中文摘要

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.