TWC: Small: Automated Protocol Design and Refinement

TWC：小型：自动化协议设计和完善

• 批准号: 1617307
• 负责人: Jay McCarthy
• 金额: $ 40万
• 依托单位: University of Massachusetts Lowell
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-08-15 至 2020-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1617307&HistoricalAwards=false
• 关键词: TWC; Small; Automated; Protocol; Design

Online security relies on communication protocols that establish trust and authentication. New protocols are created regularly, such as when Software-as-a-Service companies expose their software through new Web services. In the ideal case, network engineers and protocol experts collaborate to develop a protocol: one responsible for its efficiency and the other for its security. Unfortunately, this ideal is rarely realized. Protocol experts are rare and their techniques are too complicated for solo network engineers to use, who instead just follow informal "best practices." As a result, most of these protocols end up with security problems. This research investigates an automated protocol expert that provides the network engineer with the service normally given by the human protocol expert. The availability of this open-source expert will broadly impact the trustworthiness of cyberspace by increasing the security and reliability of the online services that use it.The PI will construct this expert after three technical advances: first, a new security property specification language based on protocol goals, as opposed to the details of the operation of a protocol, for use by network engineers; second, a new theory of protocol construction based on the composition of disjoint authentication protocols with restrictions from linear logic used to limit the sharing of sensitive information; and third, a theory of protocol optimization based on the attack calculus already used to prove that protocols are secure. These three new theories advance their respective sub-fields and coalesce into the necessary foundation for the automated protocol expert.

在线安全依赖于建立信任和身份验证的通信协议。新协议是定期创建的，例如当软件即服务公司通过新的Web服务公开其软件时。在理想的情况下，网络工程师和协议专家合作开发协议：一个负责其效率，另一个负责其安全性。不幸的是，这种理想很少实现。协议专家很少，他们的技术对于单独的网络工程师来说太复杂了，他们只是遵循非正式的“最佳实践”。因此，这些协议中的大多数最终都会出现安全问题。本研究调查了一个自动协议专家，它为网络工程师提供通常由人类协议专家提供的服务。这位开源专家的出现将通过提高使用网络空间的在线服务的安全性和可靠性，广泛地影响网络空间的可信度。PI将在三个技术进步之后构建这个专家：首先，一种新的基于协议目标的安全属性规范语言，而不是协议操作的细节，供网络工程师使用；其次，提出了一种新的协议构建理论，该理论基于线性逻辑约束下的不相交认证协议组合，用于限制敏感信息的共享；第三，基于攻击演算的协议优化理论已经被用来证明协议的安全性。这三种新理论推进了各自的子领域，并共同构成了自动化协议专家的必要基础。