TWC: Small: Automated Protocol Design and Refinement

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

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.