SECURING THE INTERNET OF THE FUTURE. SECURE MESSAGING.
Our complex world needs many security mechanisms at all levels. History has shown repeatedly that designing security mechanisms for complex systems is extremely hard to get right. We therefore not only would like propose new security mechanisms, but would also like to develop analysis methods to provide strong security guarantees for the mechanisms that we and others design. We aim for a world in which we don't just have to believe that a mechanism provides security, but can instead provide a strong mathematical guarantee.
Securing the internet of the future. The most widely used security mechanism on the internet that is used by every internet user, is the Transport Layer Security protocol (TLS) that underpins the green lock seen in browsers, and is behind the 's' in 'https:'. We have contributed to the new version of this standard (TLS 1.3) by applying the analysis methods that we developed, detecting a critical flaw in a proposed design early. In ongoing work, we are developing our analysis methods further to provide fully automated analysis of such complex new mechanisms, and will contribute to future developments.
Secure messaging. In recent years, the messaging systems that are available to users have been greatly improved in terms of the security they offer. However, it remains complex to make a definite statement about their security. Are these new systems without attacks? Can we still further improve them? In parallel to answering these questions, we have been proposing new designs for a future open standard for secure messaging with the Internet Engineering Task Force (IETF).
The Future of Security Verification. While we have developed state-of-the-art tools for the automated analysis of security mechanisms, many open problems remain, both in terms of the scale of systems we can analyse and the type of properties we can reason about. We are working on many lines of research to identify and develop possible approaches for the future of security verification, which will enables us to provide more accurate analyses for the ever more complex secure systems of the future.
