Collaborative research: High-Fidelity Methods for Security Protocols

提案编号：0430594,0429689,0430076,0430595标题：协作研究：安全协议的高保真方法PI：John Mitchell，Andre Scedrov，Vitaly Shmatkov，Daniele Micciancio使用加密原语的协议的设计和安全分析是计算机安全研究的最基本和最具挑战性的领域之一。本项目关注三个主题：协议分析的基础、自动化工具以及工具和方法在选定协议中的应用。基础性工作集中于关联和组合两种以前分开的方法：基于协议符号执行的逻辑方法，以及涉及概率和多项式时间的计算方法。符号方法使用了一种高度理想化的密码原语表示法，并已成为自动化工具的成功基础。相反，计算方法可以更深入地了解协议的优点和漏洞，但很难应用，而且只有该领域的少数真正专家才能接触到。在过去使用几个自动化工具取得成功的基础上，该项目将设计基于工具的方法，利用新的科学基础。三个可能的应用领域是安全群组通信和密钥协商协议、隐私保护计算方案以及无线网络和应用。在这些领域中的每一个领域，用户社区目前都有对新的安全协议的需求，研究和标准化社区正在进行活动，结合符号和计算分析概念的价值是显而易见的。

Proposal Number: 0430594, 0429689, 0430076, 0430595 TITLE: Collaborative Research: High-Fidelity Methods for Security Protocols PI: John Mitchell, Andre Scedrov, Vitaly Shmatikov, Daniele MicciancioThe design and security analysis of protocols that use cryptographic primitives is one of the most fundamental and challenging areas of computer security research. This project focuses on three topics: foundations of protocol analysis, automated tools, and application of tools and methods to selected protocols. Foundational work centers on relating and combining two previously separate approaches: logical methods based on symbolic execution of protocols, and computational methods involving probability and polynomial-time. The symbolic approach uses a highly idealized representation of cryptographic primitives and has been a successful basis for automated tools. Conversely, the computational approach yields more insight into the strength and vulnerabilities of protocols, but is difficult to apply and only accessible to a small number of true experts in the field. Building on past success using several automated tools, the project will devise tool-based methods that leverage new scientific foundations. Three likely application areas are secure group communication and key agreement protocols, schemes for privacy-preserving computations, and wireless networking and applications. In each of these areas, there is current demand for new secure protocols from user communities, there is ongoing activity in the research and standardization communities, and the value of combining symbolic and computational analysis concepts is evident.