Increasing the Scope of Automated Protocol Analysis

This project with Prof Cas Cremers (formally of Oxford and now with the Helmholtz Center for Information Security (CISPA) a German national BigScience Institution) was one of the most successful grants let during my predecessors assignment (2016-2018).Prof Cremers research group gained notoriety in performing detailed security analysis of the TLS draft specification the Transport Layer Security protocol is the de facto means for securing communications across the Internet. Prof Cremers research group studied the draft TLS 1.3 specification for three years while it was open for public review and comment. In their research, the team developed a fine-grain, modular, and well-annotated symbolic model of TLS 1.3 (draft 21) using the Tamarin prover, proved a majority of the protocols security requirements, and uncovered a security weakness. This model was built with the explicit goal of transparency which increases the models longevity and allows it to be used as the security protocol is updated over time which is certain to happen. Within the grant period, Prof Cremers' group produced two top tier research papers and regularly briefed DVs as they came through the EOARD office and/or made visits to Oxford University. Lastly, it is important to note that this project was a very good example of basic research approaches, tools, and science being applied to a real world problem of considerable interest as the group modeled and analyzed all of the TLS 1.3 (draft 21) protocols handshake modes (a likely place for security breaches to occur). The annotated model is available on the web for download and use. Due to the confluence of multiple events: the EOARD IPOs rotated, the PI changed universities, and the new IPO deployed the final financial paperwork was never received.