TWC: Small: Automated Protocol Design and Refinement

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

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.